[Agda] [ANNOUNCE] Agda 2.5.4 release candidate 2

[Andrés Sicard-Ramírez]

Dear all,

The Agda Team is very pleased to announce the second release candidate
of Agda 2.5.4. We plan to release 2.5.4 in one week.

Fixed issues on this RC
==============

The fixed issues since the first release candidate were:

#2306: Commands in the emacs-mode get confused if we add question
marks to the file
#3004: Agda hangs on extended lambda
#3067: checking hangs on invalid program
#3072: invalid section printing
#3074: Wrong hiding causes internal error in LHS checker
#3075: Automatic inlining and tactics
#3078: Error building with GHC 7.10.2: Missing transformers library
#3079: Wrong parameter hiding for instance open
#3080: Case splitting prints out-of-scope pattern synonyms
#3082: Emacs mode regression: a ? inserted before existing hole
hijacks its interaction point
#3083: Wrong hiding in module application
#3084: Changes to mode line do not take effect immediately
#3085: Postpone checking a pattern let binding when type is blocked

Installation
=======

This RC can be installed using the following instruction:

$ cabal install
https://hackage.haskell.org/package/Agda-2.5.3.20180526/candidate/Agda-2.5.3.20180526.tar.gz

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

This RC has been tested with GHC 7.10.3, 8.0.2, 8.2.2 and 8.4.2 on
Linux, macOS and Windows.

Please note that GHC 8.4.2 requires cabal-install ≥ 2.2.0.0.

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

For the time being, you can use the `experimental` branch of the
standard library which is compatible with
this RC. This branch is available at

https://github.com/agda/agda-stdlib/tree/experimental

What is new, some fixed issues and incompatibilities
================================

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


Enjoy the RC and please test as much as possible.

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

[Sergei Meshveliani]

Post by Andrés Sicard-Ramírez
Dear all,
The Agda Team is very pleased to announce the second release candidate
of Agda 2.5.4. We plan to release 2.5.4 in one week.
[..]
Enjoy the RC and please test as much as possible.

I have ported DoCon-A-2.02 from Agda-2.5.3 to Agda 2.5.3.20180519

(both under MAlonzo, ghc-7.10.2, Debian Linux).

* The obtained DoCon-A-2.02.1 differs only in some paths to Standard
library modules, in changing order of arguments in the gmap standard
function, changing _,_ to _,′_ is a couple of places.

* This porting does not reveal any bug in the candidate Agda (!).

* I tried two tests for running executable. They show that the
candidate produces the executable code that performs about 10% faster
than under Agda-2.5.3.

* I compared time of type-checking/making respectively
DoCon-A-2.02 under Agda-2.5.3 and
DoCon-A-2.02.1 under Agda-2.5.3.20180519.

The type checker of Agda-2.5.3.20180519 is about 30% less space eager
(at this test).
For the restriction of -M15G, the candidate `makes' DoCon-A 15% faster.
The minimal space to type-check DoCon-A is 30% smaller than under
Agda-2.5.3. The candidate Agda needs 10 G byte for this.

I wonder what may be further optimization.

Regards,

------
Sergei

[Sergei Meshveliani]

Post by Andrés Sicard-Ramírez
Dear all,
The Agda Team is very pleased to announce the second release candidate
of Agda 2.5.4. We plan to release 2.5.4 in one week.
[..]
Enjoy the RC and please test as much as possible.

After I installed the candidate, emacs started to change the color
in .agda files to red each time I enter a symbol. To return the color, I
press C-c C-x C-d now and then.

After installing, I applied

Post by Andrés Sicard-Ramírez
agda-mode compile

This installation seems to have a different effect on emacs than
previous ones.

May be you can give a hint about the effect?

Thanks,

------
Sergei

[Nils Anders Danielsson]

Post by Sergei Meshveliani
May be you can give a hint about the effect?

See "Light highlighting is performed dynamically, even if the file is
not loaded" in the changelog.