Agda 2.8.0 released

Announcements
1

Dear all,

The Agda Team is pleased to announce the release of Agda 2.8.0.

Highlights of 2.8.0

  • Agda is now a self-contained single binary.
  • Build all Agda files reachable from paths in the .agda-lib file with new flag --build-library.
  • Experimental support for polarity annotations with new flag --polarity.
  • Compile to JavaScript with ES6 module syntax with new flag --js-es6.
  • Errors now have an identifier and follow the GNU standard.

GHC supported versions

Agda 2.8.0 has been tested with GHC 9.12.2, 9.10.2, GHC 9.8.4, GHC 9.6.7, 9.4.8, 9.2.8, 9.0.2, 8.10.7, and 8.8.4 on Linux, macOS and Windows.

Installation

Binaries for Linux, MacOS and Windows are available from
Release v2.8.0 · agda/agda · GitHub
(built without -f enable-cluster-counting).

Agda 2.8.0 can be installed from source using cabal-install or stack:

  1. Getting the released source
    cabal get Agda-2.8.0
    cd Agda-2.8.0
  2. a. Using cabal-install
    cabal install -f +enable-cluster-counting
  3. b. Using stack
    stack --stack-yaml stack-a.b.c.yaml install --flag Agda:enable-cluster-counting
    replacing a.b.c with your version of GHC (8.8.4 or higher).

The flag means:

  • enable-cluster-counting:
    Enable unicode clusters for alignment in the LaTeX backend.
    Requires the ICU lib to be installed and known to pkg-config.

This flag can be dropped from the install if causing trouble.

Standard library

You can use the master branch of the
standard library with Agda 2.8.0. This branch is available at

GitHub - agda/agda-stdlib: The Agda standard library

Changes and fixed issues over Agda 2.7.0.1

Changelog for Agda-2.8.0 | Hackage

Enjoy Agda 2.8.0!
Andreas, on behalf of the Agda Team

15 Likes