Release Agda 2.6.1

[asr]

After the release of the first candidate, let's continue the discussion here.

[martinescardo]

Thanks for producing the new version of Agda.

My repository https://github.com/martinescardo/TypeTopology doesn't type check anymore. I haven't had an opportunity to investigate. But running "agda AllModulesIndex.lagda" on "source/" gives

_A_2288 : X → 𝓤 ̇  [ at /home/mhe/feathers/tudo/alive/TypeTopology/source/UF-Yoneda.lagda:584,29-43 ]
Sort _2293  [ at /home/mhe/feathers/tudo/alive/TypeTopology/source/UF-Yoneda.lagda:584,53-54 ]
_2294 : _2293  [ at /home/mhe/feathers/tudo/alive/TypeTopology/source/UF-Yoneda.lagda:584,53-54 ]
_x_2317 : X  [ at /home/mhe/feathers/tudo/alive/TypeTopology/source/UF-Yoneda.lagda:584,67-68 ]
_y_2318 : X  [ at /home/mhe/feathers/tudo/alive/TypeTopology/source/UF-Yoneda.lagda:584,63-64 ]
Sort _2320  [ at /home/mhe/feathers/tudo/alive/TypeTopology/source/UF-Yoneda.lagda:584,51-52 ]
_2321 : _2320  [ at /home/mhe/feathers/tudo/alive/TypeTopology/source/UF-Yoneda.lagda:584,51-52 ]
Sort _2328  [ at /home/mhe/feathers/tudo/alive/TypeTopology/source/UF-Yoneda.lagda:585,53-54 ]
_2329 : _2328  [ at /home/mhe/feathers/tudo/alive/TypeTopology/source/UF-Yoneda.lagda:585,53-54 ]
_x_2347 : X  [ at /home/mhe/feathers/tudo/alive/TypeTopology/source/UF-Yoneda.lagda:585,63-64 ]
_y_2348 : X  [ at /home/mhe/feathers/tudo/alive/TypeTopology/source/UF-Yoneda.lagda:585,63-64 ]
Sort _2355  [ at /home/mhe/feathers/tudo/alive/TypeTopology/source/UF-Yoneda.lagda:585,51-52 ]
_2356 : _2355  [ at /home/mhe/feathers/tudo/alive/TypeTopology/source/UF-Yoneda.lagda:585,51-52 ]

———— Errors ————————————————————————————————————————————————
Failed to solve the following constraints:
  piSort _2355
  (λ x → piSort (_2328 (z = z) (r = r) (x = x)) (λ _ → Set 𝓤))
    = Set 𝓤
  piSort _2320
  (λ x → piSort (_2293 (z = z) (r = r) (x = x)) (λ _ → Set 𝓤))
    = Set 𝓤
  λ x y p q → p ∙ q ∙ refl = λ x y p q → p ∙ (q ∙ refl) : _A_2288 z
  (x : _2356) (y : _2329 (z = z) (r = r) (x = x))
  (p
   : _x_2347 (z = z) (r = r) (x = x) (y = y) ≡
     _y_2348 (z = z) (r = r) (x = x) (y = y))
  (q : _y_2348 (z = z) (r = r) (x = x) (y = y) ≡ z₁) →
  _x_2347 (z = z) (r = r) (x = x) (y = y) ≡ z
    =< _A_2288 z
  (x : _2321) (y : _2294 (z = z) (r = r) (x = x))
  (p
   : _x_2317 (z = z) (r = r) (x = x) (y = y) ≡
     _y_2318 (z = z) (r = r) (x = x) (y = y))
  (q : _y_2318 (z = z) (r = r) (x = x) (y = y) ≡ z₁) →
  _x_2317 (z = z) (r = r) (x = x) (y = y) ≡ z
    =< _A_2288 z
  λ x y p q → p ∙ (q ∙ x₁) = λ x y p q → p ∙ (q ∙ x₁) : _A_2288 t
  λ x y p q → p ∙ q ∙ x₁ = λ x y p q → p ∙ q ∙ x₁ : _A_2288 t
  _A_2288 t = (x y : X) (p : x ≡ y) (q : y ≡ z) → x ≡ t : Set 𝓤

on the module UF-Yoneda. My worst fear, in every release, is that Agda will infer types in a different way...

[martinescardo]

My repository https://github.com/martinescardo/HoTT-UF-Agda-Lecture-Notes works fine with the new version, thankfully.

[martinescardo]

There is only one thing that goes wrong in 37137 lines of code, at UF-Yoneda.lagda line 581.

The code is

ext-assoc : {X : 𝓤 ̇ } {z t : X} (r : z ≡ t)
          → (λ (x y : X) (p : x ≡ y) (q : y ≡ z) → (p ∙ q) ∙ r)
          ≡ (λ (x y : X) (p : x ≡ y) (q : y ≡ z) → p ∙ (q ∙ r))
ext-assoc {𝓤} {X} {z} {t} = yoneda-elem-lc 
                                           (λ z r x y p q → p ∙ q ∙ r)
                                           (λ z r x y p q → p ∙ (q ∙ r))
                                           refl
                                           t

If we supply the implicit arguments as

ext-assoc : {X : 𝓤 ̇ } {z t : X} (r : z ≡ t)
          → (λ (x y : X) (p : x ≡ y) (q : y ≡ z) → (p ∙ q) ∙ r)
          ≡ (λ (x y : X) (p : x ≡ y) (q : y ≡ z) → p ∙ (q ∙ r))
ext-assoc {𝓤} {X} {z} {t} = yoneda-elem-lc {𝓤} {𝓤} {X} {z} {λ - → (x y : X) (p : x ≡ y) (q : y ≡ z) → x ≡ - }
                                           (λ z r x y p q → p ∙ q ∙ r)
                                           (λ z r x y p q → p ∙ (q ∙ r))
                                           refl
                                           t

then the whole repository type checks.

It is the fifth implicit argument {λ - → (x y : X) (p : x ≡ y) (q : y ≡ z) → x ≡ - } that is no longer inferred.

[L-TChen]

I think one way to spot this incompatibility before each release is set up a testing running regularly on GitHub and report the problem once the regression is introduced. I can write a template script for running testing in due course...

[jespercockx]

@martinescardo that looks like it could be an instance of #3960. I've spent quite some time trying to debug that one, but unfortunately all my attempts so far have failed. A small example where Agda 2.6.0.1 can infer all the implicits but the current master doesn't would be really useful.

[martinescardo]

I see. This same error has already been reported there. I will try to shrink the code giving the error.

[martinescardo]

Here is the requested, small, self-contained example:

open import Agda.Primitive public

variable
 ℓ ℓ' : Level

data _≡_ {X : Set ℓ} : X → X → Set ℓ where
  refl : {x : X} → x ≡ x

transport : {X : Set ℓ} (A : X → Set ℓ') {x y : X} → x ≡ y → A x → A y
transport A refl = λ a → a

ap : {X : Set ℓ} {Y : Set ℓ'} (f : X → Y) {x x' : X} → x ≡ x' → f x ≡ f x'
ap f refl = refl

_⁻¹ : {X : Set ℓ} {x y : X} → x ≡ y → y ≡ x
refl ⁻¹ = refl

_∙_ : {X : Set ℓ} {x y z : X} → x ≡ y → y ≡ z → x ≡ z
p ∙ refl = p

infixl 2 _∙_

yoneda-lemma : {X : Set ℓ} (x : X) (A : X → Set ℓ')
               (η : (y : X) → x ≡ y → A y) (y : X) (p : x ≡ y)
             → transport A p (η x refl) ≡ η y p
yoneda-lemma x A η y refl = refl


yoneda-elem-lc : {X : Set ℓ} {x : X} {A : X → Set ℓ'} (η θ : (y : X) → x ≡ y → A y)
               → η x refl ≡ θ x refl → ∀ y p → η y p ≡ θ y p
yoneda-elem-lc {ℓ} {ℓ'} {X} {x} {A} η θ q y p =
 (yoneda-lemma x A η y p)⁻¹ ∙ ap (transport A p) q ∙ yoneda-lemma x A θ y p


ext-assoc : {X : Set ℓ} {z t : X} (r : z ≡ t)
          → (λ (x y : X) (p : x ≡ y) (q : y ≡ z) → (p ∙ q) ∙ r)
          ≡ (λ (x y : X) (p : x ≡ y) (q : y ≡ z) → p ∙ (q ∙ r))
ext-assoc {ℓ} {X} {z} {t} = yoneda-elem-lc
                             -- {ℓ} {ℓ} {X} {z} {λ - → (x y : X) (p : x ≡ y) (q : y ≡ z) → x ≡ - }
                             (λ z r x y p q → (p ∙ q) ∙ r)
                             (λ z r x y p q → p ∙ (q ∙ r))
                             refl
                             t

You need to uncomment the above line to be able to type check this with the release candidate.

[nad]

Compilation seems to require quite a bit more memory, compared to the previous release. I guess it is for this reason that the makefile now (by default) gives the RTS option -M3G to GHC. I worry that this could lead to problems for end users:

ghc: out of memory (requested 1048576 bytes)
cabal: Failed to build Agda-2.6.1. The build process terminated with exit code
251

Can we address this problem in some way? Should we add this RTS option to the Cabal file?

[UlfNorell]

No more open issues for 2.6.1 🎉.

@asr can you prepare a new release candidate?

[asr]

Yes. I'll prepare the second release candidate.

[nad]

Compilation seems to require quite a bit more memory, compared to the previous release. I guess it is for this reason that the makefile now (by default) gives the RTS option -M3G to GHC. I worry that this could lead to problems for end users:

ghc: out of memory (requested 1048576 bytes)
cabal: Failed to build Agda-2.6.1. The build process terminated with exit code
251

Can we address this problem in some way? Should we add this RTS option to the Cabal file?

We could at least document the issue.

[asr]

Should we add this RTS option to the Cabal file?

Was not that RTS option added in the Agda.cabal file by

agda/Agda.cabal

Lines 709 to 713 in 204183c

	-- The threaded RTS by default starts a major GC after a program has
	-- been idle for 0.3 s. This feature turned out to be annoying, so
	-- the idle GC is now by default turned off (-I0).
	ghc-options: -threaded -rtsopts
	"-with-rtsopts=-M3.5G -I0"

?

We could at least document the issue.

Is not the issue documented by

agda/CHANGELOG.md

Lines 27 to 33 in 204183c

	* Agda now uses the default RTS options `-M3.5G -I0`. If
	you run Agda on a 32-bit system or a system with less than 8GB of
	RAM, it is recommended to set the RTS options explicitly to a lower
	value by running `agda` with option `+RTS -M1.2G -RTS`
	(for example) or by setting the GHCRTS enviroment variable. See the
	[GHC User's Guide](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/runtime_control.html#setting-rts-options)
	for more information.

?

[asr]

In the above commit, I updated the list of closed issues in the CHANGELOG. Anything missing or misplaced?

[jespercockx]

Looks good to me.

[asr]

The current master (af74e45) is in good shape for preparing the second the release candidate, so the release-2.6.1 branch is frozen.

[asr]

I uploaded to Hackage the second release candidate Agda-2.6.0.1.20200307 and I tested its installation on Ubuntu with

GHC	cabal-install
8.8.3	3.0.0.0
8.6.5	2.4.1.0
8.4.4	2.2.0.0
8.2.2	2.0.0.1
8.0.2	1.24.0.2

Could someone test the installation on macOS and Windows using the following instructions:

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

[asr]

I wasn't thinking in the release.

[asr]

I started the preparation for the release.

[asr]

I'm getting the error

/.../agda/test/LibSucceed/SizeInconsistentMeta4.agda:45,56-118
Found an implicit application where an explicit application was
expected
when checking that {_≤₂_ = Lex-< _≡_ _<_}
(Lex<-trans PropEq.isEquivalence (PropEq.resp₂ _<_) <-trans) p q
are valid arguments to a function of type
Transitive __<₂__92 →
Transitive Data.Product.Relation.Binary.Lex.Strict._<ₗₑₓ_

when I tried to update the submodule commit of the standard library. I guess the error is due to the changes in commit agda/agda-stdlib@ef78949.

Could someone push a fix into this branch please.

You can reproduce the error on the above branch by running

$ make std-lib-succeed

[asr]

@gallais, thanks for fixing the problem.

[asr]

Compilation seems to require quite a bit more memory, compared to the previous release. I guess it is for this reason that the makefile now (by default) gives the RTS option -M3G to GHC. I worry that this could lead to problems for end users:

ghc: out of memory (requested 1048576 bytes)
cabal: Failed to build Agda-2.6.1. The build process terminated with exit code
251

Can we address this problem in some way? Should we add this RTS option to the Cabal file?

We could at least document the issue.

I agree. Could you document the issue (in the master branch), please.

[nad]

I just saw that @Soares reported long build times: "The Agda dev version has been building on my machine for the last 2h, with no sign of stopping". @Soares, can you identify the problem?

• How did you build Agda?
• Did the machine start swapping?
• Did you give an RTS flag like -M3G to GHC?
• Did you give a flag like -j3 to GHC?

[Soares]

• How did you build Agda?

I installed the prereqs listed here and then ran make install.

After 172 min, the build failed on package ~320 out of ~360 (IIRC), having exhausted the heap. I restarted the build, hoping (correctly) that it saved the first ~320 packages; the build then completed in 5min & succeeded.

• Did the machine start swapping?

I'm not sure. It only took one (of four) CPUs, and that CPU was pegged at 100% for the duration. I had top (well, htop) running, and I expect I would have noticed if memory utilization went through the roof w/out swapping happening anytime in the first 2h (either by noticing it in htop like I noticed the CPU utilization, or by noticing everything else bog down, and I didn't notice either). On the other hand, it eventually failed by exhausting the heap, so there's definitely something up with memory use getting out of hand.

• Did you give an RTS flag like -M3G to GHC?
• Did you give a flag like -j3 to GHC?

Nope, just a vanilla make install :-)

Other facts: machine is a 2019 Thinkpad, so a laptop, but a reasonably meaty one. OS Ubuntu 18-point-something, and I think the Haskell version was just whatever-apt-gives-you but I'm not sure. (Can't be much more specific, sorry; I no longer have access to that machine.)

Reading back through the thread, I'm pretty sure this is the same thing @nad noted in this comment.

[nad]

• Did you give an RTS flag like -M3G to GHC?
• Did you give a flag like -j3 to GHC?

Nope, just a vanilla make install :-)

This includes -M3G. If memory runs out when people use this option, then we should not advocate using it.

After 172 min, the build failed on package ~320 out of ~360 (IIRC)

I'm guessing that this includes time for installing other Haskell packages as well, not just Agda.

[asr]

If memory runs out when people use this option, then we should not advocate using it.

Then I'll prepare the release from the current master.

[asr]

Agda 2.6.1 has been released. Good job everyone!

[jespercockx]

Hooray! Thanks for your hard work!

[asr]

Other facts: machine is a 2019 Thinkpad, so a laptop, but a reasonably meaty one. OS Ubuntu 18-point-something, and I think the Haskell version was just whatever-apt-gives-you but I'm not sure. (Can't be much more specific, sorry; I no longer have access to that machine.)

@Soares, how much memory has the laptop?

[Soares]

@asr 16G mem + 16G swap