[Agda] [ANNOUNCE] Agda 2.6.3

[Andreas Abel]

Hoooorray!

Thanks Andres, and all of the developers who made it happen!

On 2023-01-30 13:52, Andrés Sicard-Ramírez wrote:
> 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.
>