[Agda] Agda 2.7.0 released!
Andreas Abel
abela at chalmers.se
Fri Aug 16 17:16:45 CEST 2024
Dear all,
The Agda Team is pleased to announce Agda 2.7.0!
# 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 3 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 can be installed using cabal-install or stack:
1. Getting the release candidate
$ cabal get Agda-2.7.0
$ cd Agda-2.7.0
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/
A 2.7.0-compatible version of the Agda standard library should be
available soon(ish), progress is tracked on:
https://github.com/agda/agda-stdlib/issues/2461
# Changes and fixed issues over Agda 2.7.0
https://hackage.haskell.org/package/Agda-2.7.0/changelog
Enjoy Agda 2.7.0!
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