[Agda] [ANNOUNCE] Agda 2.6.2

Andrés Sicard-Ramírez asr at eafit.edu.co
Sat Jun 19 08:38:41 CEST 2021


Dear all,

The Agda Team is very pleased to announce the release of Agda 2.6.2.

# Highlights

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

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

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

* The Primitive Sorts (
https://agda.readthedocs.io/en/v2.6.2/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/v2.6.2/language/with-abstraction.html#with-abstraction-equality
).

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

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

# Installation

You can install Agda 2.6.2 with Cabal or stack. See
https://agda.readthedocs.io/en/v2.6.2/getting-started/installation.html .

# Standard library

For the time being, you can use the *master* branch of the standard library
with Agda 2.6.2 (https://github.com/agda/agda-stdlib/).

# Fixed issues

    https://hackage.haskell.org/package/Agda-2.6.2/changelog


Enjoy Agda 2.6.2.

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


More information about the Agda mailing list