lake update nukes entire project

Stream: general

[Christian Merten]

When minimizing this error, I stumbled upon this behaviour:

• Run

lake new bar
cd bar
mkdir docbuild
cd docbuild

• Copy lakefile.toml from the README to lakefile.toml.
• Run lake update doc-gen4.

This nukes the entire contents of the bar folder!

The error happens because "Your Library Name" does not exist, the precise error message is:

error: '«Your Library Name»' was downloaded incorrectly; you will need to manually delete './././../': directory not empty (error code: 39)
error: docbuild: package 'bar' was required as '«Your Library Name»'

This is of course fine and a user error, but nuking the entire project is maybe a bit much of a punishment :)
(Also local git history does not help here, since .git is also deleted).

[Christian Merten]

I guess this line should only be executed for downloaded dependencies, not local paths.

[Eric Wieser]

I think if matDep.manifestEntry.src matches .git .. then on the line above the one you link to is intended to protect against precisely that

[Christian Merten]

Ah and this was fixed in lean4#5878, but I had not done elan update in a while, so stable pointed to 4.12.0 which is older than lean4#5878.