[Agda] [ANNOUNCE] Agda 2.6.3 release candidate 3

[Andrés Sicard-Ramírez]

Dear all,

The Agda Team is very pleased to announce the third 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/v2.6.2.2.20230105/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.2.2.20230105/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.2.2.20230105/language/reflection.html#metaprogramming).

# Changes respect to RC2

We fixed the following issues:
[#3660](https://github.com/agda/agda/issues/3660)
[#6377](https://github.com/agda/agda/issues/6377)
[#6379](https://github.com/agda/agda/issues/6379)

# GHC supported versions

Agda 2.6.3 RC3 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

Agda 2.6.3 RC3 can be installed using cabal-install or stack:

* Getting the release candidate

    $ cabal get
https://hackage.haskell.org/package/Agda-2.6.2.2.20230105/candidate/Agda-2.6.2.2.20230105.tar.gz
    $ cd Agda-2.6.2.2.20230105

* 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 RC3.

# Fixed issues

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


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

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