Zulip Chat Archive

Stream: new members

Topic: Lean's processing


view this post on Zulip Michael Beeson (Sep 09 2020 at 22:10):

Does Lean always process my whole file every time I add one more line of code? If so how come it's still working fast enough, now that I have more than 2000 lines of proof? (HOL Light gets crazy slow with a few thousand lines of proof). Lean does make my Mac turn on its fan (sign that it's using all four cores!) sometimes. If I put say the first 1000 lines in another file and import it, will it still be processing that all the time?

view this post on Zulip Mario Carneiro (Sep 09 2020 at 22:12):

It starts from the last statement

view this post on Zulip Kevin Buzzard (Sep 09 2020 at 22:12):

It would be a very good idea to put the first 1000 lines in another file and import it; then the first 1000 lines won't be processed again and again. Yes, Lean can process a lot of a file, or at least the proof you're working on, every time you press a key. Its exact behaviour depends on what you have selected on the bottom row of VS Code ("checking visible files" or "checking visible lines and above" or whatever.

I think that very few mathlib files are 1000 lines long now. Why not split it up?

view this post on Zulip Bryan Gin-ge Chen (Sep 09 2020 at 22:13):

Lean is sent the entire file each time you make a change, but it generally starts re-processing from the last changed line.

view this post on Zulip Michael Beeson (Sep 09 2020 at 22:15):

Thanks Bryan, that clarifies something, but it makes me curious: where does Lean keep the results of its processing? Something like
a bytecode file? But then it must have indexing back to the source so it can figure out what part corresponds to the changed part
of the source file.

view this post on Zulip Michael Beeson (Sep 09 2020 at 22:19):

The set command is working perfectly. Thanks so much for getting me over that hump.

view this post on Zulip Bryan Gin-ge Chen (Sep 09 2020 at 22:28):

I think Lean keeps the results in memory but there are different data structures for files that are open for editing and Lean files that are merely imported. Lean only needs to keep track of the connections between lines of code and the resulting proof terms for the files that are open for editing.

The results of processing can be saved to disk as .olean files if you run lean --make. These are only used for imports, and I don't think they have any indexing back to the original source of the file.

(The above might be all wrong, I haven't read enough of the C++ to know for sure, so I'm mostly guessing based on experience...)


Last updated: May 13 2021 at 20:13 UTC