[Agda] [ANNOUNCE] Agda 2.6.3 release candidate 2

Andrés Sicard-Ramírez andres.sicard.ramirez at gmail.com
Wed Nov 30 00:26:07 CET 2022

Dear all,

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

# Highlights

* Added support for [Erased Cubical
  a variant of Cubical Agda that is supported by the GHC backend,
  under the flag `--erased-cubical`.

* Added a new flag `--cubical-compatible` to turn on generation of
  Cubical Agda-specific support code (previously this behaviour was
  part of `--without-K`).

  Since `--cubical-compatible` mode implies that functions should work
  with the preliminary support for [indexed inductive types in Cubical
  many pattern matching functions will now emit an
  `UnsupportedIndexedMatch` warning, indicating that the function will
  not compute when applied to transports (from `--cubical` code).

  This warning can be disabled with `-WnoUnsupportedIndexedMatch`, which
  can be used either in an `OPTIONS` pragma or in your `agda-lib` file.
  The latter is recommended if your project is only
  `--cubical-compatible`, or if it is already making extensive use of
  indexed types.

* New primitives `declareData`, `defineData`, and `unquoteDecl data`
  for generating new data types have been added to the [reflection

* Thanks to a number of performance improvements, Agda 2.6.3 is about
  30% faster than Agda at type-checking the standard library
  with the `--without-K` flag, and 10% faster when using with the
  (new) `--cubical-compatible` flag instead (some details can be found

# Changes respect to RC1

We fixed an issue in the tarball related to `agda-mode` and the
following issues were fixed: #5257, #5774, #5868, #6200, #6285, #6337
and #6338.

# GHC supported versions

Agda 2.6.3 RC2 has been tested with GHC 9.4.3, 9.2.5, 9.0.2, 8.10.7,
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.3 RC2 can be installed using cabal-install or stack:

* Getting the release candidate

    $ cabal get
    $ cd Agda-

* 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 standard library v1.7.2 - RC1
(https://github.com/agda/agda-stdlib/archive/v1.7.2-rc1.zip) with Agda
2.6.3 RC2.

# Fixed issues


Enjoy Agda 2.6.3 RC2 and please test as much as possible.

Andrés, on behalf of the Agda Team

More information about the Agda mailing list