[Haskell-cafe] [ANNOUNCE] Agda 2.6.4
Andreas Abel
abela at chalmers.se
Fri Oct 6 13:53:39 UTC 2023
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 at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda
More information about the Haskell-Cafe
mailing list