[Agda] Agda 2.7.0 release candidate 1
Andreas Abel
andreas.abel at ifi.lmu.de
Sun Jul 14 19:37:51 CEST 2024
Dear all,
The Agda Team is pleased to announce a release candidate for Agda 2.7.0.
# Highlights
* 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 1 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 1 can be installed using cabal-install or stack:
1. Getting the release candidate
$ cabal get
https://hackage.haskell.org/package/Agda-2.6.20240714/candidate/Agda-2.6.20240714.tar.gz
$ cd Agda-2.6.20240714
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.20240714/candidate/changelog
Enjoy the Agda 2.7.0 RC 1 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