[Agda] [ANNOUNCE] Agda 2.6.0 release candidate 2
Andres Sicard Ramirez
asr at eafit.edu.co
Mon Apr 1 00:19:32 CEST 2019
Dear all,
The Agda Team is very pleased to announce the second release candidate
of Agda 2.6.0.
Installation
=======
This RC can be installed using the following instructions:
$ cabal install
https://hackage.haskell.org/package/Agda-2.5.4.2.20190330/candidate/Agda-2.5.4.2.20190330.tar.gz
or
$ cabal get https://hackage.haskell.org/package/Agda-2.5.4.2.20190330/candidate/Agda-2.5.4.2.20190330.tar.gz
$ cd Agda-2.5.4.2.20190330
$ cabal install
GHC supported versions
===============
This RC has been tested with GHC 8.6.4, 8.4.4, 8.2.2, 8.0.2 and 7.10.3
on Linux, macOS and Windows.
Note that this RC cannot be installed on Windows using GHC 8.6.3 due
to a GHC bug.
Standard library
==========
For the time being, you can use the *experimental* branch of the
standard library which is compatible with this RC. This branch of the
standard library is available at
https://github.com/agda/agda-stdlib/
Highlights
======
* Added support for Cubical Agda
(https://agda.readthedocs.io/en/latest/language/cubical.html) which
adds new features such as univalence and higher inductive
types to Agda.
* Added support for ML-style automatic generalization of variables
(https://agda.readthedocs.io/en/latest/language/generalization-of-declared-variables.html).
* Added a new sort `Prop` of definitionally proof-irrelevant
propositions (https://agda.readthedocs.io/en/latest/language/prop.html).
* The implementation of instance search
(https://agda.readthedocs.io/en/latest/language/instance-arguments.html)
got a major overhaul and no longer supports overlapping instances
(unless enabled by a flag).
Complete list of changes and fixed issues
=========================
http://hackage.haskell.org/package/Agda-2.5.4.2.20190330/candidate/changelog
Enjoy the RC and please test as much as possible.
--
Andrés on behalf of the Agda Team
More information about the Agda
mailing list