[Agda] [ANNOUNCE] Agda 2.6.4 release candidate 2
Andreas Abel
andreas.abel at ifi.lmu.de
Thu Sep 14 08:40:36 CEST 2023
Dear all,
The Agda Team is very pleased to announce the second release candidate
of Agda 2.6.4.
A big thank-you to everyone who gave us feedback on the first release
candidate! Changes in RC2 over RC1 are summarized at:
https://github.com/agda/agda/pull/6849
# 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.3 RC2 has been tested with GHC 9.6.2, 9.4.6, 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.3 RC2 can be installed using cabal-install or stack:
* Getting the release candidate
$ cabal get
https://hackage.haskell.org/package/Agda-2.6.3.20230914/candidate/Agda-2.6.3.20230914.tar.gz
$ cd Agda-2.6.3.20230914
* Using cabal-install
$ cabal install
* Using stack
$ stack --stack-yaml stack-a.b.c.yaml install
replacing `a.b.c` with your version of GHC.
# Standard library
You can use standard library v1.7.2 or the `master` branch of the
standard library with Agda 2.6.4 RC2. This branch is available at
https://github.com/agda/agda-stdlib/
# Fixed issues
https://hackage.haskell.org/package/Agda-2.6.3.20230914/candidate/changelog
Enjoy Agda 2.6.4 RC2 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
More information about the Agda
mailing list