[question] How to "cache" previous edits when changing LEAN file

[realharryhero]

The motivation for this is that it would be useul to interact with LEAN by, for example, deleting or adding some definitions, from an external source such as LeanDojo. To interact with theorems in an external API such as LeanDojo, one has to trace the entire repo first - and if even one definition is changed, the entire repo would need to be traced again, even with minimal differences in the actual file. As an analogy, it would make sense to change equipment or items in addition to training in a dojo, much like it would be a good idea to change the "theorem" equipment in a LeanDojo as well.

Tracing a LEAN repo through LeanDojo, among other things, essentially "compiles" the entire lean repo, associating a compiled .olean file to each .lean file. Most likely the .olean file is only slightly changed after changing a definition in a specific way, and hence it would make sense to, instead of creating the entire .olean file from the .lean file, changing the current .olean file in another specific way.

Based on the fact that in the LEAN InfoView, when I add some definitions to the end of the file the InfoView doesn't go through the entire LEAN file (the number of messages (sorries, etc.) does not go from 0 to a large number after a small edit, so most likely it isn't re-precompiling everything), it seems that LEAN already has a way to do this.

What piece of code allows one to, given a small change to a .lean file and their corresponding .olean files, use the previous .olean file to make a new .olean file?

[digama0]

What piece of code allows one to, given a small change to a .lean file and their corresponding .olean files, use the previous .olean file to make a new .olean file?

This is not possible. You need more information than is contained in the .olean file to perform this operation efficiently. What the server does is to build up an in-memory data structure called the info tree which contains information about elaboration of all intermediate states, and when you make a modification in the middle or end of the file it retrieves one of these intermediate snapshots and uses it as the starting point instead of rebuilding the whole file. This data is not persisted to disk, so the only way to make this work effectively is to have a lean process hanging around holding this information. If you have no running lean process and just a bunch of .lean and .olean files, you will have to go through the building process (although only for that one file, not its dependencies - for imports .olean files are sufficient) before you can process a new or modified definition in the file.

[realharryhero]

Great explanation, thank you very much!

[realharryhero]

Sorry, another question; say I want to delete a theorem, and all the theorems that use a tactic that relies on this theorem. I have the ability to remove such theorems in the .lean files, but I cannot do so in the .olean files.

Since I'm just removing theorems and their dependencies, it's really only removing information from the .olean file; furthermore perhaps the .olean file is structured like a .lean file, so that I may be able to simply delete the part of the .olean file that contains that theorem.

Is there a way to remove a theorem from a .olean file by removing some specific piece of text, given I can remove a theorem in the associated .lean file by removing specific text from the .lean file? I believe this is a special case of my first question, where unlike that question no other theorem/defintions will then depend on the theorem/definition I want to change.

More abstractly, would there be a way to, instead of remembering all intermediate states, compile each theorem from top to bottom, and then once the file is changed, only recompile the theorems in the file that depend on the changed theorem?

[digama0]

In theory you could do this, but lean is not really designed for it and there is no function to do so. The .olean file is not a text file, it is more like an in-memory data structure serialized to disk, so it has pointers in it which would have to be relocated. The easiest way to do this would be to load the file, delete the element you would like to delete, and then write it using the .olean writer, which will re-compact everything and fix the pointers. You can do this without actually constructing an Environment object.

PS: For general questions about lean, it is recommended to use https://leanprover.zulipchat.com instead of the github issue tracker.

[nomeata]

Thanks for your interest in Lean, but as Mario says, questions are better posted in the zulip chat.