lake clean

Stream: lean4

[Arthur Paulino]

Is there a specific reason why lake clean doesn't wipe out the lean_packages folder?

[Mac]

It is designed just to remove build outputs, not dependencies. Also, why would you want to delete lean_packages anyway? Furthermore, there is an important file in lean_packages, manifest.json that should not be deleted (and should be commited) as it helps with reproducible builds. Hopefully that makes sense?

[Arthur Paulino]

I was getting a mysterious error because I was bumping the toolchain and a wrong version of a dependency was sticking in my lean_packages folder. So I had to delete it manually anyway

[Arthur Paulino]

The proper solution seems to be running lake update, in case someone else faces this issue of out-of-date dependencies

[Bhakti Shah]

does lake clean do something other than rm -rf build? I've been getting different build results for the two commands and from the description on the lake repo it isn't clear if it's doing something else.

[Mac Malone]

@Bhakti Shah lake clean does what is essentially rm -rf build for both the root package and all its dependencies. Running rm -rf build from the root of the package will just delete the build directory for the root (not its dependencies), so that may explain the difference. Also, on Windows, lake clean is a bit weaker than rm -rf build because it cannot delete files if they are already in use (e.g., an olean loaded by a module being edited in VSCode). This is due to limitations with the programming primitive used by lake clean.

[Bhakti Shah]

Thanks!