Zulip Chat Archive
Stream: mathlib4
Topic: diagnosing timeouts in RingHom.RespectsIso.ofRestrict_mor...
Ruben Van de Velde (Sep 04 2023 at 10:03):
Scott Morrison said:
430.063014 unusedArguments RingHom.RespectsIso.ofRestrict_morphismRestrict_iff 201.888680 simpNF AlgebraicGeometry.StructureSheaf.isLocallyFraction_pred 182.304759 simpNF Rep.MonoidalClosed.linearHomEquivComm_hom 179.932156 simpNF Rep.MonoidalClosed.linearHomEquiv_hom 145.505241 simpNF Matrix.linfty_op_nnnorm_row 119.100756 simpNF lp.infty_coeFn_nat_cast 118.556040 simpNF CategoryTheory.OplaxNatTrans.whiskerRight_naturality_comp_assoc 118.393575 simpNF lp.infty_coeFn_int_cast 116.262702 simpNF Matrix.linfty_op_norm_col 95.031026 simpNF CategoryTheory.OplaxFunctor.bicategory_comp_naturality 94.551145 simpNF AlgebraicGeometry.Scheme.GlueData.ι_isoCarrier_inv
Oh, this one?
set_option maxHeartbeats 6000000 in
theorem RespectsIso.ofRestrict_morphismRestrict_iff (hP : RingHom.RespectsIso @P) {X Y : Scheme}
Ruben Van de Velde (Sep 04 2023 at 10:16):
(Seems like the erw [f.1.c.naturality_assoc, ← X.presheaf.map_comp, ← X.presheaf.map_comp, ← X.presheaf.map_comp] at the end is already responsible for 5 minutes of compilation time here)
Bhavik Mehta (Sep 04 2023 at 10:17):
Do we know if it's the rewrites or the implicit rfl at the end? Is there erewrite?
Ruben Van de Velde (Sep 04 2023 at 10:23):
385s in rewrite, 1.5s in rfl
Ruben Van de Velde (Sep 04 2023 at 10:34):
Everything seems to be quite miserable here, random rewrites and dsimps taking several seconds each, and then it goes really off the rails towards the end. Maybe just because of the big terms?
Matthew Ballard (Sep 04 2023 at 12:24):
Ruben Van de Velde said:
Oh, this one?
set_option maxHeartbeats 6000000 in theorem RespectsIso.ofRestrict_morphismRestrict_iff (hP : RingHom.RespectsIso @P) {X Y : Scheme}
rewrite is way too expensive in all of AG
Matthew Ballard (Sep 04 2023 at 12:29):
Ruben Van de Velde said:
Everything seems to be quite miserable here, random rewrites and dsimps taking several seconds each, and then it goes really off the rails towards the end. Maybe just because of the big terms?
While porting, I generated a 1/2 Gb text file just for the goal state. Too much gets has to get exposed for the current implementation to work.
Kevin Buzzard (Sep 04 2023 at 14:06):
here is the timing for each tactic in the proof.
Kevin Buzzard (Sep 04 2023 at 14:13):
If you unfold the 40 second rewrite
[] [40.784633s] rw [morphismRestrict_c_app, Category.assoc, Category.assoc, Category.assoc] ▶
then you see...nothing of any interest. The trace is here and there seems to be no information about what is taking 40 seconds -- it's one of those situations where the traces don't add up (and here they don't add up at all, the subexpressions are only a couple of seconds in total)
Matthew Ballard (Sep 04 2023 at 14:15):
We might want to split this particular diagnosis off into another topic.
I assume it is morphismRestrict_c_app that is slow and not the repeated Category.assoc's?
Notification Bot (Sep 04 2023 at 23:37):
11 messages were moved here from #mathlib4 > ideas for speeding up CI by Scott Morrison.
Kevin Buzzard (Sep 05 2023 at 07:10):
[] [25.130139s] rw [morphismRestrict_c_app] ▶
[] [24.773864s] rw [Category.assoc, Category.assoc, Category.assoc] ▶
Furthermore,
[] [86.214118s] refine' Eq.trans _ (@Category.assoc CommRingCat _ _ _ _ _ _ _ _)
unfolds to
[] [80.402848s] ✅ let src :=
NonUnitalRingHom.comp
(RingHom.toNonUnitalRingHom
(X.presheaf.map
...
(the let is coming from docs#RingHom.comp -- is that with there considered harmful?) but half of the problem there is
[] [42.190391s] ❌ ↑(X.presheaf.map
(CategoryTheory.homOfLE
(_ :
(IsOpenMap.functor
(_ :
IsOpenMap
↑(TopologicalSpace.Opens.inclusion
((TopologicalSpace.Opens.map
f.val.base).obj
(AlgebraicGeometry.Scheme.basicOpen
Y r))))).obj
((IsOpenMap.functor
(_ :
IsOpenMap
↑(TopologicalSpace.Opens.inclusion
((TopologicalSpace.Opens.map
(AlgebraicGeometry.Scheme.ofRestrict
X
(_ :
OpenEmbedding
↑(TopologicalSpace.Opens.inclusion
((TopologicalSpace.Opens.map
f.val.base).obj
(AlgebraicGeometry.Scheme.basicOpen
Y
r))))).val.base).obj
U)))).op.obj
(Opposite.op ⊤)).unop ≤
(IsOpenMap.functor
(_ :
IsOpenMap
↑(TopologicalSpace.Opens.inclusion
U))).obj
(Opposite.op
⊤).unop)).op) =?= ↑(?m.29303 ≫ ?m.29304) ▼
```
Last updated: Dec 20 2023 at 11:08 UTC