[Agda] [ANNOUNCE] Agda 2.6.2 release candidate

Andrés Sicard-Ramírez asr at eafit.edu.co
Tue May 25 17:40:04 CEST 2021


Dear all,

The Agda Team is very pleased to announce a release candidate of Agda
2.6.2. We plan to release 2.6.2 in a few days.

# Highlights

* Several improvements and bug-fixes related to Run-time Irrelevance (
https://agda.readthedocs.io/en/latest/language/runtime-irrelevance.html).

* Several improvements and bug-fixes related to the JavaScript Backend (
https://agda.readthedocs.io/en/latest/tools/compilers.html#javascript-backend
).

* Added experimental support for Guarded Cubical Agda (
https://agda.readthedocs.io/en/latest/language/guarded-cubical.html).

* The Primitive Sorts (
https://agda.readthedocs.io/en/latest/language/built-ins.html#sorts) of
Agda (`Set` and `Prop`) are no longer keywords and can be renamed when
importing `Agda.Primitive`.

* Added native support for the Inspect Idiom (
https://agda.readthedocs.io/en/latest/language/with-abstraction.html#with-abstraction-equality
).

* Added support for making System Calls (
https://agda.readthedocs.io/en/latest/language/reflection.html#system-calls)
from the reflection API.

# GHC supported versions

Agda 2.6.2 RC has been tested with GHC 9.0.1, 8.10.4, 8.8.4, 8.6.5, 8.4.4,
8.2.2 and 8.0.2 on Linux, macOS and Windows.

# Installation

Agda 2.6.2 RC can be installed using cabal-install or stack:

* Getting the release candidate

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

* 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

For the time being, you can use the *experimental* branch of the standard
library with Agda 2.6.2 RC. This branch is available at

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

# Fixed issues


http://hackage.haskell.org/package/Agda-2.6.1.3.20210524/candidate/changelog


Enjoy Agda 2.6.2 RC and please test as much as possible.


-- 

Andrés, on behalf of the Agda Team
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210525/bf9b7da0/attachment.html>


More information about the Agda mailing list