[ANN] Agda 2.6.4 released

Announcements
#1

The Agda Team is very pleased to announce the release of Agda 2.6.4.

Highlights of Agda 2.6.4

  • Cubical Agda now displays boundary conditions in interactive mode
    (PR #6529).

  • An inconsistency in the treatment of large indices has been fixed
    (Issue #6654).

  • Unfolding of definitions can now be fine-controlled via opaque definitions.

  • Additions to the sort system: LevelUniv and Propω.

  • New flag --erasure with several improvements to erasure (declared run-time irrelevance).

  • New reflection primitives for meta-programming.

GHC supported versions

Agda 2.6.4 has been tested with 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 2.6.4 can be installed using cabal-install or stack:

  1. Getting the tarball

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

  2. a. Using cabal-install

     $ cabal install -f +optimise-heavily -f +enable-cluster-counting

  3. 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.2 or the master branch of the
standard library with Agda 2.6.4. This branch is available at

    https://github.com/agda/agda-stdlib/

Fixed issues over Agda 2.6.3

Changelog for Agda-2.6.4 | Hackage

Enjoy Agda!

18 Likes
#2

@andreasabel what’s the best introductory material for Agda?

4 Likes
#3

Wadlers : Programming Language Foundations in Agda?

3 Likes
#4

The problem I run inti immediately is the standard library. It is all so abstract and I haven’t found an easy way to search it.

All the Agda learning materials I’ve seen, including that one, introduces each concept from scratch without explaining how to use the existing abstractions from the standard library.

5 Likes
#5

I think that Part 1 of Wadler’s Programming Language Foundations in Agda is an excellent introduction to Agda when combined with general overviews of natural deduction, e.g. Wadler’s Proofs are Programs.

However, Part 2 and later of Wadler’s book are somewhat specific to lambda calculi and not as interesting to “general Haskellers”. For that, I think that Aaron Stumps’ book Verified Functional Programming in Agda covers more relevant material.

Finally, the material (documentation, tutorials, examples, …) accompanying Agda2hs is probably the most relevant for Haskellers.

9 Likes
#6

So is optmise-heavily recommended now for production builds/usage?
How much impact does it have for build-time and runtime?
(edit: I see it induces ghc-options: -fexpose-all-unfoldings -fspecialise-aggressively)

I am wondering if I should turn it on for Fedora builds…