Dear all, The Agda Team is very pleased to announce the release of Agda 2.6.4. Thanks to everyone who gave us feedback on the release candidates! # Highlights of Agda 2.6.4 * Cubical Agda now displays boundary conditions in interactive mode (PR [#6529](https://github.com/agda/agda/pull/6529)). * An inconsistency in the treatment of large indices has been fixed (Issue [#6654](https://github.com/agda/agda/issues/6654)). * Unfolding of definitions can now be fine-controlled via `opaque` definitions. * Additions to the sort system: `LevelUniv` and `PropĪ`. * New flag `--erasure` with several improvements to erasure (declared run-time irrelevance). * New reflection primitives for meta-programming. # GHC supported versions Agda 2.6.4 has been tested with GHC 9.6.3, 9.4.7, 9.2.8, 9.0.2, 8.10.7, 8.8.4 and 8.6.5 on Linux, macOS and Windows. # Installation Agda 2.6.4 can be installed using cabal-install or stack: 1. Getting the tarball $ cabal update $ cabal get Agda-2.6.4 $ cd Agda-2.6.4 2. a. Using cabal-install $ cabal install -f +optimise-heavily -f +enable-cluster-counting 2. b. Using stack $ stack --stack-yaml stack-a.b.c.yaml install --flag Agda:optimise-heavily --flag Agda:enable-cluster-counting replacing `a.b.c` with your version of GHC. The flags mean: - optimise-heavily: Turn on extra optimisation for a faster Agda. Takes large resources during compilation of Agda. - enable-cluster-counting: Enable unicode clusters for alignment in the LaTeX backend. Requires the ICU lib to be installed and known to pkg-config. These flags can be dropped from the install if causing trouble. # Standard library You can use standard library v1.7.2 or the `master` branch of the standard library with Agda 2.6.4. This branch is available at https://github.com/agda/agda-stdlib/ # Fixed issues over Agda 2.6.3 https://hackage.haskell.org/package/Agda-2.6.4/changelog Enjoy Agda! Andreas, on behalf of the Agda Team _______________________________________________ Agda mailing list Agda@lists.chalmers.se https://lists.chalmers.se/mailman/listinfo/agda