[Agda] [ANNOUNCE] Agda 2.6.4 release candidate 1

Andreas Abel andreas.abel at ifi.lmu.de
Sat Aug 5 23:22:05 CEST 2023


Dear all,

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

# Highlights

* Cubical Agda now displays boundary conditions in interactive mode
   (PR [#6529](https://github.com/agda/agda/pull/6529)).

* An inconsistency in the treatment of large indices has been fixed
   (Issue [#6654](https://github.com/agda/agda/issues/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.3 RC1 has been tested with GHC 9.6.2, 9.4.5, 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.3 RC1 can be installed using cabal-install or stack:

* Getting the release candidate

     $ cabal get 
https://hackage.haskell.org/package/Agda-2.6.3.20230805/candidate/Agda-2.6.3.20230805.tar.gz
     $ cd Agda-2.6.3.20230805

* Using cabal-install

     $ cabal install

* Using stack

     $ stack --stack-yaml stack-a.b.c.yaml install

replacing `a.b.c` with your version of GHC.

# Standard library

You can use standard library v1.7.2 or the `master` branch of the
standard library with Agda 2.6.4 RC1.  This branch is available at

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

# Fixed issues

 
https://hackage.haskell.org/package/Agda-2.6.3.20230805/candidate/changelog


Enjoy Agda 2.6.4 RC1 and please test as much as possible.
Report problems and regressions to: https://github.com/agda/agda/issues

-- 

Andreas, on behalf of the Agda Team


More information about the Agda mailing list