[WIP] Add support for Agda 2.5.4

[timjb]

This addresses #42

[timjb]

When I run

$ env TRAVIS_BUILD_DIR=/home/Projects/HoTT-Agda agda --library-file=travis-script/libraries --without-K --rewriting theorems/index1.agda

I get the following error:

[...]
  Checking cohomology.SpectrumModel (/home/Projects/HoTT-Agda/theorems/cohomology/SpectrumModel.agda).
   Checking groups.SuspAdjointLoop (/home/Projects/HoTT-Agda/theorems/groups/SuspAdjointLoop.agda).
    Checking groups.FromSusp (/home/Projects/HoTT-Agda/theorems/groups/FromSusp.agda).
An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/InstanceArguments.hs:292

(Here's the line mentioned in the error message.)

I will report this to the Agda people.

[timjb]

The/One problematic definition is

    abstract
      C-additive-is-equiv : is-equiv (GroupHom.f (Πᴳ-fanout (C-fmap n ∘ ⊙bwin {X = X})))
      C-additive-is-equiv = transport is-equiv
        (λ= $ Trunc-elim
          (λ _ → idp))
        ((ac (uCEl n ∘ X)) ∘ise (is-eq into out into-out out-into))

in cohomology.SpectrumModel.

[timjb]

The commit above solves this issue by giving two implicit arguments of transport explicitly instead of letting Agda infer them.

[timjb]

Apart from homotopy.GroupSetsRepresentCovers, which is stubbornly resisting my attempts, all modules typecheck successfully with Agda 2.5.4 now.

[favonia]

@timjb Thanks! By the way, I think f71c7c0 is really a workaround for some strange bug. What do you think?

[timjb]

Also homotopy.3x3.PushoutPushout doesn't check in a reasonable amount of time with 2.5.4 (I've abborted typechecking after the process ran for one hour).

[favonia]

Let me take care of homotopy.3x3.PushoutPushout.

[timjb]

@favonia Yes, it is a workaround for a bug that causes Agda 2.5.4 to not apply available rewriting rules. I don't have any good insight into what the specific circumstances are that make this bug appear, I just followed the general strategy "mark things abstract so Agda doesn't get too confused" and it worked!

[favonia]

Could it be agda/agda#2979 again?

[timjb]

Yes, that's possible

[timjb]

Here's the Agda issue for the internal error in InstanceArguments: agda/agda#3125

[favonia]

Progress report: something needs to be fixed for homotopy.3x3.PushoutPushout! It has been running for more than 10 19 hours and was probably stuck at checking span^2=-raw.

[timjb]

I've tried getting my cup-products branch working with 2.5.4, but there again is a module that seems to get Agda into an infinite loop: More specifically, checking the term in this line and this term both in homotopy.EM1HSpaceAssoc don't terminate (within several minutes). Strangely enough, this line works fine despite being quite similar to the first problematic line.

[favonia]

@timjb Hi, I am back. Agda master branch seems to be fine with the current Pushout definitions (yay), but there are other issues. Let me open up another branch and do some experiments.

[ice1000]

So what's the current progress?

[favonia]

@ice1000 I did not merge this PR yet because I really want to keep the original Pushout definitions, and Agda 2.5.4 is still unhappy about @timjb's development after the changes.

[ice1000]

Can you try Agda 2.5.4.2？

[favonia]

Can you try Agda 2.5.4.2？

@ice1000 The hott-core library works without modification as in 2.6.0. Yay! I am stuck at homotopy.GroupSetsRepresentCovers as @timjb noticed. By the way, please ignore my nonsensical comment "feel-free-to-make-a-PR". I did not realize you are an Agda developer.

[ice1000]

The hott-core library works without modification as in 2.6.0.

~/git-repos/FormalVerification/HoTT-Agda λ> agda --version
Agda version 2.6.0-a40792b
~/git-repos/FormalVerification/HoTT-Agda λ> agda core/HoTT.agda
Checking HoTT (core/HoTT.agda).
 Checking lib.Basics (core/lib/Basics.agda).
  Checking lib.Base (core/lib/Base.agda).
  Checking lib.Equivalence (core/lib/Equivalence.agda).
   Checking lib.NType (core/lib/NType.agda).
    Checking lib.PathGroupoid (core/lib/PathGroupoid.agda).
    Checking lib.Relation (core/lib/Relation.agda).
   Checking lib.PathFunctor (core/lib/PathFunctor.agda).
   Checking lib.Function (core/lib/Function.agda).
  Checking lib.Funext (core/lib/Funext.agda).
   Checking lib.Univalence (core/lib/Univalence.agda).
    Checking lib.PathOver (core/lib/PathOver.agda).
   Checking lib.PathSeq (core/lib/PathSeq.agda).
    Checking lib.path-seq.Ap (core/lib/path-seq/Ap.agda).
     Checking lib.path-seq.Reasoning (core/lib/path-seq/Reasoning.agda).
      Checking lib.path-seq.Concat (core/lib/path-seq/Concat.agda).
      Checking lib.path-seq.Split (core/lib/path-seq/Split.agda).
    Checking lib.path-seq.Inversion (core/lib/path-seq/Inversion.agda).
    Checking lib.path-seq.Rotations (core/lib/path-seq/Rotations.agda).
 Checking lib.Equivalence2 (core/lib/Equivalence2.agda).
  Checking lib.types.Sigma (core/lib/types/Sigma.agda).
  Checking lib.types.Pi (core/lib/types/Pi.agda).
   Checking lib.types.Empty (core/lib/types/Empty.agda).
   Checking lib.types.Paths (core/lib/types/Paths.agda).
  Checking lib.types.Unit (core/lib/types/Unit.agda).
 Checking lib.NConnected (core/lib/NConnected.agda).
  Checking lib.NType2 (core/lib/NType2.agda).
   Checking lib.Relation2 (core/lib/Relation2.agda).
    Checking lib.types.Coproduct (core/lib/types/Coproduct.agda).
     Checking lib.types.Bool (core/lib/types/Bool.agda).
     Checking lib.types.Lift (core/lib/types/Lift.agda).
   Checking lib.types.TLevel (core/lib/types/TLevel.agda).
    Checking lib.types.Nat (core/lib/types/Nat.agda).
  Checking lib.types.Truncation (core/lib/types/Truncation.agda).
core/HoTT.agda:8,13-27
Failed to solve the following constraints:
  _299
    := λ {;i} {;j} {A} {B} {n} {h} c {;k} P t →
         λ=
         (λ a →
            transport
            (λ r →
               Trunc-rec (_d_284 (c = c) (P = P) (t = t) (a = a) (r = r)) r ==
               t a)
            (! (snd (has-level-apply (c (h a))) [ a , idp ]))
            (_298 (c = c) (P = P) (t = t) (a = a)))
    [blocked on problem 338]
  [338, 343] Trunc-elim
             (_d_284 (c = c) (P = P) (t = t) (a = x)
              (r = (contr-center (c (h x)))))
             (contr-center (c (h x)))
               = Trunc-elim
                 (λ x → transport (λ y → fst (P y)) (snd x) (t (fst x)))
                 (fst (has-level-apply (c (h x))))
               : fst (P (h x))
  _297 := λ {;i} {;j} {A} {B} {n} {h} c {;k} P t a → idp
    [blocked on problem 333]
  [333, 337] Trunc-elim (_d_284 (r = [ a , idp ])) [ a , idp ] = t a
               : fst (P (h a))
when scope checking the declaration
  open import lib.NConnected public
core/HoTT.agda:8,13-27
Unsolved metas at the following locations:
  core/lib/NConnected.agda:57,49-50
  core/lib/NConnected.agda:59,13-16
  core/lib/NConnected.agda:56,19-59,16
when scope checking the declaration
  open import lib.NConnected public

[favonia]

@ice1000 Sorry, I forgot I already committed 63972b7 to make core/HoTT.agda type check on my local branch. Also, the termination checker of 2.6.0-ac38171 seems to reject new code from #29. So there's still some work to do to support 2.6.0.

[kiniry]

@ice1000 Sorry, I forgot I already committed 63972b7 to make core/HoTT.agda type check on my local branch. Also, the termination checker of 2.6.0-ac38171 seems to reject new code from #29. So there's still some work to do to support 2.6.0.

I was looking into the state of HoTT + Agda recently and happened upon this PR. Is anyone still interested in this topic? I just tried 2.6.1 and it is still unhappy about the state of master at least.

[favonia]

@ice1000 Sorry, I forgot I already committed 63972b7 to make core/HoTT.agda type check on my local branch. Also, the termination checker of 2.6.0-ac38171 seems to reject new code from #29. So there's still some work to do to support 2.6.0.

I was looking into the state of HoTT + Agda recently and happened upon this PR. Is anyone still interested in this topic? I just tried 2.6.1 and it is still unhappy about the state of master at least.

Thanks for checking! I believe there's still interest, but all main developers seem occupied by something else now. On the other hand, we always welcome pull requests. :-)

[kiniry]

@ice1000 Sorry, I forgot I already committed 63972b7 to make core/HoTT.agda type check on my local branch. Also, the termination checker of 2.6.0-ac38171 seems to reject new code from #29. So there's still some work to do to support 2.6.0.

I was looking into the state of HoTT + Agda recently and happened upon this PR. Is anyone still interested in this topic? I just tried 2.6.1 and it is still unhappy about the state of master at least.

Thanks for checking! I believe there's still interest, but all main developers seem occupied by something else now. On the other hand, we always welcome pull requests. :-)

I knew you'd say that. ;)

[ice1000]

@ice1000 Sorry, I forgot I already committed 63972b7 to make core/HoTT.agda type check on my local branch. Also, the termination checker of 2.6.0-ac38171 seems to reject new code from #29. So there's still some work to do to support 2.6.0.

I was looking into the state of HoTT + Agda recently and happened upon this PR. Is anyone still interested in this topic? I just tried 2.6.1 and it is still unhappy about the state of master at least.

Thanks for checking! I believe there's still interest, but all main developers seem occupied by something else now. On the other hand, we always welcome pull requests. :-)

I knew you'd say that. ;)

Try agda/cubical, which is as well Agda + HoTT (constructive ver.)!

[kiniry]

@ice1000 Sorry, I forgot I already committed 63972b7 to make core/HoTT.agda type check on my local branch. Also, the termination checker of 2.6.0-ac38171 seems to reject new code from #29. So there's still some work to do to support 2.6.0.

I was looking into the state of HoTT + Agda recently and happened upon this PR. Is anyone still interested in this topic? I just tried 2.6.1 and it is still unhappy about the state of master at least.

Thanks for checking! I believe there's still interest, but all main developers seem occupied by something else now. On the other hand, we always welcome pull requests. :-)

I knew you'd say that. ;)

Try agda/cubical, which is as well Agda + HoTT (constructive ver.)!

I didn't know about cubical. Thanks for pointing it out. Constructive FTW!