[Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1

[Andrés Sicard-Ramírez]

Dear all,

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


Installation
=======

This RC can be installed using the following instruction:

$ cabal install
http://hackage.haskell.org/package/Agda-2.5.3.20180519/candidate/Agda-2.5.3.20180519.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/


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

http://hackage.haskell.org/package/Agda-2.5.3.20180519/candidate/changelog



Enjoy the RC and please test as much as possible.

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

[Andrés Sicard-Ramírez]

Post by Andrés Sicard-Ramírez
Dear all,
The Agda Team is very pleased to announce the first release candidate
of Agda 2.5.4. We plan to release 2.5.4 in one week.
Installation
=======
$ cabal install
http://hackage.haskell.org/package/Agda-2.5.3.20180519/candidate/Agda-2.5.3.20180519.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.

the above command under ghc-7.10.2, Debian Linux
leads to an error which report ends with
"... perhaps you need to add `transformers' to build-depends in
your .cabal file."
I have downloaded the archive, and added `transformers' there to
Agda.cabal.
And this seems to help.

Thanks for reporting!

The problem is caused by the following lines in Agda.cabal:

if impl(ghc >= 7.10.3) && impl(ghc < 8.0)
build-depends: transformers == 0.4.2.0

I'll fix it.

[Andrés Sicard-Ramírez]

Post by Andrés Sicard-Ramírez

Post by Andrés Sicard-Ramírez
$ cabal install
http://hackage.haskell.org/package/Agda-2.5.3.20180519/candidate/Agda-2.5.3.20180519.tar.gz

the above command under ghc-7.10.2, Debian Linux
leads to an error which report ends with
"... perhaps you need to add `transformers' to build-depends in
your .cabal file."

if impl(ghc >= 7.10.3) && impl(ghc < 8.0)
build-depends: transformers == 0.4.2.0

The issue was fixed on the `release-2.5.4`, `stable-2.5` and `master` branches.

[Sergei Meshveliani]

Post by Andrés Sicard-Ramírez
Dear all,
The Agda Team is very pleased to announce the first release candidate
of Agda 2.5.4. We plan to release 2.5.4 in one week.

In CHANGELOG.md in

* The `_⊆_` relation has been moved out of the `Membership` modules to
new modules `List.Relation.Sublist.(Setoid/Propositional)`.
Consequently the `mono` proofs that were in
`Membership.Propositional.Properties` have been moved to
`Relation.Sublist.Propositional.Properties`.

the prefix "Data." is needed in some module names.
Maybe there are more such places.

--
SM

[Andrés Sicard-Ramírez]

Post by Sergei Meshveliani

Post by Andrés Sicard-Ramírez
Dear all,
The Agda Team is very pleased to announce the first release candidate
of Agda 2.5.4. We plan to release 2.5.4 in one week.

In CHANGELOG.md in

* The `_⊆_` relation has been moved out of the `Membership` modules to
new modules `List.Relation.Sublist.(Setoid/Propositional)`.
Consequently the `mono` proofs that were in
`Membership.Propositional.Properties` have been moved to
`Relation.Sublist.Propositional.Properties`.

the prefix "Data." is needed in some module names.
Maybe there are more such places.

I filled (on the standard library bug tracker)
https://github.com/agda/agda-stdlib/issues/324 .

[Sergei Meshveliani]

Post by Andrés Sicard-Ramírez
Dear all,
The Agda Team is very pleased to announce the first release candidate
of Agda 2.5.4. We plan to release 2.5.4 in one week.
Installation
=======
$ cabal install
http://hackage.haskell.org/package/Agda-2.5.3.20180519/candidate/Agda-2.5.3.20180519.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/
[]

I am porting Binary-3.1 (see it on the web) to this
Agda-2.5.4-candidate (version 2.5.3.20180519)
under ghc-7.10.2, MAlonzo, Debian Linux.

First, this needs to change
import Data.List.Any.Membership as Membership
-->
import Data.List.Membership.Setoid as Membership

in several files.
Then, everything is type-checked by

Post by Andrés Sicard-Ramírez
agda $agdaLibOpt GCD.agda

Then, `making' the test

Post by Andrés Sicard-Ramírez
agda -c $agdaLibOpt GCDTest.agda

compiles several modules and then, reports

----------------------------------
...
[ 72 of 103] Compiling MAlonzo.Code.Data.Bool.Properties
( MAlonzo/Code/Data/Bool/Properties.hs,
MAlonzo/Code/Data/Bool/Properties.o )
[ 73 of 103] Compiling MAlonzo.Code.Data.List.NonEmpty
( MAlonzo/Code/Data/List/NonEmpty.hs,
MAlonzo/Code/Data/List/NonEmpty.o )
[ 74 of 103] Compiling MAlonzo.Code.Data.Colist
( MAlonzo/Code/Data/Colist.hs, MAlonzo/Code/Data/Colist.o )
Compilation error:

MAlonzo/Code/Data/Colist.hs:295:11:
Couldn't match type ‘MAlonzo.RTE.Inf (T48 xa xA)’ with ‘[xA]’
Expected type: xA
-> MAlonzo.RTE.Infinity xa (T48 xa xA) -> T48 xa xA
Actual type: xA -> [xA] -> [xA]
Relevant bindings include
check60 :: xA -> MAlonzo.RTE.Infinity xa (T48 xa xA) -> T48 xa xA
(bound at MAlonzo/Code/Data/Colist.hs:295:1)
In the expression: (:)
In an equation for ‘check60’: check60 = (:)
-------------------------------------

Regards,

------
Sergei

[Andrés Sicard-Ramírez]

Post by Sergei Meshveliani
I am porting Binary-3.1 (see it on the web)

Where/what is Binary-3.1?

[Nils Anders Danielsson]

Post by Sergei Meshveliani
Couldn't match type ‘MAlonzo.RTE.Inf (T48 xa xA)’ with ‘[xA]’
Expected type: xA
-> MAlonzo.RTE.Infinity xa (T48 xa xA) -> T48 xa xA
Actual type: xA -> [xA] -> [xA]

See the changelog entry that starts with "The GHC backend now compiles
the INFINITY, SHARP and FLAT builtins in a different way".

[Andrés Sicard-Ramírez]

Post by Sergei Meshveliani

Post by Andrés Sicard-Ramírez
agda -c $agdaLibOpt GCDTest.agda

Couldn't match type ‘MAlonzo.RTE.Inf (T48 xa xA)’ with ‘[xA]’
Expected type: xA
-> MAlonzo.RTE.Infinity xa (T48 xa xA) -> T48 xa xA
Actual type: xA -> [xA] -> [xA]
Relevant bindings include
check60 :: xA -> MAlonzo.RTE.Infinity xa (T48 xa xA) -> T48 xa xA
(bound at MAlonzo/Code/Data/Colist.hs:295:1)
In the expression: (:)
In an equation for ‘check60’: check60 = (:)

I have no problem using the *experimental* branch of the standard
library (but I could reproduce the above error using its *master*
branch).

Note that you should use the *experimental* branch of the standard
library with Agda 2.5.4 RC 1.

[Sergei Meshveliani]

Post by Andrés Sicard-Ramírez

Post by Sergei Meshveliani

Post by Andrés Sicard-Ramírez
agda -c $agdaLibOpt GCDTest.agda

Couldn't match type ‘MAlonzo.RTE.Inf (T48 xa xA)’ with ‘[xA]’
Expected type: xA
-> MAlonzo.RTE.Infinity xa (T48 xa xA) -> T48 xa xA
Actual type: xA -> [xA] -> [xA]
Relevant bindings include
check60 :: xA -> MAlonzo.RTE.Infinity xa (T48 xa xA) -> T48 xa xA
(bound at MAlonzo/Code/Data/Colist.hs:295:1)
In the expression: (:)
In an equation for ‘check60’: check60 = (:)

I have no problem using the *experimental* branch of the standard
library (but I could reproduce the above error using its *master*
branch).
Note that you should use the *experimental* branch of the standard
library with Agda 2.5.4 RC 1.

Post by Sergei Meshveliani
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/

I go to
https://github.com/agda/agda-stdlib/

and choose the button "Clone or download", choosing "download".
And it downloads
agda-stdlib-master.zip (483201 byte).

Is this the experimental branch?
I apply

Post by Andrés Sicard-Ramírez
agda -V

Agda version 2.5.3.20180519

Post by Andrés Sicard-Ramírez
unzip agda-stdlib-master.zip
mv <appeared directory> master-may23
cd master-may23
cabal update
cabal install

This seems to work.

I put "/home/mechvel/agda/stLib/master-may23/src"
on the path in $agdaLibOpt and test it by

Post by Andrés Sicard-Ramírez
echo $agdaLibOpt

-i . -i /home/mechvel/agda/stLib/master-may23/src
-i /home/mechvel/agda/UNPrelude/src

Then I apply

Post by Andrés Sicard-Ramírez
agda $agdaLibOpt GCD.agda
agda -c $agdaLibOpt GCDTest.agda

and again, it yieds

MAlonzo/Code/Data/Colist.hs:295:11:
Couldn't match type ‘MAlonzo.RTE.Inf (T48 xa xA)’ with ‘[xA]’
...

??

------
Sergei

[Ulf Norell]

Post by Sergei Meshveliani
I go to
https://github.com/agda/agda-stdlib/
and choose the button "Clone or download", choosing "download".
And it downloads
agda-stdlib-master.zip (483201 byte).
Is this the experimental branch?

No, that's the master branch, which you can tell from the fact that it ends
with `-master`.
There's a drop down on the left side of the main page which says "Branch:
master". Fiddle
with that until it says "Branch: experimental", then try the download again.

/ Ulf

[Sergei Meshveliani]

I see now. Thanks to Andres and Ulf.
Binary-3.1 has been ported.
Now I am going to port DoCon-A-2.02.

------
Sergei

Post by Sergei Meshveliani
I go to
https://github.com/agda/agda-stdlib/
and choose the button "Clone or download", choosing
"download".
And it downloads
agda-stdlib-master.zip (483201 byte).
Is this the experimental branch?
No, that's the master branch, which you can tell from the fact that it
ends with `-master`.
There's a drop down on the left side of the main page which says
"Branch: master". Fiddle
with that until it says "Branch: experimental", then try the download again.
/ Ulf

[Andrés Sicard-Ramírez]

Thank you for testing the release candidate.

Post by Sergei Meshveliani
I see now. Thanks to Andres and Ulf.
Binary-3.1 has been ported.
Now I am going to port DoCon-A-2.02.
------
Sergei

Post by Sergei Meshveliani
I go to
https://github.com/agda/agda-stdlib/
and choose the button "Clone or download", choosing
"download".
And it downloads
agda-stdlib-master.zip (483201 byte).
Is this the experimental branch?
No, that's the master branch, which you can tell from the fact that it
ends with `-master`.
There's a drop down on the left side of the main page which says
"Branch: master". Fiddle
with that until it says "Branch: experimental", then try the download again.
/ Ulf

_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
La información contenida en este correo electrónico está dirigida únicamente a su destinatario y puede contener información confidencial, material privilegiado o información protegida por derecho de autor. Está prohibida cualquier copia, utilización, indebida retención, modificación, difusión, distribución o reproducción total o parcial. Si usted recibe este mensaje por error, por favor contacte al remitente y elimínelo. La información aquí contenida es responsabilidad exclusiva de su remitente por lo tanto la Universidad EAFIT no se hace responsable de lo que el mensaje contenga. The information contained in this email is addressed to its recipient only and may contain confidential information, privileged material or information protected by copyright. Its prohibited any copy, use, improper retention, modification, dissemination, distribution or total or partial reproduction. If you receive this message by error, please contact the sender and delete it. The information contained herein is the sole responsibility of the sender therefore Universidad EAFIT is not responsible for what the message contains.

[Sergei Meshveliani]

Post by Andrés Sicard-Ramírez
Dear all,
The Agda Team is very pleased to announce the first 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.

On

-------------------------------------------------
open import Data.Product using (_×_; _,_)
open import Data.List using (List; map)
open import Data.Nat using (ℕ; suc)

f : List (ℕ × ℕ) → List (ℕ × ℕ)
f ps =
map (\p → let (x , y) = p in (x , suc y)) ps
--------------------------------------------------


Agda 2.5.3.20180519 reports

/home/mechvel/agda/tosave/bugs/T.agda:7,21-26
Cannot split on argument of non-datatype _A_10 ps
when checking that the pattern x , y has type _A_10 ps

Is this a bug in Agda?

------
Sergei

[Ulf Norell]

This is a deliberate change to the type checker. See the second bullet point
in the changelog here:

https://github.com/agda/agda/blob/release-2.5.4/CHANGELOG.md#pattern-matching

and the corresponding issue

https://github.com/agda/agda/issues/2834

In your case the fix is to add a type signature to p (warning, untested
code):

map (\ (p : _ × _) → let (x , y) = p in (x , suc y)) ps

/ Ulf

Post by Sergei Meshveliani

Post by Andrés Sicard-Ramírez
Dear all,
The Agda Team is very pleased to announce the first 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.

On
-------------------------------------------------
open import Data.Product using (_×_; _,_)
open import Data.List using (List; map)
open import Data.Nat using (ℕ; suc)
f : List (ℕ × ℕ) → List (ℕ × ℕ)
f ps =
map (\p → let (x , y) = p in (x , suc y)) ps
--------------------------------------------------
Agda 2.5.3.20180519 reports
/home/mechvel/agda/tosave/bugs/T.agda:7,21-26
Cannot split on argument of non-datatype _A_10 ps
when checking that the pattern x , y has type _A_10 ps
Is this a bug in Agda?
------
Sergei
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Sergei Meshveliani]

Post by Ulf Norell
This is a deliberate change to the type checker. See the second bullet point
https://github.com/agda/agda/blob/release-2.5.4/CHANGELOG.md#pattern-matching
and the corresponding issue
https://github.com/agda/agda/issues/2834
In your case the fix is to add a type signature to p (warning,
map (\ (p : _ × _) → let (x , y) = p in (x , suc y)) ps

Thank you.
And I find that
map (uncurry (\x y → (x , suc y))) ps

also works.

------
Sergei

Post by Ulf Norell
On Fri, May 25, 2018 at 12:56 PM, Sergei Meshveliani

Post by Andrés Sicard-Ramírez
Dear all,
The Agda Team is very pleased to announce the first release

candidate

Post by Andrés Sicard-Ramírez
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.

On
-------------------------------------------------
open import Data.Product using (_×_; _,_)
open import Data.List using (List; map)
open import Data.Nat using (ℕ; suc)
f : List (ℕ × ℕ) → List (ℕ × ℕ)
f ps =
map (\p → let (x , y) = p in (x , suc y)) ps
--------------------------------------------------
Agda 2.5.3.20180519 reports
/home/mechvel/agda/tosave/bugs/T.agda:7,21-26
Cannot split on argument of non-datatype _A_10 ps
when checking that the pattern x , y has type _A_10 ps
Is this a bug in Agda?
------
Sergei
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Nils Anders Danielsson]

Post by Ulf Norell
This is a deliberate change to the type checker. See the second bullet point
https://github.com/agda/agda/blob/release-2.5.4/CHANGELOG.md#pattern-matching
and the corresponding issue
https://github.com/agda/agda/issues/2834
map (\ (p : _ × _) → let (x , y) = p in (x , suc y)) ps

Issue #2834 is related to disambiguation of types based on patterns. In
this case, given that ps is known to be a list of pairs, it should be
possible for Agda to figure out what the type of p is without a type
annotation. I guess the problem is that Agda checks the pattern eagerly,
rather than waiting until the meta-variable ("_A_10") has been resolved.

[Jesper Cockx]

I guess we should postpone checking a pattern let when the type is blocked
on a meta, like we already do for pattern lambdas and top-level pattern
matching definitions. I filed an issue here:
https://github.com/agda/agda/issues/3085

-- Jesper

Post by Nils Anders Danielsson

Post by Ulf Norell
This is a deliberate change to the type checker. See the second bullet point
https://github.com/agda/agda/blob/release-2.5.4/CHANGELOG.md
#pattern-matching
and the corresponding issue
https://github.com/agda/agda/issues/2834
map (\ (p : _ × _) → let (x , y) = p in (x , suc y)) ps

Issue #2834 is related to disambiguation of types based on patterns. In
this case, given that ps is known to be a list of pairs, it should be
possible for Agda to figure out what the type of p is without a type
annotation. I guess the problem is that Agda checks the pattern eagerly,
rather than waiting until the meta-variable ("_A_10") has been resolved.
--
/NAD
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Sergei Meshveliani]

Post by Andrés Sicard-Ramírez
Dear all,
The Agda Team is very pleased to announce the first 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.

Please, consider a small code attached.
This is a lemma about mapping the _⊆_ relation for lists over setoids:

map⊆ : (f : C → C') → (f Preserves _≈_ ⟶ _≈'_) →
(map f) Preserves _⊆_ ⟶ _⊆'_

In DoCon-A-2.02 (see there List.L0.agda) a similar code works under
Agda-2.5.3.

To port to Agda 2.5.3.20180519, I change the import for the experimental
Standard library:

import Data.List.Membership.Setoid as Membership
import Data.List.Relation.Sublist.Setoid as Sublist-Setoid
import Data.List.Relation.Sublist.Propositional as Sublist-≡

And change the local import in module CongMap0 to

open Membership A using (_∈_)
open Sublist-Setoid A using (_⊆_)
open Membership A' using () renaming (_∈_ to _∈'_)
open Sublist-≡ {A = C'} using () renaming (_⊆_ to _⊆'_) -- *


Now, everything is type-checked there -- except this last function

map⊆ : (f : C → C') → (f Preserves _≈_ ⟶ _≈'_) →
(map f) Preserves _⊆_ ⟶ _⊆'_
map⊆ f fCong {xs} {ys} xs⊆ys {z} z∈f-xs =
let
(x , x∈≡xs , fx≈z) = counter-map {A = C} {sd = A'} f z∈f-xs
x∈xs = ∈≡→∈ x∈≡xs
x∈ys = xs⊆ys x∈xs
fx∈f-ys = map∈ f fCong x∈ys
in
cong₁∈' fx≈z fx∈f-ys

The report is
β != β= of type Level
when checking that the expression z∈f-xs has type
_y_249 A A' f fCong xs⊆ys z∈f-xs ∈'
map f (_xs_248 A A' f fCong xs⊆ys z∈f-xs)

I wonder whether
* this is a bug in the candidate Agda
* or an error in List.L0.agda (missed by Agda 2.5.3)
* or a wrong port.

Can you, please, help?

------
Sergei

[Sergei Meshveliani]

I am sorry, please, withdraw this report.

When porting to Standard library, I have confused the parametric module
import. It needs to be

open Sublist-Setoid A' using () renaming (_⊆_ to _⊆'_)

instead of
open Sublist-≡ {A = C'} using () renaming (_⊆_ to _⊆'_)

------
Sergei

Post by Sergei Meshveliani

Post by Andrés Sicard-Ramírez
Dear all,
The Agda Team is very pleased to announce the first 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.

Please, consider a small code attached.
map⊆ : (f : C → C') → (f Preserves _≈_ ⟶ _≈'_) →
(map f) Preserves _⊆_ ⟶ _⊆'_
In DoCon-A-2.02 (see there List.L0.agda) a similar code works under
Agda-2.5.3.
To port to Agda 2.5.3.20180519, I change the import for the experimental
import Data.List.Membership.Setoid as Membership
import Data.List.Relation.Sublist.Setoid as Sublist-Setoid
import Data.List.Relation.Sublist.Propositional as Sublist-≡
And change the local import in module CongMap0 to
open Membership A using (_∈_)
open Sublist-Setoid A using (_⊆_)
open Membership A' using () renaming (_∈_ to _∈'_)
open Sublist-≡ {A = C'} using () renaming (_⊆_ to _⊆'_) -- *
Now, everything is type-checked there -- except this last function
map⊆ : (f : C → C') → (f Preserves _≈_ ⟶ _≈'_) →
(map f) Preserves _⊆_ ⟶ _⊆'_
map⊆ f fCong {xs} {ys} xs⊆ys {z} z∈f-xs =
let
(x , x∈≡xs , fx≈z) = counter-map {A = C} {sd = A'} f z∈f-xs
x∈xs = ∈≡→∈ x∈≡xs
x∈ys = xs⊆ys x∈xs
fx∈f-ys = map∈ f fCong x∈ys
in
cong₁∈' fx≈z fx∈f-ys
The report is
β != β= of type Level
when checking that the expression z∈f-xs has type
_y_249 A A' f fCong xs⊆ys z∈f-xs ∈'
map f (_xs_248 A A' f fCong xs⊆ys z∈f-xs)
I wonder whether
* this is a bug in the candidate Agda
* or an error in List.L0.agda (missed by Agda 2.5.3)
* or a wrong port.
Can you, please, help?
------
Sergei
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Sergei Meshveliani]

Post by Andrés Sicard-Ramírez
Dear all,
The Agda Team is very pleased to announce the first release candidate
of Agda 2.5.4. We plan to release 2.5.4 in one week.

Can you please delay it a bit?
For I have ported only about 1/10 of DoCon-A-2.02.

Changelog says

Post by Andrés Sicard-Ramírez
* Call-by-need reduction.
Compile-time weak-head evaluation is now call-by-need, but each
weak-head reduction has a local heap, so sharing is not maintained
between different reductions.
The reduction machine has been rewritten from scratch and should be
faster than the old one in all cases, even those not exploiting
laziness.

So that there are likely bugs to reveal during this porting.
It is strange that I do not meet them, so far.

By the way, do the above "compile-time", "reduction machine", and
"call-by-need" refer to the type check stage?

------
Sergei

[Ulf Norell]

Post by Sergei Meshveliani
By the way, do the above "compile-time", "reduction machine", and
"call-by-need" refer to the type check stage?

Yes.

/ Ulf

[Andrés Sicard-Ramírez]

Post by Sergei Meshveliani

Post by Andrés Sicard-Ramírez
The Agda Team is very pleased to announce the first release candidate
of Agda 2.5.4. We plan to release 2.5.4 in one week.

Can you please delay it a bit?

We have decided not to release Agda 2.5.4 this week but next week.

[Arseniy Alekseyev]

I tried the RC on my Primes <https://github.com/Rotsor/Primes> repo and the
new version is much more memory-hungry (I want to say ~2x) and slightly
slower (~60 seconds instead of 53) compared to Agda 2.5.3.

It's totally unimportant to have this specific thing work well, but I
thought people might find the slowdown surprising.

Post by Andrés Sicard-Ramírez

Post by Sergei Meshveliani

Post by Andrés Sicard-Ramírez
The Agda Team is very pleased to announce the first release candidate
of Agda 2.5.4. We plan to release 2.5.4 in one week.

Can you please delay it a bit?

We have decided not to release Agda 2.5.4 this week but next week.
--
Andrés
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Ulf Norell]

I'm not sure what made the memory usage spike in 2.5.4, but I've made a
pull request [1] fixing the problem in your code.
Om my machine it now checks in 7s instead of 45s.

/ Ulf

[1] https://github.com/Rotsor/Primes/pull/1

On Sat, May 26, 2018 at 5:19 AM, Arseniy Alekseyev <

Post by Arseniy Alekseyev
I tried the RC on my Primes <https://github.com/Rotsor/Primes> repo and
the new version is much more memory-hungry (I want to say ~2x) and slightly
slower (~60 seconds instead of 53) compared to Agda 2.5.3.
It's totally unimportant to have this specific thing work well, but I
thought people might find the slowdown surprising.

Post by Andrés Sicard-Ramírez

Post by Sergei Meshveliani

Post by Andrés Sicard-Ramírez
The Agda Team is very pleased to announce the first release candidate
of Agda 2.5.4. We plan to release 2.5.4 in one week.

Can you please delay it a bit?

We have decided not to release Agda 2.5.4 this week but next week.
--
Andrés
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Arseniy Alekseyev]

Ah, thank you!
FYI, I tried upgrading BinDivMod <https://github.com/Rotsor/BinDivMod> (I
used RC2) and that becomes ~2x faster (but still ~1.5x more memory-hungry)
with RC2 compared to 2.5.3.

Post by Ulf Norell
I'm not sure what made the memory usage spike in 2.5.4, but I've made a
pull request [1] fixing the problem in your code.
Om my machine it now checks in 7s instead of 45s.
/ Ulf
[1] https://github.com/Rotsor/Primes/pull/1
On Sat, May 26, 2018 at 5:19 AM, Arseniy Alekseyev <

Post by Arseniy Alekseyev
I tried the RC on my Primes <https://github.com/Rotsor/Primes> repo and
the new version is much more memory-hungry (I want to say ~2x) and slightly
slower (~60 seconds instead of 53) compared to Agda 2.5.3.
It's totally unimportant to have this specific thing work well, but I
thought people might find the slowdown surprising.

Post by Andrés Sicard-Ramírez

Post by Sergei Meshveliani

Post by Andrés Sicard-Ramírez
The Agda Team is very pleased to announce the first release candidate
of Agda 2.5.4. We plan to release 2.5.4 in one week.

Can you please delay it a bit?

We have decided not to release Agda 2.5.4 this week but next week.
--
Andrés
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda