[Agda] [ANNOUNCE] Agda 2.6.4 release candidate 2

mechvel at scico.botik.ru mechvel at scico.botik.ru
Thu Sep 14 23:54:13 CEST 2023


I have tested this  2.6.4-RC2
on my large library for computer algebra under MAlonzo, ghc-9.2.7,
Linux (Debian and Ubuntu 18.04).

Its work at the whole example does not show any difference to  RC1.

(Though, the are many tools in Agda which I did not try or failed to 
use:
for example, instances, --erasure, opaque definitions, `inspect', 
`rewrite',  `cubical').

------
Sergei


On 2023-09-14 09:40, Andreas Abel wrote:
> Dear all,
> 
> The Agda Team is very pleased to announce the second release candidate
> of Agda 2.6.4.
> 
> A big thank-you to everyone who gave us feedback on the first release
> candidate!  Changes in RC2 over RC1 are summarized at:
> 
>   https://github.com/agda/agda/pull/6849
> 
> 
> # 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.3 RC2 has been tested with GHC 9.6.2, 9.4.6, 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 RC2 can be installed using cabal-install or stack:
> 
> * Getting the release candidate
> 
>      $ cabal get
> https://hackage.haskell.org/package/Agda-2.6.3.20230914/candidate/Agda-2.6.3.20230914.tar.gz
>      $ cd Agda-2.6.3.20230914
> 
> * 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 RC2.  This branch is available at
> 
>      https://github.com/agda/agda-stdlib/
> 
> # Fixed issues
> 
> 
> https://hackage.haskell.org/package/Agda-2.6.3.20230914/candidate/changelog
> 
> 
> Enjoy Agda 2.6.4 RC2 and please test as much as possible.
> Report problems and regressions to: https://github.com/agda/agda/issues


More information about the Agda mailing list