[Agda] [ANNOUNCE] Agda 2.6.4 release candidate 3

Andreas Abel abela at chalmers.se
Sat Sep 30 18:25:16 CEST 2023


Dear all,

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

Thanks to everyone who gave us feedback on the previous release 
candidates!  Changes in RC3 over RC2 are summarized at:

    https://github.com/agda/agda/pull/6893


# Highlights of Agda 2.6.4

* 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.4 RC2 has been tested with GHC 9.6.2, 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 RC2 can be installed using cabal-install or stack:

1. Getting the release candidate

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

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

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

# Fixed issues over Agda 2.6.3

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


Enjoy Agda 2.6.4 RC3 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
_______________________________________________
Agda mailing list
Agda at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda

-- 
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