Speeding up Elaboration

Stream: maths

[Shing Tak Lam]

Hello,

So I've been working on this with @Kevin Buzzard , and one issue that is coming up is how long it takes for Lean to finish checking the file.

https://gist.github.com/shingtaklam1324/7939604394643c1ac1b0e70b0022548e

I suspect it's to do with ring, since commenting out ring and replacing it with sorry in structure_theorem speeds it up significantly, from 11 seconds to 2.

Also, structure_classification takes around 2 seconds to parse. Is this normal?

[Kevin Buzzard]

Nice work! You should update the docstring now you've proved structure_classification. Can you use this stuff to prove the STEP question we started with? That would be a cool finish :-)

But on the other hand I can see that you don't really want to add code at the bottom of the file because the orange bars are getting tedious.

[Background: I wrote the skeleton and Shing proved the theorems]

[Kenny Lau]

yeah don't use ring

[Kevin Buzzard]

So use ten rewrites instead??

[Kevin Buzzard]

Or are they all easy?

[Kevin Buzzard]

If they're all easy, why is ring taking a long time -- @Mario Carneiro do you have any idea?

[Mario Carneiro]

my first guess if ring is slow is the defeq check

[Mario Carneiro]

hm, looks like the default unfolding mode is reducible, it shouldn't really start unfolding unless you use ring!

[Mario Carneiro]

next guess is typeclass inference

[Mario Carneiro]

I try not to use any lean builtin tactics because they all have bad edge case behavior, but it's not 100%

[Mario Carneiro]

oh, we're talking about polynomials, so it's almost certainly typeclass inference

[Mario Carneiro]

One thing you can try is to break out just the statement of the theorem you want to prove by ring as a separate lemma, and see if it's still slow

[Mario Carneiro]

If so, try replacing the base type with a variable of type comm_ring and see if it's still slow

[Kevin Buzzard]

These are great ideas, thanks.

[Kevin Buzzard]

@Shing Tak Lam get in touch with me offline if you don't understand what Mario is suggesting.

[Shing Tak Lam]

Alright that worked. Extracting the goal and proving that separately sped it up significantly. 10ms for the lemma and 2.6 seconds for the main theorem. Much faster than the 11 seconds previously.

[Kevin Buzzard]

Nice.

[Kevin Buzzard]

So now you can update the gist and get to work on doing the STEP question :-)

[Shing Tak Lam]

I'll extract the goal from the other places where it's slow first.

[Shing Tak Lam]

(deleted)

[Scott Morrison]

Yeah, I think the general lesson is that structures are very-super-linear in elaboration time, and breaking out anything but the most trivial of proofs in fields into separate lemmas is a good idea.