Lean extension reverts mathlib version

Stream: mathlib4

[Nir Paz]

When I pull the latest version of mathlib it works fine, but as soon as I restart vscode it automatically moves back to the commit I was in, as well as showing an error (or warning): "Lean version changed", with a suggestion to restart lean. When the lean extension is disabled this doesn't happen, so I assume it's related to the error (they also happen at the same time, a few seconds after opening vscode).

[Alex J. Best]

Are you working on a project that has mathlib as a dependency? Or just a git clone of mathlib itself?

[Nir Paz]

A project depending of mathlib

[Alex J. Best]

Then you should use lake update in the root of your project to update the dependencies (including mathlib), rather than a manual git pull

[Nir Paz]

Thanks! Is this documented/explained somewhere? It's a silly mistake but as someone who doesn't know much cs these things can take up a lot of time if they're not shown explicitly

[Nir Paz]

Maybe there should be a list of useful lake commands in the "using lake" page

[Filippo A. E. Nuccio]

One thing that I find very strange is that if one runs lake update while in a clone of mathlib (instead that in a project depending on it), some update takes place (notably in the folder \lake_packages\std) and the manifest changes, so that nothing works any more (the whole library needs to be rebuilt and lake exe cache get does not work). Wouldn't it be possible to raise an error if one calls lake update when in mathlib?

[Ruben Van de Velde]

Can you clarify what happens?

[Filippo A. E. Nuccio]

Sure

[Filippo A. E. Nuccio]

I start with the usual git clone of mathlib4, and everything works on the nose (a part from the PR issue mentioned here. If I simply code . the cacheis already there, and I can immediately work on any file (say, on master if I am just willing to play).

[Filippo A. E. Nuccio]

Then I close VSCode and I do lake update: two updating messages show up

$ lake update
std: updating repository '.\lake-packages\std' to revision 'e3f238c972c1b747e0b7605ff568017e6a5107c5'
aesop: updating repository '.\lake-packages\aesop' to revision 'b601328752091a1cfcaebdd6b6b7c30dc5ffd946'

after which, if I code . everything is red and VSCode tells me I have to rebuild everything, which takes ages of course. If I rather close VSCode and type lake exe cache get, no file is downloaded (because the manifest has changed, I suppose: this I can see by opening the diff view in VSCode).

[Filippo A. E. Nuccio]

If I manually revert the manifest to the one that has been downloaded (before the lake update call) everything is still broken, but lake exe cache get works and then everything is super-fast again.

[Ruben Van de Velde]

Oh, I thought something weirder happened. This is just lake update doing what it says on the tin.

[Ruben Van de Velde]

What made you think that it would do something useful (to you)?

[Filippo A. E. Nuccio]

Sure, I am not claiming anything strange happens. I am just suggesting that lake update raises a warning if you try to do it while on mathlib.

[Filippo A. E. Nuccio]

Ruben Van de Velde said:

Oh, I thought something weirder happened. This is just lake update doing what it says on the tin.

I called it by mistake, but it seems quite an innocuous call (it should just 'update' stuff and if one has just downloaded a fresh copy, it is a honest guess to suppose that nothing bad will happen, no?)

[Patrick Massot]

This has nothing to do with mathlib. lake update is the most disruptive command you can run. You should never type it randomly. Lake itself used to recommend running it whenever something was wrong but my hope is this is no longer true.

[Richard Copley]

lake build also checks out libraries to the version specified in the manifest.

[Filippo A. E. Nuccio]

Patrick Massot said:

This has nothing to do with mathlib. lake update is the most disruptive command you can run. You should never type it randomly. Lake itself used to recommend running it whenever something was wrong but my hope is this is no longer true.

Well, the only point I was trying to make is that it might help people to see a message explaining that "lake update is the most disruptive command you can run. You should never type it randomly". I can live with it and can solve my problem when VSCode is all red. I hope this is the same for all new members.

[Eric Wieser]

Would renaming to update-deps resolve the confusion here?

[Scott Morrison]

That's a pretty good idea!

[Scott Morrison]

I think there is now a mechanism to have libraries declare special hooks to run on lake update, and Mathlib could provide one that warns you are breaking everything.

[Scott Morrison]

I'd prefer not to implement this myself, but nominate @Patrick Massot to do so, so he can leave an appropriate trail of issues behind if there are difficulties either discovering where this mechanism is, how it is documented, or how it works. :-)

[Scott Morrison]

Of course, anyone who would like to should do it!

[Scott Morrison]

Proposal to rename lake update to lake upgrade-deps at lean4#2726.

[Scott Morrison]

If there was a verb like "upgrade, almost surely breaking my project as a result", we could try that. :-)

[Patrick Massot]

Scott, I think the hook you have in mind is a post-update hook, not a pre-update hook.

[Scott Morrison]

Do we need that too? If so, let's ask for it.

[Filippo A. E. Nuccio]

Scott Morrison said:

If there was a verb like "upgrade, almost surely breaking my project as a result", we could try that. :-)

Simply a warning like "this is likely to break your project unless [add some cases where it is safe]: are you sure you want to proceed: Y/N" and then execute it if Y?

[Eric Wieser]

What did you (or other people who ran it and got unpleasantly surprised) expect the command to do?

[Filippo A. E. Nuccio]

In general, I would expect lake update to update the mathlib version my project depends on. If I run it on mathlib, I would hope it to do nothing (or simply a git pull) but I understand this is not the way it works, which is fine. The warning seemed to me to be a good way to avoid using it for wrong purposes.

[Eric Wieser]

It sounds a bit silly, but maybe we should really hard-code Mathlib in lake such that on mathlib specifically, lake update errors with a message, and only lake update --i-know-this-isnt-git-pull works...

[Eric Wieser]

Likely in the short term only Scott will be running lake update on mathlib anyway

[Scott Morrison]

Mac is fairly adamant against hardcoding Mathlib into Lake, and I agree that in an ideal world this is a good aspiration. My preference would be that we did hardcode exceptions for Mathlib into Lake, opening issues for each such exception we make, asking for a generic solution (which presumably required more work) to come later.

[Scott Morrison]

I don't think it's unreasonable for users to hope that running an update command will not break their setup. Even if they consider the possibility that it is upgrading the versions of dependencies, they might reasonably hope that we have provided them with a sufficient safety net of version compatibility guarantees (which of course don't exist in the real world!) that it is safe to do so.

That is, we should be designing the convenient and user-facing interface for lake around the most naive beginners. The expert users of course need to be able to do what they need to do, but it is very difficult when designing these tools to remember to prioritize the beginner experience.

[Kevin Buzzard]

We hardcoded mathlib into leanproject and I literally recall nobody ever complaining. That was the setup for years. What do you think about mathematician users forking lake? I suspect that this would also be a very unpopular decision in some parts? But even now I believe that lake still gives really lousy (ie "do what lake says and break your project") advice for projects which depend on mathlib and other projects. I just know from experience not to ever ever ever type lake update without saying what I want to update.

[Eric Wieser]

But even now I believe that lake still gives really lousy (ie "do what lake says and break your project") advice for projects which depend on mathlib and other projects. I just know from experience not to ever ever ever type lake update without saying what I want to update.

I'm pretty sure this is no longer true, and hasn't been for a month or more

[Eric Wieser]

If you have a project that depends on mathlib then lake update will in almost all cases do exactly the same as lake update mathlib

[Eric Wieser]

It is still true that it doesn't touch lean-toolchain and breaks your project until you update yourself

[Scott Morrison]

Eric Wieser said:

It is still true that it doesn't touch lean-toolchain and breaks your project until you update yourself

And this is the part that can be solved by a post-update hook now! @Patrick Massot? :-)

[Scott Morrison]

Just noting that there is parallel discussion going on in the thread at lean4#2726

[Eric Wieser]

Digging deeper (as explained in the issue Scott links); I think this is less of an issue of confused beginners, and more of (experienced?) Lean 3 users who expect their leanproject update muscle memory to transfer to lake update, but on mathlib specifically it does not.

[Patrick Massot]

Scott Morrison said:

And this is the part that can be solved by a post-update hook now! Patrick Massot? :-)

Very easy, let me take a look at the lake README to see the documentation of this feature... Then spend five minutes trying to add this postUpdate? option everywhere in the Lake file before going to the git history of lake, searching for the API change that did not get reflected in the README. And now it's dinner time.

[Patrick Massot]

I opened #7846, but I want to wait until CI provides oleans to be able to actually test this code (which is mostly lifted from the postUpdate docstring in lake).

[Patrick Massot]

And I opened lean4#2735 for the lake README issue.

[Kevin Buzzard]

Eric Wieser said:

I'm pretty sure this is no longer true, and hasn't been for a month or more

Oh, then I apologise for this false accusation. I've been out of the loop for nearly a month because of teaching. Sorry.

[Scott Morrison]

Patrick Massot said:

I opened #7846, but I want to wait until CI provides oleans to be able to actually test this code (which is mostly lifted from the postUpdate docstring in lake).

:ping_pong:

[Patrick Massot]

To be honest I'm not quite sure how to test that code in a real situation.

[Patrick Massot]

And the new VSCode extension made it a lot less urgent.

[Eric Wieser]

#8243 looks like another attempt at the same thing

[Patrick Massot]

Indeed.