Lake deleted my stuff

Stream: lean4

[Max Nowak 🐉]

This is technically user error on my part, but I did the following in my lakefile: require stuff from "../Stuff", ran lake update, and the next thing I see is my entire Stuff folder getting deleted, including its .git subdirectory. I'm on Lean 4.12. I imagine those files are now unrecoverable?

[Henrik Böving]

Those files should certainly be recoverable. A mere rm does not actually touch the content on disk but just marks it as "overwriteable if required" so unless you continued doing a lot of writes afterwards and have bad luck we should certainly be able to recover stuff. I would recommend to shutdown your system and boot from a live distro, then run recovery tools such as photorec to try and see if they are still on your drive.

[Max Nowak 🐉]

Ah, oof. I lost my last commit, but I think it'll be less effort to just re-do that by hand. Thanks though

[Junyan Xu]

The second time this bug was rediscovered recently. I assume no server is still distributing the buggy lake version now, but it might still be present on many people's local machines? I forgot whether and when this appeared in the #announce channel; maybe the topic should be pinned to remind everyone to check their lake version?