lake update

Stream: mathlib4

[Yaël Dillies]

I often get a prompt from Lean and from lake to run lake update. However, my understanding is that the only occasion where one should run this command is when bumping mathlib. Can we turn off those warnings for mathlib to avoid many people accidentally running lake update?

[Yaël Dillies]

Or is the consensus that these warnings will appear way less once Lean 4 has stabilised?

[Sebastian Ullrich]

It's not really about stability of Lean 4 but of mathlib4 dependencies. Which of course should get more stable as well. It would also be possible to suppress this by making Lake more like Nix' --override-input, storing both the original and current source of a dependency in the manifest so that it can detect whether someone changed the lakefile or manifest and warn only in the former case.

[Sebastian Ullrich]

In fact Nix auto-updates the lockfile when it detects that the equivalent of the lakefile has changed, which I think is the right call

[Gabriel Ebner]

(deleted)

[Gabriel Ebner]

storing both the original and current source of a dependency in the manifest so that it can detect whether someone changed the lakefile or manifest and warn only in the former case.

Ah, I didn't realize that this was for --override-input, clever.

[Gabriel Ebner]

@Yaël Dillies The current warning is a windows-only bug. The lake-manifest.json says the packages directory is ./lake-packages, while on windows we get .\lake-packages.

[Yaël Dillies]

Ahah. So I assume this will eventually get fixed.