Zulip Chat Archive

Stream: maths

Topic: Speeding up Elaboration


view this post on Zulip 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.

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?

view this post on Zulip 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]

view this post on Zulip Kenny Lau (Mar 26 2020 at 13:43):

yeah don't use ring

view this post on Zulip Kevin Buzzard (Mar 26 2020 at 13:50):

So use ten rewrites instead??

view this post on Zulip Kevin Buzzard (Mar 26 2020 at 13:50):

Or are they all easy?

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Mar 26 2020 at 13:51):

my first guess if ring is slow is the defeq check

view this post on Zulip 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!

view this post on Zulip Mario Carneiro (Mar 26 2020 at 13:53):

next guess is typeclass inference

view this post on Zulip 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%

view this post on Zulip Mario Carneiro (Mar 26 2020 at 13:55):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 26 2020 at 13:57):

These are great ideas, thanks.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 26 2020 at 14:03):

Nice.

view this post on Zulip Kevin Buzzard (Mar 26 2020 at 14:04):

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

view this post on Zulip Shing Tak Lam (Mar 26 2020 at 14:04):

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

view this post on Zulip Shing Tak Lam (Mar 26 2020 at 14:07):

(deleted)

view this post on Zulip 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