[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