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