noncomputable for performance

Stream: lean4

[Eric Wieser]

There have been multiple situations now where we've put noncomputable on a definition in mathlib4 not because it uses choice, but because it takes too long for the compiler to compile. Is there a tracking issue for this? Should we be filing issues for when the kernel check is quick but compilation is slow?

[Eric Wieser]

Perhaps the answer to my first question is #7103

[James Gallicchio]

It's great if Mathlib can catch these issues before programming projects get big enough to run into them :big_smile:

[Eric Wieser]

As an extreme example; the noncomputable keyword in #7265 makes things 30x faster

[Matthew Ballard]

Make your lean code 30x faster with this one weird trick

[Alex J. Best]

James Gallicchio said:

It's great if Mathlib can catch these issues before programming projects get big enough to run into them :big_smile:

I wonder if programs that are actually designed to be run would ever run in to these issues though? It seems these issues come from trying to generate code from highly nontrivial mathematical definitions which are fairly nested, which is probably not super nice code at all

[Matthew Ballard]

I don't think anyone has attempted a minimization yet

[Eric Wieser]

Are these any trace diagnostics available to find out which parts of the compiler are to blame here?

[Henrik Böving]

you can trace the new compiler with set_option trace.Compiler true and get proper nested timings etc.

[Henrik Böving]

If it's in the new compiler my bet would be that the simplifier is slow.

[Eric Wieser]

Is "the simplifier" unrelated to simp?

[Henrik Böving]

Yes, although it too is called simp in the compiler trace^^

[Sebastian Ullrich]

(the terminology is from GHC, and perhaps even older than that)