[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!