Running lake update broken everything

Stream: new members

[Alexander Byard]

Hi, I'm newer to Lean and CS in general. I'm a mathematician, so getting up and running with simple things like Bash and Git was a struggle. I have a project, which I used to present for a class, and I have been continuing to use it as I work on learning and developing some new graph theory.

I wanted to work on a functional analysis project, so I needed to update my copy of Mathlib. I think that the correct way to do this is run lake update in the terminal. I don't know if I was supposed to do something with Git first. This stopped everything from working, and the problem is fixed when I revert back to a previous commit using git log --oneline to identify the previous commit I want to revert to, and git revert ____ to do this. I tried running lake update again and I have the same issue. I've attached an image of my Lean Infoview when I try to open IntervalIntegral.lean. For others, like Lebesgue.lean, it simply says "processing stopped".

If anyone can help me update Mathlib, that would be fantastic. : )
Screenshot-161.png

[Ruben Van de Velde]

It seems likely that you updated mathlib but not version of lean4 that corresponds to it

[Ruben Van de Velde]

Try making sure that the lean-toolchain file in your project matches the one in https://github.com/leanprover-community/mathlib4/blob/master/lean-toolchain for the mathlib commit you're on

[Alexander Byard]

They are the same.

[Alexander Byard]

Could it be an issue with how I ran lake update?

Screenshot-162.png

[Alexander Byard]

This is the most recent time I ran lake update. The stuff above it is a previous commit

[Patrick Massot]

Did you run lake exe cache get after running lake update and copying the lean-toolchain file?

[Alexander Byard]

I did not run lake exe cache get. Should I do this? My lean-toolchain file is currently the same as the one sent by @Ruben Van de Velde .

[Eric Wieser]

Should I do this?

Not without ensuring lean has stopped first

[Eric Wieser]

(i.e. by closing vscode and running it from a regular command line)

[Alexander Byard]

@Eric Wieser Is it also an issue that I ran lake update in vscode?

[Patrick Massot]

No, that part is fine

[Alexander Byard]

Okay, let me try it.

[Alexander Byard]

I run lake exe cache get in a separate terminal after vscode has closed. It returns error: no such file or directory (error code: 2) file: .\lakefile.lean

[Eric Wieser]

You need to be in the directory of your project

[Yakov Pechersky]

I think I see why one might think that lake update would be the right thing to do. We have this:
https://github.com/leanprover-community/mathlib4#updating-mathlib4,

lake update; curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain; lake exe cache get

which is really about updating "mathlib4 as a dependency of my other non-mathlib4 project", not "update mathlib4 for its own sake"
and also this:
https://github.com/leanprover/lake#adding-dependencies

To update mathlib after this, you will need to run lake update -- other commands do not update resolved dependencies.

The thing that has always worked for me to update mathlib4 (for its own sake) is git pull; lake exe cache get. That is most like this section in our collective READMEs:
https://github.com/leanprover-community/mathlib4#build-instructions

Perhaps we need better clarity around what "update" means to whom.

[Scott Morrison]

In some sense, no "regular user" of mathlib should ever be running lake update within mathlib. That is really only useful for regular contributors who are doing housekeeping chores (i.e. preparing a PR that bumps dependencies).

I wonder if we can discourage this?

I agree with Yakov's assessment about the documentation in aggregate being confusing. Nevertheless both times there is an instruction to lake update it is in the context of a downstream project that depends on mathlib. (And hence it is correct!) Perhaps in our own README it is slightly unobvious by the time you reach the bottom of the page that you are still in the Using mathlib as a dependency section.

[Scott Morrison]

lake update could check if you have write access to the (remote of the) repository you are running in :-)

[Mac Malone]

Scott Morrison said:

In some sense, no "regular user" of mathlib should ever be running lake update within mathlib. That is really only useful for regular contributors who are doing housekeeping chores (i.e. preparing a PR that bumps dependencies).

I wonder if we can discourage this?

You could have mathlib's lakefile use exact commits in its require statements. That way lake update will not do anything unless the file is edited. To update a library, a maintainer could then remove the exact commit (or change to a branch), run lake update, and then copy the new commit from the lake-manifest back to the lakefile to fix it to the new version.

[Mac Malone]

Alternatively, Lake could get a new package configuration option (e.g., forceUpdateOnly) that would print an error on a bare lake update and require instead lake update --force (which most new users would not accidently type).

[Scott Morrison]

I like the second option!

Perhaps I should try implementing that myself sometime, as a lake learning exercise.

[Sebastian Ullrich]

Adding a flag that is, essentially, --are-you-sure-youre-running-the-right-command sounds like an unorthodox solution to me. If the underlying issue is that the readme is too confusing, the dependency part could be moved to a different file. Alternatively, as I believe has been mentioned before, Lake update could be renamed to upgrade to emphasize its code breaking nature. And ideally no command should be necessary at all to add a new dependency from the lakefile to the manifest.

[Mauricio Collares]

How about mentioning "manifest" explicitly in commands that change it? Say, lake update-manifest. By the way, I agree with the point about new dependencies.

[Mauricio Collares]

Or be more Nix-like and call it lake recreate-manifest

[Scott Morrison]

I agree either upgrade or update-manifest are slightly better.

I think this is a pretty serious issue, when you keep in mind all the "new users" (particularly students) who are going to break their Lean setups by typing something innocuous/appealing sounding.