Lean won't invalidate its import cache

Stream: general

[Robert Maxton]

Somehow, I've gotten my environment into a state where Lean occasionally just refuses to recompile its imports.

I have two files, A.lean and B.lean, where A imports B. Every now and then, I add some new definitions to B, and then restart A so it can see the changes. Up until last night, this just worked. However, last night I got Lean into a state where Lean refused to notice that B had changed: not when I restarted the file, not when I restarted the server, not even when I restarted the editor (Cursor Nightly) or the whole computer.

Eventually, I managed to get it to compile by removing a blank line from the top of file A, which suddenly seemed to make it 'wake up'. However, the problem has just reoccurred and even 'real' changes to As imports aren't making it rebuild its imports.

I'm currently in the process of nuking .lake and redownloading the cache, but even if that works, I'd like some assistance debugging what's going on.

[Marc Huisinga]

Do you remember if the file was saved when you were trying to use 'Restart File'? There is a bug in Lake right now where it will not rebuild the set of imports in your editor, only those in the saved file.