chronic problems with "imports out of date"

Stream: new members

[alcuin]

I initially had some issues with lean4 constantly rebuilding my imports every single time I changed them at the top of my file, as in forcing me to sit down and wait as 1400 different modules got rebuilt.

After futzing around with lake exe cache get seeming to have no result I came upon the following workflow:

1. run lake +stable myProject math
2. cd myProject && lake exe cache get

This at least stopped the immediate issues, but now after working on my project for a while I'm somewhat back to the status quo ante because now it still says "Imports are out of date // restart file" after a while.

Is there a straightforward flag to set or something to stop this from happening so I don't have to haplessly wait for the build to finish before I can start filling in tactics again?

[Yaël Dillies]

If lake exe cache get seemingly does nothing, it's possibly because you have corrupted olean headers. One solution is to remove the incriminating file by hand. But it's annoying to try figuring out which one it is, so I usually do rm -rf .lake within my project folder :boom:

[Yaël Dillies]

Then I rerun lake exe cache get and things usually work

[Kent Van Vels]

Thank you, I had the same issue today. Your solution worked.

[Kent Van Vels]

I just tried a "lake clean" followed by "lake exe cache get
and then "lake build". That worked too. I get nervous typing "rm -rf".