[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