[Agda] [ANNOUNCE] Agda 2.6.3

[Andrés Sicard-Ramírez]

Dear all,

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

# Highlights

* Added support for [Erased Cubical
  Agda](https://agda.readthedocs.io/en/v2.6.3/language/cubical.html#cubical-agda-with-erased-glue),
  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
  Agda](https://agda.readthedocs.io/en/v2.6.3/language/cubical.html#indexed-inductive-types),
  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.

  Note that code that uses (only) `--without-K` can no longer be
  imported from code that uses `--cubical`. Thus it may make sense to
  replace `--without-K` with `--cubical-compatible` in library code,
  if possible.

  Note also that Agda tends to be quite a bit faster if `--without-K`
  is used instead of `--cubical-compatible`.

* Agda 2.6.3 seems to type-check one variant of the standard library
  about [30%  faster](https://github.com/agda/agda/issues/6049#issuecomment-1329163727)
  than Agda 2.6.2.2 (on one system; the library was changed in a small
  way between the tests to accommodate changes to Agda). In that test
  the standard library did not use the new flag
  `--cubical-compatible`. With that flag enabled in all the files that
  used to use `--without-K` (and the warning `UnsupportedIndexedMatch`
  turned off) Agda 2.6.3 was still about 10% faster.

* New primitives `declareData`, `defineData`, and `unquoteDecl data`
  for generating new data types have been added to the [reflection
API](https://agda.readthedocs.io/en/v2.6.3/language/reflection.html#metaprogramming).

# GHC supported versions

Agda 2.6.3 has been tested with GHC 9.4.4, 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

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

# 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.

# Fixed issues

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


Enjoy Agda 2.6.3.

-- 
Andrés, on behalf of the Agda Team