Why is tensor product noncomputable?

Stream: mathlib4

[Kenny Lau]

I looked at the file, and it has the tag suppress_compilation, and the docstring says

This is a hack to work around https://github.com/leanprover-community/mathlib4/issues/7103 .

And the issue is 2 years old, is it still an issue now? Can someone summarise the main problem? Isn't it just a quotient of List?

[Matthew Ballard]

With the new compiler, it would be a good idea to see if the situation has improved.

[Kenny Lau]

When was the new compiler born?

[Matthew Ballard]

ETA soonish I think

[Matthew Ballard]

The problem is that noncomputable means try to compile and give up if unsuccessful. Failure was taking too long

[Kenny Lau]

@Matthew Ballard so the question is why was it taking too long?

[Matthew Ballard]

Still an unknown. Pretty sure it was somewhere in the old compiler

[Matthew Ballard]

Since it’s bothering me but not enough to touch code let me hedge the above with: it might only apply to noncomputable section

[Matthew Ballard]

Profiling the C++ components of the language is rather murky (to me at least). And compiled code isn’t a priority (for math) so you get the solution above.

Hopefully the new compiler can give us more visibility. For the kernel you should be able to use lean4lean but I was not able to get that working in limited attempts.

[Cameron Zwarich]

Which file do you mean in particular? With the new compiler, if I remove this from Mathlib/LinearAlgebra/TensorProduct/Basic.lean (which doesn't have this notice, but seems to be the root of the dependency tree here), there is no difference to compile time or maxrss.

[Matthew Ballard]

Oh yeah. You might be able to remove that on current master.

[Matthew Ballard]

With set_option profiler true commenting out suppress_compilation in that file doesn't seem change output.

[Kenny Lau]

@Cameron Zwarich If you look at the original PR that made tensor product noncomputable, it is #7281, and the reason stated is to minimise the total compilation, with the following benchmark:

image.png

And the file with the most instruction reduction was Mathlib.Algebra.Lie.BaseChange.

[Cameron Zwarich]

Thanks @Kenny Lau ! I removed suppress_compilation and noncomputable from enough of that file's dependencies to get it building without suppress_compilation again. With -D Elab.async=false, the elaboration user time for that file goes from 3.90s to 3.91s, and the max RSS goes from 1337840 to 1340080. Seems like whatever problem was there is now fixed with the new compiler.

[Cameron Zwarich]

More generally, I hope that all of Mathlib's uses of suppress_compilation for performance reasons can be removed. If we're aiming for Lean to be usable for increasingly complex SW projects, then we should be able to handle the relatively simple definitions found in Mathlib (especially when a lot of subterms are computationally irrelevant). If there are any remaining issues, I would definitely like to debug/fix them.

[Eric Wieser]

#26642 tries turning off a batch of suppress_compilations, though we'll have to wait a few hours for a benchmark result

[Kenny Lau]

Finally I can remove noncomputable when talking about tensor product!

[Eric Wieser]

I plan to add a Repr and ToExpr instance too, after that lands :)

[Kenny Lau]

is it sound?

[Eric Wieser]

No, but nor is the ToExpr instance on Multiset

[Cameron Zwarich]

Thanks for taking a look at this right after the 4.22 RC! If you find any issues, this increases the chances I can address them in time for 4.23.

[Eric Wieser]

Cameron Zwarich said:

I hope that all of Mathlib's uses of suppress_compilation for performance reasons can be removed.

If this is the case, do you feel the same way about noncomputable? Should there be a CI step that detects noncomputable on things that actually can be compiled after all?

[Eric Wieser]

Results are in: compilation is 7% (40s / ~10 minutes) slower, but that doesn't seem like a big deal

[Cameron Zwarich]

Eric Wieser said:

If this is the case, do you feel the same way about noncomputable?

If it's for performance reasons, definitely. It's possible I'm proven wrong by some definition I haven't seen yet.

Should there be a CI step that detects noncomputable on things that actually can be compiled after all?

Once I fix lean#9021, then this would be pretty simple to do (basically make a mode where noncomputable behaves like noncomputable section, but issues a diagnostic if compilation doesn't fail). Part of my motivation for doing this is to make it easier to detect the root cause of noncomputability through a bunch of noncomputable sections. It should be possible to print the chain of definitions back to the root one that failed (or was explicitly marked noncomputable).

[Cameron Zwarich]

Eric Wieser said:

Results are in: compilation is 7% (40s / ~10 minutes) slower, but that doesn't seem like a big deal

What's the most affected file? I wouldn't mind taking a look.

[Eric Wieser]

There's no per-file compilation time

[Eric Wieser]

But file#Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean in total uses 2.5x as many instructions

[Eric Wieser]

So I guess a reasonable thing to do right now is leave that file with compilation suppressed and merge the rest?

[Eric Wieser]

With trace.profiler, docs#TensorProduct.gradedMul emits:

[Elab.async] [112.428655] Lean.compileDecls ▼
  [Compiler] [112.321887] compiling new: [TensorProduct.wrapped._@.Mathlib.LinearAlgebra.TensorProduct.Graded.External._hyg.3854] ▼
    [] [11.591867] new compiler phase: base, pass: specialize
    [] [1.009664] new compiler phase: base, pass: simp
    [] [0.222378] new compiler phase: base, pass: cse
    [] [0.324857] new compiler phase: base, pass: saveBase
    [] [2.581758] new compiler phase: base, pass: toMono
    [] [1.499076] new compiler phase: mono, pass: simp
    [] [0.102651] new compiler phase: mono, pass: structProjCases
    [] [0.013452] new compiler phase: mono, pass: extendJoinPointContext
    [] [0.081286] new compiler phase: mono, pass: floatLetIn
    [] [0.284566] new compiler phase: mono, pass: reduceArity
    [] [0.481790] new compiler phase: mono, pass: simp
    [] [0.010177] new compiler phase: mono, pass: floatLetIn
    [] [90.545429] new compiler phase: mono, pass: elimDeadBranches
    [] [0.101724] new compiler phase: mono, pass: lambdaLifting
    [] [0.028384] new compiler phase: mono, pass: simp
    [] [0.020180] new compiler phase: mono, pass: cse
    [] [0.037286] new compiler phase: mono, pass: saveMono
    [] [0.026466] new compiler phase: mono, pass: extractClosed

[Cameron Zwarich]

Thanks Eric! Improving the algorithm used by elimDeadBranches was already on my radar for other non-performance reasons.

[Eric Wieser]

Note that I've reverted the change from #26642 which enabled this slowness, in the hope of getting the rest merged

[Eric Wieser]

"most of tensor products are computable" is still a better place to be in than "none of them are"

[Kevin Buzzard]

Did we make TensorProduct irreducible yet? This will surely help.

[Eric Wieser]

I would be surprised if that's relevant

[Eric Wieser]

I thought the compiler only cares about inline, not reducibility

[Eric Wieser]

Eric Wieser said:

Note that I've reverted the change from #26642 which enabled this slowness, in the hope of getting the rest merged

Benchmark is now mostly neutral (6s longer over 10 minutes), so computability is free!

[Eric Wieser]

Eric Wieser said:

I plan to add a Repr and ToExpr instance too, after that lands :)

#26646 has the Repr

[Eric Wieser]

The ToExpr instance is a little cursed, and perhaps is a bad idea

[Kevin Buzzard]

Eric Wieser said:

I would be surprised if that's relevant

Oh. So is the point that irreducibility might help with elaboration, but we're talking about compilation which only happens after that?

[Eric Wieser]

#26786 removes a few more suppress_compilation, though it looks like the speedcenter can't be trusted since very basic files I didn't touch changed signficantly

[Kenny Lau]

how do i effectively search for noncomputable tags that can be removed?

[Eric Wieser]

I would guess this is a bad use of time, and we should make things computable as we need them

[Eric Wieser]

(or until Cameron Zwarich decides to make this a feature upstream)