compiling behaviour within one file

Stream: mathlib4

[Ralf Stephan]

Thanks to incremental compile and the progress display bar, and simple manipulation of the code, one can identify quickly which lines in a file take most of the compile time. In one case I find this line
https://github.com/leanprover-community/mathlib4/blob/476f5f1808912a5922e3e3e756a0e44f55b9f1da/Mathlib/RingTheory/PowerSeries/Basic.lean#L666

convert MvPowerSeries.coeff_prod _ _ _

stopping the progress bar for 10 seconds. Is this believable? I didn't think convert would be a complex tactic.

[Ralf Stephan]

Is there (another) tool assigning percentage of compile time in a file to single lines?

[Michael Rothgang]

Lean has two built-in profilers: this page describes the "old" one, which gives line-based information. trace.profiler is the new one (which creates collapsible traces; I'm not sure if/where documentation for that one is).

[Michael Rothgang]

Wow, 10 seconds for a convert is really slow: that means something in the file needs to be fixed.

[Kevin Buzzard]

10 seconds for a convert is absolutely normal, it means that, somewhere in the goal and somewhere in what you are trying to convert it to, there were two terms which (a) looked different (b) turned out to be equal by rfl and (c) to prove that they were equal by rfl involved unfolding and unfolding and unfolding until each term was gigantic. The take home is that convert should not be being used here and one wants instead to use convert ... using ... or other tactics which won't embark upon the massive unfold.

[Ralf Stephan]

Thanks. I'll try that. :working_on_it:

[Kevin Buzzard]

In fact, if you write set_option trace.profiler true in before the theorem's docstring and then unfold the trace by clicking on or near the triangles, it turns out that the problem is

  [] [6.725668] ❌ (Multiset.map (fun x ↦ ∏ x_1 ∈ s, (MvPowerSeries.coeff R (Finsupp.single () (x x_1))) (f x_1))
        (s.finsuppAntidiag
            d).val).sum =?= (Multiset.map (fun l ↦ ∏ i ∈ s, (MvPowerSeries.coeff R (l i)) (f i))
        (s.finsuppAntidiag (Finsupp.single () d)).val).sum ▶

Lean takes 6.7 seconds on my computer to fail to prove that two things are equal by rfl.

Changing line 666 to erw [MvPowerSeries.coeff_prod] makes the proof instant, because Lean does not get induced into doing a "heavy rfl", which is the phenomenon you're running into (a rfl which succeeds or fails but takes an age to do so because of an explosion in the size of terms). I'm on a train so don't fancy making a PR but please feel free to make one yourself!

[Kevin Buzzard]

The reason that just a straight rw fails is that if you try

  rw [MvPowerSeries.coeff_prod f (single () d) s]

then you get the error

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  (MvPowerSeries.coeff R (single () d)) (∏ j ∈ s, f j)
...
⊢ (MvPowerSeries.coeff R (single () d)) (∏ j ∈ s, f j) = ...

which looks counterintuitive, but if you then start looking in the innards of what's going on, you find that the MvPowerSeries.coeff in the lemma you're trying to use is (when written out in full)

@DFunLike.coe (MvPowerSeries Unit R →ₗ[R] R) (MvPowerSeries Unit R) (fun x ↦ R) LinearMap.instFunLike
  (MvPowerSeries.coeff R (single () d)) : MvPowerSeries Unit R → R

whereas the MvPowerSeries.coeff in the goal is

@DFunLike.coe (R⟦X⟧ →ₗ[R] R) R⟦X⟧ (fun x ↦ R) LinearMap.instFunLike (MvPowerSeries.coeff R (single () d)) : R⟦X⟧ → R

so there is some slight difference here, caused by the fact that

def PowerSeries (R : Type*) :=
  MvPowerSeries Unit R

is not an abbrev. Perhaps this is the root cause of the issue. erw is a tactic which tries harder to unify, so sees through this non-reducible definition and works successfully.

[Kevin Buzzard]

If you change line 54 of the file from a def to

abbrev PowerSeries (R : Type*) :=
  MvPowerSeries Unit R

then two proofs break because they have rfls in them which aren't needed any more because the goal is already closed (so they can just be deleted), and you can change the bad convert line to just a plain old rw because now rw can see through the problem which was making it break before when the definition of PowerSeries was more irreducible. I would regard this as a good change. It would be interesting to see what else breaks in mathlib after this change -- you can do this by making the change I suggest on a branch, fixing the rfl errors in that same file, and then pushing the branch to github and opening a WIP PR and seeing what CI thinks of it. Once you've got mathlib compiling again (a green tick in CI), you can type !bench in your PR and you'll get a profile of how much faster or slower mathlib is compiling. Sorry I am not able to do this myself, I have ropey internet for the next hour or so.

[Matthew Ballard]

I would think we would want MvPowerSeries API to apply directly to the single variable case

[Kevin Buzzard]

That's your way of saying "I agree that abbrev is worth pursuing" right?

[Matthew Ballard]

But it depends on if we spend tons of time searching for things applying to \sigma := Unit

[Kevin Buzzard]

So the benchmarking is going to be interesting because you're saying that right now we don't know which way it will go.

[Matthew Ballard]

Then it should be a structure probably

[Matthew Ballard]

Yeah, depends on the performance impact on the field

[Ralf Stephan]

The first variant with erw is #14910. Since, with abbrev, the fixes in RingTheory/LaurentSeries.lean will require me some time to get a grip on the subject, you may either help at #14913, or merge #14910. I may be half a math, but I'm definitely no polymath.

[Matthew Ballard]

This exposes a rather nasty diamond

import Mathlib

open Polynomial

variable {F : Type*} [Field F] (f : F[X])

example : (f : RatFunc F) = (f : LaurentSeries F) := by with_unfolding_all rfl -- fails

[Matthew Ballard]

Fails on current master

[Riccardo Brasca]

I think the problem comes from docs#RatFunc.coeAlgHom

[Riccardo Brasca]

Let me see if I can do something

[Riccardo Brasca]

Well, thinking more about it I don't think we can make it defeq: on the RHS everything is clear, the coercion is defined coefficientwise. But on the LHS something nontrivial is happening, a polynomial is viewed as a rational function (and this is trivial), but then to prove that a rational function "is" a power series one has to prove something.

[Riccardo Brasca]

Maybe docs#RatFunc.coe_coe should be simp?

[Riccardo Brasca]

Unless we decide that the coercion from polynomials to power series is "going through RatFunc"

[Riccardo Brasca]

Can we define a morphism out of the fraction ring that has good defeq properties wrt the base ring? If we can then it should be fixable. But I have to go now

[Matthew Ballard]

TIL: irreducible_def involves an opaque

[Riccardo Brasca]

Currently I don't think they're defeq in any sense

[Damiano Testa]

Certainly, most weakenings of Field to something less restrictive will not just prevent DefEq but even PropEq.

[Damiano Testa]

RatFunc F does not contain F if F has non-zero nilpotent elements, right?

[Matthew Ballard]

I am just trying to get it to unfold until really break

[Matthew Ballard]

No defeq + coercions makes this really fiddly

[Riccardo Brasca]

(deleted)

[Riccardo Brasca]

/-- The coercion `RatFunc F → LaurentSeries F` as bundled alg hom. -/
def coeAlgHom (F : Type u) [Field F] : RatFunc F →ₐ[F[X]] LaurentSeries F :=
  liftAlgHom (Algebra.ofId _ _) <|
    nonZeroDivisors_le_comap_nonZeroDivisors_of_injective _ <|
      Polynomial.algebraMap_hahnSeries_injective _

example (F : Type*) [Field F] (p : F[X]) : coeAlgHom F p = Algebra.ofId F[X] (LaurentSeries F) p := by
  rfl --fails

This seems already a problem

[Matthew Ballard]

Some of that is docs#RatFunc.liftOn and docs#RatFunc.mk both use irreducible_def's

[Kyle Miller]

When I debug convert lines, I usually do convert ... using 0 and increment 0 a step at a time until something bad happens.

Then there are also configuration options you can use with convert (config := { ... }) ... using ...; here's the documentation

For example, you can do (config := { closePost := false }) to make it not try to apply rfl when closing sub-goals once nothing else applies. You can also do with_reducible convert ... to make it apply rfl only at reducible transparency. It already tries rfl before descending into a term at reducible transparency (controlled by closePre and preTransparency).

[Matthew Ballard]

Something benchmark-able is queued up for bot

[Matthew Ballard]

I don't understand how the abbrev alters the instance ordering.

[Matthew Ballard]

Benchmarking seems happy

[Riccardo Brasca]

Which branch are you talking about?

[Ralf Stephan]

#14913

[Ralf Stephan]

Matthew Ballard said:

This exposes a rather nasty diamond

By chance, I found something about it in an interview with @Yakov Pechersky :

With rational functions, I find it particularly interesting, because we have a diamond.
From polynomials, you can go to rational functions, and then to Laurent series.
Or you can go from polynomials to power series, and then to Laurent series.

https://leanprover-community.github.io/blog/posts/backstage-with-pechersky/