GammaSpecAdjunction

Stream: mathlib4

[Ruben Van de Velde]

It seems like Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean was already slow in places, but it got much worse on recent nightlies with isIso_locallyRingedSpaceAdjunction_counit needing 1.6M heartbeats on the nightly-testing branch (up from .4M). @Junyan Xu , would you happen to be around to take a look?

[Kevin Buzzard]

You can see in the term that we're forcing Lean to unify f.unop.op.unop with f.unop, although I don't know if this is the problem. I haven't seriously thought about the algebraic geometry part of Lean since the port so am only just getting up to speed. Note that right now the proof has convert ... using 1 but ...using 0 or just removing the using completely all work, and are all equally slow.

[Adam Topaz]

ooof this whole file is slow!

[Adam Topaz]

but yeah my laptop's fans started kicking in with isIso_...

[Kevin Buzzard]

Lol I've got it! It's a universe issue! Hang on

[Kevin Buzzard]

instance isIso_locallyRingedSpaceAdjunction_counit :
    IsIso.{u + 1, u + 1} locallyRingedSpaceAdjunction.counit :=
  IsIso.of_iso_inv (NatIso.op SpecΓIdentity)

This is immediate. It also removes the porting note; the dsimp is gone. rfl is telling me that this is the same term as before.

[Matthew Ballard]

I’d like to see where Lean is spending its time here

[Andrew Yang]

Also I wonder how you found it?

[Adam Topaz]

I bet the adjunction itself has some unnecessary universe parameters… docs#locallyRingedSpaceAdjunction

[Adam Topaz]

docs#CategoryTheory.IsIso

[Adam Topaz]

FWIW, adding a universe annotation as follows:

def SpecΓIdentity : Spec.toLocallyRingedSpace.{u}.rightOp ⋙ Γ ≅ 𝟭 _ :=

also speeds things up (and allows to remove the heartbeat setting there)

[Ruben Van de Velde]

Please push those somewhere :)

[Kevin Buzzard]

Andrew Yang said:

Also I wonder how you found it?

Oh I am a lean guru and it was obvious to me the moment I saw the question. No, actually it was blind luck. I was trying to figure out which parts of the terms didn't unify in the convert call, so I changed the proof to have foo := IsIso.of_iso_inv (NatIso.op SpecΓIdentity); convert foo and then printed out the goal and foo with pp.all on and then tried to diff them in a console. But one was full of ?u.117323s and the other was full of ?u.116808s so the diff was huge. So I decided to make them both u to make the diff smaller and then the declaration just magically compiled immediately. I have absolutely no idea why (that was why it got a lol, I had been banging my head against a wall for about an hour before that)

[Kevin Buzzard]

Ruben Van de Velde said:

Please push those somewhere :)

I'll do this now.

[Kevin Buzzard]

Adam Topaz said:

FWIW, adding a universe annotation as follows:

def SpecΓIdentity : Spec.toLocallyRingedSpace.{u}.rightOp ⋙ Γ ≅ 𝟭 _ :=

also speeds things up (and allows to remove the heartbeat setting there)

I'm not entirely sure which heartbeat setting you're talking about. What is so weird is that in the isIso_locallyRingedSpaceAdjunction_counit example there just seem to be two universe metavariables in the convert call and it's trivial to unify them just by making them equal.

[Adam Topaz]

@Kevin Buzzard I'm talking about this one: https://github.com/leanprover-community/mathlib4/blob/ca5e44c32834549fd360f9b38470252b297e314c/Mathlib/AlgebraicGeometry/Spec.lean#L335

[Kevin Buzzard]

#12469 for the GammaSpecAdjunction file

[Kevin Buzzard]

Adam Topaz said:

Kevin Buzzard I'm talking about this one: https://github.com/leanprover-community/mathlib4/blob/ca5e44c32834549fd360f9b38470252b297e314c/Mathlib/AlgebraicGeometry/Spec.lean#L335

I cannot find this on master, and I'm not up to speed with how nightly-testing works. Perhaps it's time someone explained to me (possibly for the second time :-/ ) how I could help here.

[Ruben Van de Velde]

1. check out the nightly testing branch
2. put a :hammer_and_wrench: on the latest message in https://leanprover.zulipchat.com/#narrow/stream/428973-nightly-testing/topic/Mathlib.20status.20updates
3. fix an issue
4. push back to nightly-testing

[Ruben Van de Velde]

+ ~Mathlib.AlgebraicGeometry.GammaSpecAdjunction   instructions   -54.2%

Damn

[Kevin Buzzard]

yeah that is very weird. Note that SpecΓIdentity_hom_app_presheaf_obj is particularly wild; the only change made in the PR is changing {X : Scheme} to {X : Scheme.{u}} and compilation time on my machine reliably drops from 0.7 secs to 0.23 according to trace.profiler. As explained in the PR, I spotted this one by lowering maxHeartbeats in the entire file to 20000 from 200000 and then fixing what broke with these crazy explicit universe annotations. Note that I don't change the proof at all in this one, and there was only ever one universe in the statement, so this totally contradicts my model of what is going on.

[Kevin Buzzard]

An example of the diff with trace.profiler on:

<             [Elab.step] [0.222938s] expected type: Quiver.Hom.{?u.133110 + 1, ?u.133110 + 1}
<                   (AlgebraicGeometry.Scheme.Γ.{?u.133110}.obj
<                     (Opposite.op.{?u.133110 + 2}
<                       (AlgebraicGeometry.Scheme.Spec.{?u.133110}.obj
<                         (Opposite.op.{?u.133110 + 2}
<                           (X.presheaf.obj
<                             (Opposite.op.{?u.133110 + 1}
<                               ((IsOpenMap.functor.{?u.133110} ⋯).obj Top.top.{?u.133110})))))))
<                   ((TopCat.Presheaf.pushforwardObj.{?u.133110, ?u.133110, ?u.133110 + 1}
<                         (AlgebraicGeometry.ΓSpec.adjunction.{?u.133110}.unit.app (X ∣_ᵤ U)).val.base
<                         ((CategoryTheory.Functor.id.{?u.133110, ?u.133110 + 1} AlgebraicGeometry.Scheme.{?u.133110}).obj
---
>             [Elab.step] [0.017098s] expected type: Quiver.Hom.{u + 1, u + 1}
>                   (AlgebraicGeometry.Scheme.Γ.{u}.obj
>                     (Opposite.op.{u + 2}
>                       (AlgebraicGeometry.Scheme.Spec.{u}.obj
>                         (Opposite.op.{u + 2}
>                           (X.presheaf.obj (Opposite.op.{u + 1} ((IsOpenMap.functor.{u} ⋯).obj Top.top.{u})))))))
>                   ((TopCat.Presheaf.pushforwardObj.{u, u, u + 1}
>                         (AlgebraicGeometry.ΓSpec.adjunction.{u}.unit.app (X ∣_ᵤ U)).val.base
>                         ((CategoryTheory.Functor.id.{u, u + 1} AlgebraicGeometry.Scheme.{u}).obj

Seems to be literally equal other than the fact that one universe metavariable is replaced with one concrete universe, and we have a 13x speedup.

[Ruben Van de Velde]

SpecΓIdentity_naturality was the last one that caused trouble on nightly, so I fixed a similar fix to your PR

[Kevin Buzzard]

Just to confirm -- I'm still tinkering with the GammaSpecAdjunction file trying to figure out what's going on, feel free to play with the nightly.

[Ruben Van de Velde]

It builds, so I'm not touching it anymore :)

[Ruben Van de Velde]

Sadly, Mathlib/AlgebraicGeometry/AffineScheme.lean has issues that seem similar

[Kevin Buzzard]

OK, next observation is that with set_option trace.profiler true on SpecΓIdentity_hom_app_presheaf_obj, even with set_option profiler.threshold 1, changing {X : Scheme} to {X : Scheme.{u}} makes the total size of the trace output go from 1421 lines to 88 lines. So that's maybe the source of the speedup -- there is a whole ton of stuff which literally isn't happening any more?

[Kevin Buzzard]

2000 lines of trace output starting with this:

<               [Meta.isDefEq] [0.202370s] ✅ Quiver.Hom.{?u.133110 + 1, ?u.133110 + 1}
<                     (AlgebraicGeometry.Scheme.Γ.{?u.133110}.obj
<                       (Opposite.op.{?u.133110 + 2}
<                         (AlgebraicGeometry.Scheme.Spec.{?u.133110}.obj
<                           (Opposite.op.{?u.133110 + 2}
<                             (X.presheaf.obj
<                               (Opposite.op.{?u.133110 + 1}
<                                 ((IsOpenMap.functor.{?u.133110} ⋯).obj Top.top.{?u.133110})))))))
<                     ?m.133590 =?= Quiver.Hom.{?u.133110 + 1, ?u.133110 + 1}
<                     (((CategoryTheory.Functor.comp.{?u.133110, ?u.133110, ?u.133110, ?u.133110 + 1, ?u.133110 + 1,
<                                   ?u.133110 + 1}
<                                 (CategoryTheory.Functor.rightOp.{?u.133110, ?u.133110, ?u.133110 + 1, ?u.133110 + 1}
<                                   AlgebraicGeometry.Scheme.Γ.{?u.133110})
<                                 AlgebraicGeometry.Scheme.Spec.{?u.133110}).obj
<                             (X ∣_ᵤ U)).presheaf.obj
<                       (Opposite.op.{?u.133110 + 1} Top.top.{?u.133110}))
<                     ((TopCat.Presheaf.pushforwardObj.{?u.133110, ?u.133110, ?u.133110 + 1}
<                           (AlgebraicGeometry.ΓSpec.adjunction.{?u.133110}.unit.app (X ∣_ᵤ U)).val.base
<                           ((CategoryTheory.Functor.id.{?u.133110, ?u.133110 + 1}
<                                   AlgebraicGeometry.Scheme.{?u.133110}).obj
<                               (X ∣_ᵤ U)).presheaf).obj
<                       (Opposite.op.{?u.133110 + 1} Top.top.{?u.133110}))

are literally missing once you supply the universe explicitly. So explicitly adding the universe seems to makes defeq much better. That's perhaps a useful take-home.