Agda Versions Save

Agda is a dependently typed programming language / interactive theorem prover.

nightly

2 weeks ago

What's Changed

New Contributors

Full Changelog: https://github.com/agda/agda/compare/v2.6.4.3...nightly

v2.6.4.3

2 months ago

Release notes for Agda version 2.6.4.3

This release fixes a regression in 2.6.4.3 and one in 2.6.4. It aims to be API-compatible with 2.6.4.1 and 2.6.4.2.

Agda 2.6.4.3 supports GHC versions 8.6.5 to 9.8.1.

Closed issues

For 2.6.4.3, the following issues were closed (see bug tracker):

  • Issue #7148: Regression in 2.6.4.2 concerning with
  • Issue #7150: Regression in 2.6.4 in rewrite with instances

Full Changelog: https://github.com/agda/agda/compare/v2.6.4.2...v2.6.4.3

v2.6.4.2

2 months ago

Release notes for Agda version 2.6.4.2

This is a bug-fix release. It aims to be API-compatible with 2.6.4.1. Agda 2.6.4.2 supports GHC versions 8.6.5 to 9.8.1.

Highlights

List of closed issues

For 2.6.4.2, the following issues were closed (see bug tracker):

  • Issue #6972: Unfolding fails when code is split up into multiple files
  • Issue #6999: Unification failure for function type with erased argument
  • Issue #7020: question: haskell backend extraction of Data.Nat.DivMod.DivMod?
  • Issue #7029: Internal error on confluence check when rewriting a defined symbol with a hole
  • Issue #7033: transpX clauses can be beat out by user-written _ clauses, leading to proof of ⊥
  • Issue #7034: Internal error with --two-level due to blocking on solved meta
  • Issue #7044: Serializer crashes on blocked definitions when using --allow-unsolved-metas
  • Issue #7048: hcomp symbols in interface not hidden under --cubical-compatible
  • Issue #7059: Don't recompile if --keep-pattern-variables option changes
  • Issue #7070: Don't set a default maximum heapsize for Agda runs
  • Issue #7081: Missing IsString instance with debug flags enabled
  • Issue #7095: Agda build flags appear as "automatic", but they are all "manual"
  • Issue #7104: Warning "there are two interface files" should not be serialized
  • Issue #7105: Internal error in generate-helper (C-c C-h)
  • Issue #7113: Instance resolution runs too late, leads to with-abstraction failure

These PRs not corresponding to issues were merged:

  • PR #6988: Provide a .agda-lib for Agda builtins
  • PR #7065: Some documentation fixes
  • PR #7072: Add 'Inference in Agda' to the list of tutorials
  • PR #7091: Add course to “Courses using Agda”

What's Changed (merged PRs, auto-generated)

Full Changelog: https://github.com/agda/agda/compare/v2.6.4.1...v2.6.4.2

v2.6.4.1

5 months ago

Release notes for Agda version 2.6.4.1

This is a minor release of Agda 2.6.4 featuring a few changes:

  • Make recursion on proofs legal again.
  • Improve performance, e.g. by removing debug printing unless built with cabal flag debug.
  • Switch to XDG directory convention.
  • Reflection: change to order of results returned by getInstances.
  • Fix some internal errors.

Installation

  • Agda supports GHC versions 8.6.5 to 9.8.1.

  • Verbose output printing via -v or --verbose is now only active if Agda is built with the debug cabal flag. Without debug, no code is generated for verbose printing, which makes building Agda faster and Agda itself faster as well. (PR #6863)

Language

  • A change in 2.6.4 that prevented all recursion on proofs, i.e., members of a type A : Prop ℓ, has been reverted. It is possible again to use proofs as termination arguments. (See issue #6930.)

Reflection

Changes to the meta-programming facilities.

  • The reflection primitive getInstances will now return instance candidates ordered by specificity, rather than in unspecified order: If a candidate c1 : T has a type which is a substitution instance of that of another candidate c2 : S, c1 will appear earlier in the list.

    As a concrete example, if you have instances F (Nat → Nat), F (Nat → a), and F (a → b), they will be returned in this order. See issue #6944 for further motivation.

Library management

  • Agda now follows the XDG base directory standard on Unix-like systems, see PR #6858. This means, it will look for configuration files in ~/.config/agda rather than ~/.agda.

    For backward compatibility, if you still have an ~/.agda directory, it will look there first.

    No change on Windows, it will continue to use %APPDATA% (e.g. C:/Users/USERNAME/AppData/Roaming/agda).

Other issues closed

For 2.6.4.1, the following issues were also closed (see bug tracker):

  • #6745: Strange interaction between opaque and let open
  • #6746: Support GHC 9.8
  • #6852: Follow XDG Base Directory Specification
  • #6913: Internal error on primLockUniv-sorted functions
  • #6930: Termination checking with --prop: change in 2.6.4 compared with 2.6.3
  • #6931: Internal error with an empty parametrized module from a different file
  • #6941: Interaction between opaque and instance arguments
  • #6944: Order instances by specificity for reflection
  • #6953: Emacs 30 breaks agda mode
  • #6957: Agda stdlib installation instructions broken link
  • #6959: Warn about opaque unquoteDecl/unquoteDef
  • #6983: Refine command does not work on Emacs 30

What's Changed (auto-generated)

New Contributors

Full Changelog: https://github.com/agda/agda/compare/v2.6.4...v2.6.4.1

v2.6.3

7 months ago

v2.6.4

7 months ago