Lean's processing

Stream: new members

[Michael Beeson]

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?

[Mario Carneiro]

It starts from the last statement

[Kevin Buzzard]

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?

[Bryan Gin-ge Chen]

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

[Michael Beeson]

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.

[Michael Beeson]

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

[Bryan Gin-ge Chen]

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...)