[Agda] [ANNOUNCE] Agda 2.6.3 release candidate 2

[Andrés Sicard-Ramírez]

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
  Agda](https://agda.readthedocs.io/en/latest/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/latest/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.

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

* Thanks to a number of performance improvements, Agda 2.6.3 is about
  30% faster than Agda 2.6.2.2 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
  [here](https://github.com/agda/agda/issues/6049#issuecomment-1293698980)).

# 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
https://hackage.haskell.org/package/Agda-2.6.2.2.20221128/candidate/Agda-2.6.2.2.20221128.tar.gz
    $ cd Agda-2.6.2.2.20221128

* 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

    https://hackage.haskell.org/package/Agda-2.6.2.2.20221128/candidate/changelog


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


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