[Agda] [ANNOUNCE] Agda 2.5.1 release candidate 2

Andrés Sicard-Ramírez asr at eafit.edu.co
Wed Apr 13 17:34:16 CEST 2016


Dear all,

The Agda Team is very pleased to announce the second release candidate
(RC 2) of Agda 2.5.1 available at

  http://www1.eafit.edu.co/asr/tmp/Agda-2.5.0.20160412.tar.gz


GHC supported versions
======================

The RC 2 has been tested with GHC 7.6.3, 7.8.4 and 7.10.3.


Installation
============

The RC 2 can be installed using the following instructions:

  $ tar xzf Agda-2.5.0.20160214.tar.gz
  $ cd Agda-2.5.0.20160214.tar.gz
  $ cabal install


Standard library
================

The version of the standard library compatible with the RC 2 is
available at

  https://github.com/agda/agda-stdlib/releases/tag/2.5.0.20160412


What is new?
============

The RC 2 includes various new features and changes:

* Allow version suffix on libraries file. [Issue 1693]

* Emacs mode. Module contents (C-c C-o) now also works for
  records. [Issue 1926]

* New pragma HASKELL for adding inline Haskell code (GHC backend only)

More information about the changes included in the RC 2 can be found
in

  https://raw.githubusercontent.com/agda/agda/2.5.0.20160412/CHANGELOG


Incompatibilities
=================

The RC 2 is not full compatible with the Agda 2.5.1 RC 1 nor Agda
2.4.2.5. The main incompatibilities are:

* Builtins and primitives are now defined in a new set of modules
  available to all users, independent of any particular library. The
  standard library reexports the primitives from the new modules.

  The Agda.Builtin modules are installed in the same way as Agda.Primitive,
  but unlike Agda.Primitive they are not loaded automatically.

* The aggressive behaviour of `with` introduced in 2.4.2.5 has been
  rolled back [Issue 1692]. With no longer abstracts in the types of
  variables appearing in the with-expressions. [Issue 745]

* Record modules now properly hide all their parameters. [Issue 1759]

* Removed --no-coverage-check option. [Issue 1918]

More information about the incompatibilities included in the RC 2 can
be found in the above CHANGELOG.


Fixed issues after Agda 2.5.1 RC 1
==================================

Approximately 40 bugs/regressions were fixed, some of them
long-standing ones:

* https://github.com/agda/agda/issues/140

* https://github.com/agda/agda/issues/610

* https://github.com/agda/agda/issues/745

* https://github.com/agda/agda/issues/994


Know regressions
================

* https://github.com/agda/agda/issues/1775

* https://github.com/agda/agda/issues/1821


Enjoy Agda 2.5.1 release candidate 2 and please test as much as
possible.


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


More information about the Agda mailing list