[Agda] [ANNOUNCE] Agda 2.6.3 release candidate 1

Andrés Sicard-Ramírez andres.sicard.ramirez at gmail.com
Sun Nov 6 18:27:05 CET 2022

Dear all,

The Agda Team is very pleased to announce the first 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 and
  JavaScript backends, 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

# GHC supported versions

Agda 2.6.3 RC1 has been tested with GHC 9.2.4, 9.2.2, 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 RC1 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 the `release-v1.7.2` branch of the
standard library with Agda 2.6.3 RC1. This branch is available at


# Fixed issues


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


Andrés, on behalf of the Agda Team

More information about the Agda mailing list