Stream: maths

Topic: Speeding up Elaboration

Shing Tak Lam (Mar 26 2020 at 13:17):

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.

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 (Mar 26 2020 at 13:19):

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 (Mar 26 2020 at 13:43):

yeah don't use ring

Kevin Buzzard (Mar 26 2020 at 13:50):

Or are they all easy?

Kevin Buzzard (Mar 26 2020 at 13:50):

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

Mario Carneiro (Mar 26 2020 at 13:51):

my first guess if ring is slow is the defeq check

Mario Carneiro (Mar 26 2020 at 13:52):

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

Mario Carneiro (Mar 26 2020 at 13:53):

next guess is typeclass inference

Mario Carneiro (Mar 26 2020 at 13:54):

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

Mario Carneiro (Mar 26 2020 at 13:55):

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

Mario Carneiro (Mar 26 2020 at 13:56):

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 (Mar 26 2020 at 13:57):

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

Kevin Buzzard (Mar 26 2020 at 13:57):

These are great ideas, thanks.

Kevin Buzzard (Mar 26 2020 at 13:58):

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

Shing Tak Lam (Mar 26 2020 at 14:03):

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.

Nice.

Kevin Buzzard (Mar 26 2020 at 14:04):

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

Shing Tak Lam (Mar 26 2020 at 14:04):

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

(deleted)

Scott Morrison (Mar 26 2020 at 22:46):

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.

Last updated: May 11 2021 at 16:22 UTC