explosion involving `Pi.commSemiring`

Stream: mathlib4

[Kevin Buzzard]

I was looking at #13032 . In this, @Michael Stoll increases the priority of Algebra.id . The idea is that the obvious instance docs#Algebra.id of type Algebra R R should hopefully be quick to fail (is this right? Typeclass inference only uses a weak quick-to-fail rfl, right?) so there's no harm in trying it first rather than last (it is the first-declared instance of Algebra X Y declared in mathlib so the typeclass algorithm places it at the back of the queue behind all other default prio Algebra instances in mathlib; the PR is arguing that it should be at the front).

The change broke mathlib in two places. One of them was Mathlib/RingTheory/Jacobson.lean, where the proof of the (private, although this is not the issue) theorem docs#quotient_mk_comp_C_isIntegral_of_jacobson' broke. At a point where the goal was

⊢ (quotientMap P C _ : R ⧸ comap C P →+* R[X] ⧸ P).IsIntegral

the tactic

  refine' RingHom.IsIntegral.tower_bot φ (algebraMap _ (Localization M')) _ _

was breaking. At first glance you can imagine that something involving algebraMap _ X could well be affected by a change to Algebra.id : algebraMap R R on the basis that it might apply (I am reminded of @Kim Morrison 's comment to me years ago when I asked them whether one should fill in underscores or not, when we know what they are, and they replied that it was probably good practice, although I think that leaving easy-to-fill-in underscores is part of "golf culture" so of course they plague mathlib). I figured out the underscore manually (it was R[X] ⧸ P) and filled it in. @Ruben Van de Velde then benchmarked the PR and there was a 10% reduction in the file speed!

This inspired me to look at some traces, so I started with dumping set_option trace.profiler true in before the proof of the theorem, and then I kept opening the trace following it towards the refine' line, which was indeed looking like it was taking a suspicious amount of time:

      [] [0.882695] refine' RingHom.IsIntegral.tower_bot φ (algebraMap _ (Localization M')) _ _  ▶

which turned into a

              [Meta.synthInstance] [0.796256] 💥 CommSemiring ?m.264932  ▶

Intrigued, I clicked onto the triangle to see what was causing the explosion, and VS Code crashed.

So I compiled the file through lake on the command line and piped the output to a file. It was 19 megabytes long. This is completely absurd. My first question is: is there a way to profile every declaration in mathlib like this, and flag proofs whose traces turn out to be 19 megabytes long?

I'm currently trying to make sense of the trace. Most of it seems to be really really really long lines which start

                [Meta.synthInstance] [0.010800] ✅ apply @Pi.commSemiring to (i : ?m.265071) →
                      (i_1 : ?m.265127 i) →
                        (i_2 : ?m.265191 i i_1) →
                          (i_3 : ?m.265263 i i_1 i_2) →
                            (i_4 : ?m.265343 i i_1 i_2 i_3) →
                              (i_5 : ?m.265431 i i_1 i_2 i_3 i_4) →
                                (i_6 : ?m.265527 i i_1 i_2 i_3 i_4 i_5) →
                                  (i_7 : ?m.265631 i i_1 i_2 i_3 i_4 i_5 i_6) →
                                    (i_8 : ?m.265743 i i_1 i_2 i_3 i_4 i_5 i_6 i_7) →
                                      (i_9 : ?m.265863 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8) →
                                        (i_10 : ?m.265991 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9) →
                                          (i_11 : ?m.266127 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10) →
                                            (i_12 : ?m.266271 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8 i_9 i_10 i_11) →
      ...

or

                  [Meta.synthInstance.tryResolve] [0.012807] ✅ CommSemiring
                        ((i_1 :
                            ?m.316431 i✝¹⁰⁵ i✝¹⁰⁴ i✝¹⁰³ i✝¹⁰² i✝¹⁰¹ i✝¹⁰⁰ i✝⁹⁹ i✝⁹⁸ i✝⁹⁷ i✝⁹⁶ i✝⁹⁵ i✝⁹⁴ i✝⁹³ i✝⁹² i✝⁹¹
                              i✝⁹⁰ i✝⁸⁹ i✝⁸⁸ i✝⁸⁷ i✝⁸⁶ i✝⁸⁵ i✝⁸⁴ i✝⁸³ i✝⁸² i✝⁸¹ i✝⁸⁰ i✝⁷⁹ i✝⁷⁸ i✝⁷⁷ i✝⁷⁶ i✝⁷⁵ i✝⁷⁴ i✝⁷³
                              i✝⁷² i✝⁷¹ i✝⁷⁰ i✝⁶⁹ i✝⁶⁸ i✝⁶⁷ i✝⁶⁶ i✝⁶⁵ i✝⁶⁴ i✝⁶³ i✝⁶² i✝⁶¹ i✝⁶⁰ i✝⁵⁹ i✝⁵⁸ i✝⁵⁷ i✝⁵⁶ i✝⁵⁵
                              i✝⁵⁴ i✝⁵³ i✝⁵² i✝⁵¹ i✝⁵⁰ i✝⁴⁹ i✝⁴⁸ i✝⁴⁷ i✝⁴⁶ i✝⁴⁵ i✝⁴⁴ i✝⁴³ i✝⁴² i✝⁴¹ i✝⁴⁰ i✝³⁹ i✝³⁸ i✝³⁷
                              i✝³⁶ i✝³⁵ i✝³⁴ i✝³³ i✝³² i✝³¹ i✝³⁰ i✝²⁹ i✝²⁸ i✝²⁷ i✝²⁶ i✝²⁵ i✝²⁴ i✝²³ i✝²² i✝²¹ i✝²⁰ i✝¹⁹
                              i✝¹⁸ i✝¹⁷ i✝¹⁶ i✝¹⁵ i✝¹⁴ i✝¹³ i✝¹² i✝¹¹ i✝¹⁰ i✝⁹ i✝⁸ i✝⁷ i✝⁶ i✝⁵ i✝⁴ i✝³ i✝² i✝¹ i✝ i) →

Again one could ask whether it's possible to ask Lean which proofs involve metavariables with the name i✝³⁷ because you would imagine that something had gone wrong at this point.

The punchline seems to be

                  [Meta.synthInstance.tryResolve] [0.012807] ✅ CommSemiring
                        ((i_1 :
                            ?m.316431 i✝¹⁰⁵ i✝¹⁰⁴ i✝¹⁰³ i✝¹⁰² i✝¹⁰¹ i✝¹⁰⁰ i✝⁹⁹ i✝⁹⁸ i✝⁹⁷ i✝⁹⁶ i✝⁹⁵ i✝⁹⁴ i✝⁹³ i✝⁹² i✝⁹¹
                              i✝⁹⁰ i✝⁸⁹ i✝⁸⁸ i✝⁸⁷ i✝⁸⁶ i✝⁸⁵ i✝⁸⁴ i✝⁸³ i✝⁸² i✝⁸¹ i✝⁸⁰ i✝⁷⁹ i✝⁷⁸ i✝⁷⁷ i✝⁷⁶ i✝⁷⁵ i✝⁷⁴ i✝⁷³
                              i✝⁷² i✝⁷¹ i✝⁷⁰ i✝⁶⁹ i✝⁶⁸ i✝⁶⁷ i✝⁶⁶ i✝⁶⁵ i✝⁶⁴ i✝⁶³ i✝⁶² i✝⁶¹ i✝⁶⁰ i✝⁵⁹ i✝⁵⁸ i✝⁵⁷ i✝⁵⁶ i✝⁵⁵
                              i✝⁵⁴ i✝⁵³ i✝⁵² i✝⁵¹ i✝⁵⁰ i✝⁴⁹ i✝⁴⁸ i✝⁴⁷ i✝⁴⁶ i✝⁴⁵ i✝⁴⁴ i✝⁴³ i✝⁴² i✝⁴¹ i✝⁴⁰ i✝³⁹ i✝³⁸ i✝³⁷
                              i✝³⁶ i✝³⁵ i✝³⁴ i✝³³ i✝³² i✝³¹ i✝³⁰ i✝²⁹ i✝²⁸ i✝²⁷ i✝²⁶ i✝²⁵ i✝²⁴ i✝²³ i✝²² i✝²¹ i✝²⁰ i✝¹⁹
                              i✝¹⁸ i✝¹⁷ i✝¹⁶ i✝¹⁵ i✝¹⁴ i✝¹³ i✝¹² i✝¹¹ i✝¹⁰ i✝⁹ i✝⁸ i✝⁷ i✝⁶ i✝⁵ i✝⁴ i✝³ i✝² i✝¹ i✝ i) →
                          ?m.316432 i✝¹⁰⁵ i✝¹⁰⁴ i✝¹⁰³ i✝¹⁰² i✝¹⁰¹ i✝¹⁰⁰ i✝⁹⁹ i✝⁹⁸ i✝⁹⁷ i✝⁹⁶ i✝⁹⁵ i✝⁹⁴ i✝⁹³ i✝⁹² i✝⁹¹
                            i✝⁹⁰ i✝⁸⁹ i✝⁸⁸ i✝⁸⁷ i✝⁸⁶ i✝⁸⁵ i✝⁸⁴ i✝⁸³ i✝⁸² i✝⁸¹ i✝⁸⁰ i✝⁷⁹ i✝⁷⁸ i✝⁷⁷ i✝⁷⁶ i✝⁷⁵ i✝⁷⁴ i✝⁷³
                            i✝⁷² i✝⁷¹ i✝⁷⁰ i✝⁶⁹ i✝⁶⁸ i✝⁶⁷ i✝⁶⁶ i✝⁶⁵ i✝⁶⁴ i✝⁶³ i✝⁶² i✝⁶¹ i✝⁶⁰ i✝⁵⁹ i✝⁵⁸ i✝⁵⁷ i✝⁵⁶ i✝⁵⁵
                            i✝⁵⁴ i✝⁵³ i✝⁵² i✝⁵¹ i✝⁵⁰ i✝⁴⁹ i✝⁴⁸ i✝⁴⁷ i✝⁴⁶ i✝⁴⁵ i✝⁴⁴ i✝⁴³ i✝⁴² i✝⁴¹ i✝⁴⁰ i✝³⁹ i✝³⁸ i✝³⁷
                            i✝³⁶ i✝³⁵ i✝³⁴ i✝³³ i✝³² i✝³¹ i✝³⁰ i✝²⁹ i✝²⁸ i✝²⁷ i✝²⁶ i✝²⁵ i✝²⁴ i✝²³ i✝²² i✝²¹ i✝²⁰ i✝¹⁹
                            i✝¹⁸ i✝¹⁷ i✝¹⁶ i✝¹⁵ i✝¹⁴ i✝¹³ i✝¹² i✝¹¹ i✝¹⁰ i✝⁹ i✝⁸ i✝⁷ i✝⁶ i✝⁵ i✝⁴ i✝³ i✝² i✝¹ i✝ i
                            i_1) ≟ CommSemiring
                        ((i_1 :
                            ?m.316431 i✝¹⁰⁵ i✝¹⁰⁴ i✝¹⁰³ i✝¹⁰² i✝¹⁰¹ i✝¹⁰⁰ i✝⁹⁹ i✝⁹⁸ i✝⁹⁷ i✝⁹⁶ i✝⁹⁵ i✝⁹⁴ i✝⁹³ i✝⁹² i✝⁹¹
                              i✝⁹⁰ i✝⁸⁹ i✝⁸⁸ i✝⁸⁷ i✝⁸⁶ i✝⁸⁵ i✝⁸⁴ i✝⁸³ i✝⁸² i✝⁸¹ i✝⁸⁰ i✝⁷⁹ i✝⁷⁸ i✝⁷⁷ i✝⁷⁶ i✝⁷⁵ i✝⁷⁴ i✝⁷³
                              i✝⁷² i✝⁷¹ i✝⁷⁰ i✝⁶⁹ i✝⁶⁸ i✝⁶⁷ i✝⁶⁶ i✝⁶⁵ i✝⁶⁴ i✝⁶³ i✝⁶² i✝⁶¹ i✝⁶⁰ i✝⁵⁹ i✝⁵⁸ i✝⁵⁷ i✝⁵⁶ i✝⁵⁵
                              i✝⁵⁴ i✝⁵³ i✝⁵² i✝⁵¹ i✝⁵⁰ i✝⁴⁹ i✝⁴⁸ i✝⁴⁷ i✝⁴⁶ i✝⁴⁵ i✝⁴⁴ i✝⁴³ i✝⁴² i✝⁴¹ i✝⁴⁰ i✝³⁹ i✝³⁸ i✝³⁷
                              i✝³⁶ i✝³⁵ i✝³⁴ i✝³³ i✝³² i✝³¹ i✝³⁰ i✝²⁹ i✝²⁸ i✝²⁷ i✝²⁶ i✝²⁵ i✝²⁴ i✝²³ i✝²² i✝²¹ i✝²⁰ i✝¹⁹
                              i✝¹⁸ i✝¹⁷ i✝¹⁶ i✝¹⁵ i✝¹⁴ i✝¹³ i✝¹² i✝¹¹ i✝¹⁰ i✝⁹ i✝⁸ i✝⁷ i✝⁶ i✝⁵ i✝⁴ i✝³ i✝² i✝¹ i✝ i) →
                          ?m.316432 i✝¹⁰⁵ i✝¹⁰⁴ i✝¹⁰³ i✝¹⁰² i✝¹⁰¹ i✝¹⁰⁰ i✝⁹⁹ i✝⁹⁸ i✝⁹⁷ i✝⁹⁶ i✝⁹⁵ i✝⁹⁴ i✝⁹³ i✝⁹² i✝⁹¹
                            i✝⁹⁰ i✝⁸⁹ i✝⁸⁸ i✝⁸⁷ i✝⁸⁶ i✝⁸⁵ i✝⁸⁴ i✝⁸³ i✝⁸² i✝⁸¹ i✝⁸⁰ i✝⁷⁹ i✝⁷⁸ i✝⁷⁷ i✝⁷⁶ i✝⁷⁵ i✝⁷⁴ i✝⁷³
                            i✝⁷² i✝⁷¹ i✝⁷⁰ i✝⁶⁹ i✝⁶⁸ i✝⁶⁷ i✝⁶⁶ i✝⁶⁵ i✝⁶⁴ i✝⁶³ i✝⁶² i✝⁶¹ i✝⁶⁰ i✝⁵⁹ i✝⁵⁸ i✝⁵⁷ i✝⁵⁶ i✝⁵⁵
                            i✝⁵⁴ i✝⁵³ i✝⁵² i✝⁵¹ i✝⁵⁰ i✝⁴⁹ i✝⁴⁸ i✝⁴⁷ i✝⁴⁶ i✝⁴⁵ i✝⁴⁴ i✝⁴³ i✝⁴² i✝⁴¹ i✝⁴⁰ i✝³⁹ i✝³⁸ i✝³⁷
                            i✝³⁶ i✝³⁵ i✝³⁴ i✝³³ i✝³² i✝³¹ i✝³⁰ i✝²⁹ i✝²⁸ i✝²⁷ i✝²⁶ i✝²⁵ i✝²⁴ i✝²³ i✝²² i✝²¹ i✝²⁰ i✝¹⁹
                            i✝¹⁸ i✝¹⁷ i✝¹⁶ i✝¹⁵ i✝¹⁴ i✝¹³ i✝¹² i✝¹¹ i✝¹⁰ i✝⁹ i✝⁸ i✝⁷ i✝⁶ i✝⁵ i✝⁴ i✝³ i✝² i✝¹ i✝ i i_1)

Just getting off a train, will be offline for several hours now but that's as far as I got.

[Matthew Ballard]

What about changing refine' to refine?

[Kevin Buzzard]

Solves it!

[Kevin Buzzard]

So what is the reason for the explosion?

[Matthew Ballard]

lean#4206 I believe

[Matthew Ballard]

@Jovan Gerbscheid mentions that refine' and convert share this issue

[Yaël Dillies]

Kevin Buzzard said:

Intrigued, I clicked onto the triangle to see what was causing the explosion, and VS Code crashed.

Forbidden knowledge :zip_it:

[Ruben Van de Velde]

Vs code is protecting you from the horrors that lean is creating

[Ruben Van de Velde]

(and now I have an actual argument against refine')

[Matthew Ballard]

Terrible Secret of Lean

[Jovan Gerbscheid]

On the branch with the bug fix, the proof does not break :)

[Jovan Gerbscheid]

Also, Mathlib.RingTheory.Jacobson is the most affected file by the bug fix, reducing build instructions by 28%

[Matthew Ballard]

I think it is fine to backport this change from #13001 to master

- refine' ((isMaximal_iff_isMaximal_disjoint (Localization M) _ _).mp (by rwa [map_bot])).1
+ exact ((isMaximal_iff_isMaximal_disjoint (Localization M) a _).mp (by rwa [map_bot])).1

[Matthew Ballard]

I decided to clean out this file #13062

[Kevin Buzzard]

So refine' should be purged from mathlib? Can one automatically check for other occurrences of instance search going out of control in this precise way? (the "is there a ^{37} in the term" test).

[Matthew Ballard]

Let's see the results of @Damiano Testa 's experiment at #13059 before we get too aggressive about purging.

[Matthew Ballard]

It looks like the refine' penalty might be localized

[Jovan Gerbscheid]

Matthew Ballard said:

I decided to clean out this file #13062

That's funny, it looks like the speedup you get from replacing the refine' with refine is the same as the speedup that we get from the bug fix. 28% for the bug-fix, 29% for your clean-up

[Matthew Ballard]

Yes, the erroneous metavariable assignments seem to be the main source of performance degradation. Even so, I think refine' should be phased out

[Jovan Gerbscheid]

I'm not up to date with the difference. What is wrong with refine'?

[Matthew Ballard]

I think the main issue is that it is less declarative impacting readability. It was also developed during the port because refine itself had some rough edges. Things are different now

[Jovan Gerbscheid]

For something like refine (isIntegral_quotientMap_iff _).mp ?_, where apply (isIntegral_quotientMap_iff _).mp also works, do we prefer refine for the same readability reason, that you can immediately see the arity of the application?

[Matthew Ballard]

I would say no but that is very much my personal taste speaking. Others might feel differently