Changing lakefile.lean forces rebuilding entire project

Stream: lean4

[Michael Rothgang]

Changing the lakefile.lean in a trivial way (such as, changing a doc comment or the definition of an executable defined there) makes lake build rebuild the world: is this expected or known?

This is obviously not very high priority, but if fixing it is easy, it might be worth it.

[Yaël Dillies]

In general this is necessary because you might have changed some Lean options, right?

[Michael Rothgang]

Sure; I agree that rebuilding the entire project is needed in the general case. My complaint request is that lake seems to always rebuild, with no notion of "no relevant changes were made, so let me skip this".

[Damiano Testa]

I agree with the sentiment, but I think that measuring what counts as "no relevant change" is very hard.

[Damiano Testa]

Specifically to doc-comments, those are involved in some linters, so that would be even harder to check what counts as "irrelevant change".

[Damiano Testa]

Maybe, whitespace/comments-only changes? And applicable to every lean file, not just lakefile.

[Michael Rothgang]

How about "only changes to executables"? In my case, I was renaming the checkYaml executable, which is not used at all for building mathlib.

[Michael Rothgang]

Would some kind of incremental compilation be able to detect this?

[Mac Malone]

Lake should not rebuild things just because the configuration file changed. Do you have a #mwe?

[Mac Malone]

I have not experienced this beahavior before, so I am curious as to the context in which this occurs.

[Michael Rothgang]

Mac Malone said:

Lake should not rebuild things just because the configuration file changed. Do you have a #mwe?

I do: mathlib PR #14892 - the workflow run reveals that CI was rebuilding all of mathlib. (The "build mathlib" step should have taken less than two minutes, all of cache, instead of 45.) All I did was renaming the checkYaml executable, which has no bearing to building mathlib itself.

[Michael Rothgang]

I can reproduce the same locally (on my linux notebook).

[Michael Rothgang]

It's good to hear that this is meant to be different - gives me hope this might be fixed :smile:

[Sebastian Ullrich]

You're blaming the wrong software - this shows that cache does not work as expected, not Lake

[Michael Rothgang]

I see - I apologise to lake then. @Mario Carneiro Can cache get fixed? How difficult would this be?

[Eric Wieser]

My understanding was that cache doesn't have access to Lake's data, and so the best effort thing to do is assume the data changed if the lakefile changed

[Mac Malone]

Michael Rothgang said:

I can reproduce the same locally (on my linux notebook).

Locally, lake exe cache get should only be run on a fresh checkout (of a git commit w/o without changes). After making changes, a lake build should only rebuild the changed files. There should not be a need to run lake exe cache get after making local changes, so the cache invalidation should not matter much.

[Kim Morrison]

Hmmmm, I think I disagree with this advice. I regularly, and successfully, run cache get on modified branches, expecting to get oleans for every thing prior to the changes.

[Mario Carneiro]

I think it is a bad idea to mix changes to the lakefile and "mathematical" changes which would need lots of cache files. In the past it's usually been for either maintenance changes or new tools, neither of which really needs mathlib to be compiled locally