[Haskell-cafe] [ANNOUNCE] Agda

Andreas Abel abela at chalmers.se
Thu Nov 30 18:33:25 UTC 2023

Dear all,

The Agda Team is pleased to announce Agda

Agda is a minor release of Agda 2.6.4 featuring a few changes:

- Make recursion on proofs legal again (regression in 2.6.4).
- Improve performance, e.g. by removing debug printing unless built with 
cabal flag `debug`.
- Switch to XDG directory convention.
- Reflection: change to order of results returned by `getInstances`.
- Fix some internal errors.
- Fix some issues with `opaque`.

# GHC supported versions

Agda has been tested with GHC 9.8.1, GHC 9.6.3, 9.4.7, 9.2.8, 
9.0.2, 8.10.7, 8.8.4 and 8.6.5 on Linux, macOS and Windows.

# Installation

Agda can be installed using cabal-install or stack:

1. Getting the tarball

         $ cabal update
         $ cabal get Agda-
         $ cd Agda-

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.

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 standard library v1.7.3 or v2.0 (soon to be released) of the
standard library with Agda

# Fixed issues over Agda 2.6.4


Enjoy Agda!

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

More information about the Haskell-Cafe mailing list