[Agda] [ANNOUNCE] Agda 2.5.4.2

[Andres Sicard Ramirez]

Dear all,

The Agda Team is very pleased to announce the release of Agda 2.5.4.2.

In this bug-fix release, we fixed a regression in Agda 2.5.4 related
to slow type-checking with unsolved instance constraint (this fix
wasn't included in the CHANGELOG by mistake, so see
https://github.com/agda/agda/issues/3177 ) and we fixed a regression
in Agda 2.5.4.1 related to the installation with some old versions of
`cabal-install`. See the details and other changes in

https://hackage.haskell.org/package/Agda-2.5.4.2/changelog

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

Agda 2.5.4.2 has been tested with GHC 7.10.3, 8.0.2, 8.2.2 and 8.4.4.

Note that GHC 8.4.* requires cabal-install ≥ 2.2.0.0.

Installation
=======

cabal update && cabal install Agda

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

The standard library 0.17 is compatible with Agda 2.5.4.2.


Enjoy Agda 2.5.4.2.
--
Andrés on behalf of the Agda Team

[Sergei Meshveliani]

Post by Andres Sicard Ramirez
Dear all,
The Agda Team is very pleased to announce the release of Agda 2.5.4.2.
In this bug-fix release, we fixed a regression in Agda 2.5.4 related
to slow type-checking with unsolved instance constraint (this fix
wasn't included in the CHANGELOG by mistake, so see
https://github.com/agda/agda/issues/3177 ) and we fixed a regression
in Agda 2.5.4.1 related to the installation with some old versions of
`cabal-install`. See the details and other changes in
https://hackage.haskell.org/package/Agda-2.5.4.2/changelog
[..]

1. What is, briefly, its relation to the Development version of
September 6, 2018 ?

2.
Also I have a certain application tested under Agda-2.5.3 + lib-0.16,
and I try to port it to Agda-2.5.4.2 + lib-0.17.
This occurs difficult.

For example, it imported _≟_ for Char by

open import Data.Char as Char using (Char) renaming (_≟_ to _≟c_)

Now, I am somehow forced to write
open import Data.Char as Char using (Char)
...
open StrictTotalOrder Char.strictTotalOrder using ()
renaming (_≟_ to _≟c_)

Still this _≟c_ does not work as earlier. The code

delimiters = ' ' ∷ ',' ∷ ';' ...

delimiter? : Decidable (_∈ delimiters)
delimiter? c = any (c ≟c_) delimiters

is not type-checked any more. The report is

ℕ != Char of type Set
when checking that the expression any (c ≟c_) delimiters has type
Relation.Nullary.Dec (c ∈ delimiters)

Has _≟_ changed its definition for Char ?

Thanks,

------
Sergei

[Matthew Daggitt]

Hi Sergei,
This is a change to the standard library. If you read the CHANGELOG for
v0.17 you will see that decidable equality has been moved to
`Data.Char.Unsafe`. It also explains the reasons for doing so.
Best,
Matthew

Post by Sergei Meshveliani

Post by Andres Sicard Ramirez
Dear all,
The Agda Team is very pleased to announce the release of Agda 2.5.4.2.
In this bug-fix release, we fixed a regression in Agda 2.5.4 related
to slow type-checking with unsolved instance constraint (this fix
wasn't included in the CHANGELOG by mistake, so see
https://github.com/agda/agda/issues/3177 ) and we fixed a regression
in Agda 2.5.4.1 related to the installation with some old versions of
`cabal-install`. See the details and other changes in
https://hackage.haskell.org/package/Agda-2.5.4.2/changelog
[..]

1. What is, briefly, its relation to the Development version of
September 6, 2018 ?
2.
Also I have a certain application tested under Agda-2.5.3 + lib-0.16,
and I try to port it to Agda-2.5.4.2 + lib-0.17.
This occurs difficult.
For example, it imported _≟_ for Char by
open import Data.Char as Char using (Char) renaming (_≟_ to _≟c_)
Now, I am somehow forced to write
open import Data.Char as Char using (Char)
...
open StrictTotalOrder Char.strictTotalOrder using ()
renaming (_≟_ to _≟c_)
Still this _≟c_ does not work as earlier. The code
delimiters = ' ' ∷ ',' ∷ ';' ...
delimiter? : Decidable (_∈ delimiters)
delimiter? c = any (c ≟c_) delimiters
is not type-checked any more. The report is
ℕ != Char of type Set
when checking that the expression any (c ≟c_) delimiters has type
Relation.Nullary.Dec (c ∈ delimiters)
Has _≟_ changed its definition for Char ?
Thanks,
------
Sergei
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Andres Sicard Ramirez]

Post by Sergei Meshveliani
1. What is, briefly, its relation to the Development version of
September 6, 2018 ?

The main changes in the upstream version *are being* documented as
"Release notes for Agda version 2.6.0" in

https://github.com/agda/agda/blob/0776b8813731d6593626bc908ddc247ea5a66c08/CHANGELOG.md

Best,

--
Andrés