optimized re-compilations

Stream: lean4

[Arthur Paulino]

I noticed that any change in a lean file triggers a recompilation, like inserting a new line or calling a helper command like #check. Will lean4 be more optimized in these situations? e.g.: not recompile the whole thing if a file change can't change the machine state

[Sebastian Ullrich]

https://github.com/leanprover/lean4/issues/416

[Mac]

@Arthur Paulino are you using leanpkg or lake? leanpkg uses modification times to determine when to rebuild a file so any (asved) change to a file will trigger a recompilation (of dependent/importing modules). lake, on the other hand, uses hash traces where possible, so things like adding a newline or inserting then deleting a temporary command like #check should not trigger a recompilation (of dependent/importing modules).

[Arthur Paulino]

I'm not sure. I'm inside VS Code using this extension: https://marketplace.visualstudio.com/items?itemName=jroesch.lean
In the connectivity.lean file (in the walks_and_trees branch), when I add a new line the vertical orange progress bar signals that it's checking everything from that line and onward

[Arthur Paulino]

ezgif-6-60adf937e85d.gif

[Sebastian Ullrich]

I think there was some prior discussion on enabling that as well. It's doable, but far from trivial.

[Arthur Paulino]

I don't think it's too problematic if the following proofs are light/fast, but could be bothersome for slower/heavier cases

[Wojciech Nawrocki]

Mac said:

lake, on the other hand, uses hash traces where possible, so things like adding a newline or inserting then deleting a temporary command like #check should not trigger a recompilation (of dependent/importing modules).

Why would adding a newline not change the hash? Are you preprocessing the file for whitespace somehow before hashing?

[Kyle Miller]

@Wojciech Nawrocki I believe Mac is talking about hashes of the olean files -- adding newlines triggers recompilation of the module, but if the resulting olean is "the same" it won't cause dependent modules to be recompiled.

[Wojciech Nawrocki]

Ah, I see. The .olean itself would still be recompiled but nothing further would.

[Sebastian Ullrich]

Unfortunately, the .olean file does change because of the embedded file positions. Except of course if, as Mac mentioned as the second example, you revert the change before compiling dependent modules.

[Mac]

@Sebastian Ullrich oh, that is unfortunate. :sad: However, there are still some things, like comment typo corrections that will not trigger full rebuilds of the chain.

[Sebastian Ullrich]

...as long as they are not in docstrings :)

[Johan Commelin]

But if the idea is to split .oleans into "signature-oleans" and "full-oleans", then I guess the embedded file positions could end up in their own olean-variant as well?

[Johan Commelin]

And that embedded-file-position-db-olean might be a lot faster to recompute.