!4#4322 last dependency for `Ext`

Stream: mathlib4

[Kevin Buzzard]

!4#4322 is CategoryTheory.Abelian.Projective, the last remaining dependency before category_theory.abelian.ext. It's all working apart from one horrible timeout, where dsimp starts with a long pause, and finishes with

  Message: Server process for file:///home/buzzard/lean-projects/mathlib4/Mathlib/CategoryTheory/Abelian/Projective.lean crashed, likely due to a stack overflow or a bug.
  Code: -32902

I'm leaving this for the day now; I've marked it help-wanted and left some notes.

[Matthew Ballard]

I also had timeouts for the dual declaration in CategoryTheory.Abelian.InjectiveResolutions. I had to outline some of the results used in the construction of of to get it built in a reasonable amount of time. I did the same thing here. The sorry is now gone but the build time for is still quite high. Worse than for injectives.

[Matthew Ballard]

In the worst declaration exact_ofComplex there are two branches each calling simp. They both take about 8s.

[Matthew Ballard]

One simp is unsqueezed and the other is squeezed.

[Matthew Ballard]

From a quick look, it does not appear replacing simp with a chain of rw’s will help much

[Scott Morrison]

I added some notes suggesting a better design that perhaps could be explored. Please have a look! I'm not sure if it is better to try this out now, or just to merge with these notes in place and try to come back to this soon. I'm inclined towards the later.

[Kevin Buzzard]

I've not looked at Scott's notes but here's what the profiler says on the last half of the file and it's not pretty.

All Messages (4)
Projective.lean:84:0
dsimp took 1.54s
simp took 6.12s
compilation of CategoryTheory.ProjectiveResolution.ofComplex took 6.25s
Projective.lean:96:0
simp took 5.39s
Projective.lean:106:0
simp took 9.72s
simp took 10.4s
tactic execution of Lean.Parser.Tactic.rewriteSeq took 846ms
tactic execution of Lean.Parser.Tactic.apply took 74.1s
type checking took 145ms
linting took 291ms
Projective.lean:118:0
tactic execution of Lean.Parser.Tactic.apply took 10.9s
simp took 15.6s

"Apply took 74 seconds" :-/

[Kevin Buzzard]

But it compiles. Am I right in thinking that of is still definitionally equal to what it was before? Seems that it's just the proofs which have been refactored. If so I would also be happy with the idea of "merge now, try the refactor later".

[Matthew Ballard]

Yes. Thanks for the investigation Scott and Kevin. It’s the same proof but more hand holding, smaller steps. I also think merge now and return to the issue later is probably best.