[Agda] [ANNOUNCE] Agda 2.6.4 release candidate 3
Andreas Abel
abela at chalmers.se
Sat Sep 30 18:25:16 CEST 2023
Dear all,
The Agda Team is very pleased to announce the third release candidate
of Agda 2.6.4.
Thanks to everyone who gave us feedback on the previous release
candidates! Changes in RC3 over RC2 are summarized at:
https://github.com/agda/agda/pull/6893
# 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 RC2 has been tested with GHC 9.6.2, 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 RC2 can be installed using cabal-install or stack:
1. Getting the release candidate
$ cabal get
https://hackage.haskell.org/package/Agda-2.6.3.20230930/candidate/Agda-2.6.3.20230930.tar.gz
$ cd Agda-2.6.3.20230930
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 RC3. 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.3.20230930/candidate/changelog
Enjoy Agda 2.6.4 RC3 and please test as much as possible.
Report problems and regressions to: https://github.com/agda/agda/issues
--
Andreas, on behalf of the Agda Team
_______________________________________________
Agda mailing list
Agda at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda
--
Andreas Abel <>< Du bist der geliebte Mensch.
Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden
andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/
More information about the Agda
mailing list