[Agda] [ANNOUNCE] Agda 2.6.4 release candidate 3

[mechvel at scico.botik.ru]

I have tested it on my large library for computer algebra
under Agda-2.6.4-RC2, ghc-9.2.7, MAlonzo, Ubuntu Linux 18.04.

It does not show any difference to Agda-2.6.4-RC2.

------
Sergei



On 2023-09-30 19:25, Andreas Abel wrote:
> 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