RFC: rename `lake update` to `lake upgrade-deps`

[kim-em]

Proposal

Users continue to injure themselves with lake update. Renaming it to upgrade-deps is both clearer as to what it does, and slightly scarier sounding.

Impact

Add :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.

[kim-em]

update-deps was suggested by @eric-wieser on zulip, but I think upgrade is clearer that it is changing the versions of your dependencies.

[Vtec234]

In my view, this change would take the Lake CLI in the wrong direction. The current command name is in line with what other package managers do, for instance npm update (updates package-lock.json) or nix flake update (updates flake.lock).

The reason why running lake update on mathlib4 continues to cause breakage is that mathlib4 points its require directives at development branches of its dependencies. The standard practice in other package ecosystems is not to do this, but rather point at a specific version of a dependency (or a range of versions that sticks to one major release, precluding breaking changes). It is expected that if any version of a dependency is marked as acceptable, then updating it may introduce breaking changes. The fix should not be to change the CLI, but rather to restrict the versions required in the lakefile. This is not easy to do currently due to package authors not delimiting versions of their packages, and a lack of mechanism to mark breaking changes. I believe that @tydeu was looking into providing support for semver specifications in lakefiles.

[eric-wieser]

I don't fully agree that's the problem here though; even with proper semver in the lakefile.lean, the people running lake update are not intending to upgrade the dependencies, to compatible versions or otherwise. The problem is that the following meaning is assumed:

1. lake update in a project depending on mathlib: "update the mathlib version". This works as expected, and I don't think anyone is complaining about this case. Unfortunately this mnemonic doesn't generalize well, because then we get to...
2. lake update in mathlib itself: "update the mathlib version" (aka git pull). This obviously isn't what actually happens.

I am not for a moment proposing that 2 actually means git pull, but there does seem to be a pattern of people expecting it to mean this, and no amount of semver is going to help with that.

The two easiest ways to fix this, IMO, are:

• rename the command to make it harder to falsely believe the git pull meaning.
• Add a special error just for mathlib users that tells them the command doesn't do what they think it does (and a --i-know-what-im-doing flag to silence the error and actually update mathlibs dependencies)

[kim-em]

@Vtec234, I think "perfect is the enemy of good" is the correct reaction here to your comment.

It would be lovely if we could have version numbers for the upstream dependencies of Mathlib. But we don't today (there are both good and bad reasons for this --- but the reasons are I think not actually relevant to this discussion). So we need to think about short term solutions that solve the problem of users regularly breaking their systems via lake update. We can open issues or plan roadmaps that intend to revert these short term solutions once we have changed things to enable the long term solutions. But I don't think that "Mathlib should refer to its dependencies via version numbers" is a viable answer today.

[eric-wieser]

But I don't think that "Mathlib should refer to its dependencies via version numbers" is a viable answer today.

I don't think this helps the problem of new users mistakenly running lake update, today or in the distant future; even if all the versions were compatible, they're still going to invalidate their cache of mathlib, and waste hours rebuilding it before realizing something is wrong. And if they get through this, they're going to make a PR to mathlib that edits the lake manifest and we're going to tell them to revert it because it doesn't belong there in the first place.

The problem is that all of our new lean4 users coming from Lean 3 are expecting lake update to mean the same thing as leanproject update did, which is exactly what I outlined above.

Better documentation is unlikely to help these users; they will assume their Lean3 knowledge is transferrable, and just start guessing. To get the message to these users that lake update is not the same as leanproject update, we need to make lake update fail on the command line; either by renaming it, or by making it refuse to run on mathlib without confirmation

[tydeu]

@semorrison You previously approved of my suggestion of a lake update --force invocation to solve this problem, and also expressed an interest in implementing it yourself. Are still up for that? Since this feature comes with a configuration option, the actual change cannot be merged until ABI compatibility in lakefiles is no longer a problem, but I am hoping to solve that this week.

As for the suggestion here of renaming the update command, I am not sold. As @Vtec234 mentioned, the command update is nigh-universally used in other package managers for this behavior, and I do not think we should break that convention. As a side note, Lake does now provide an upgrade alias for update (like NPM does).

[mhuisi]

Just chiming in to note that this would also require effort on the VS Code extension side because it will need to be backwards compatible with both lake update and lake upgrade-deps.

[kim-em]

Another instance of a user misunderstanding the intention of lake update, and borking themselves as a result:

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Lake.20errors.20on.20a.20new.20project/near/422128011

[eric-wieser]

That looks like the actual problem is that lake update resulted in incompatible toolchain versions (because it updates dependencies but not the lean-toolchain)

[kim-em]

Yes, that too --- but if I understood them correctly they never intended to run lake update in the first place. Maybe I misread.