[Agda] Agda 2.7.0 release candidate 2
Andreas Abel
andreas.abel at ifi.lmu.de
Wed Jul 31 23:08:48 CEST 2024
Dear all,
The Agda Team is pleased to announce a second release candidate (RC2)
for Agda 2.7.0.
# Chnages over RC1
* Reverted PR #5627 which had made options like --type-in-type infective.
* Fixed issues #7382 (internal error in deserialization) and #7401
(`cabal install --lib`).
# Highlights of Agda 2.7.0
* Mimer, a re-implementation of the "auto" term synthesizer,
replaces Agsy.
* New syntax `using x ← e` to bind values on the left-hand-side
of a function clause.
* Instance search is more performant thanks to a new indexing structure.
Additionally, users can now control how instances should be selected
in the case multiple candidates exist.
* User-facing options `--exact-split`, `--keep-pattern-variables`,
and `--postfix-projections` are now on by default.
# GHC supported versions
Agda 2.7.0 RC 2 has been tested with GHC 9.10.1, GHC 9.8.2, GHC 9.6.6,
9.4.8, 9.2.8, 9.0.2, 8.10.7, 8.8.4 and 8.6.5 on Linux, macOS and Windows.
# Installation
Agda 2.7.0 RC 2 can be installed using cabal-install or stack:
1. Getting the release candidate
$ cabal get
https://hackage.haskell.org/package/Agda-2.6.20240731/candidate/Agda-2.6.20240731.tar.gz
$ cd Agda-2.6.20240731
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 (8.8.4 or higher).
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 the `experimental` branch of the
standard library with Agda 2.7.0. This branch is available at
https://github.com/agda/agda-stdlib/
# Changes and fixed issues over Agda 2.6.4.3
https://hackage.haskell.org/package/Agda-2.6.20240731/candidate/changelog
Enjoy the Agda 2.7.0 RC 2 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
--
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