Recommend way to add mathlib master as lib?

Stream: new members

[Shanghe Chen]

Hi! Say I want to add the master branch of mathlib as lib like require mathlib from git "https://github.com/leanprover-community/mathlib4"@"master" in the lakefile.lean file. What’s the recommend way to update it regularly?

[Shanghe Chen]

I found that the directory .lake/package/mathlib is checked out directly on a specific commit. Currently I update it via removing lake-manifest.json and rerun lake exec cache get. Is it the correct way?

[Utensil Song]

Are you aware of lake update Mathlib? Or preferably if you need doc-gen4, lake update -R -Kenv=dev Mathlib.

[Utensil Song]

See also lake's new TOML configuration if it's a simple project.

[Shanghe Chen]

Ah I don’t pay attention to lake update before. Yeah it’s quite simple:big_smile:

[Utensil Song]

Never use lake update without a specific package name, it might have unexpected result on other packages, and it could become non-trivial to fix manually, unless you know how git and lake work regarding this very clearly.

[Shanghe Chen]

Oh thank you for bringing this to my attention. I hadn’t realized it either.

[Eric Wieser]

Utensil Song said:

Never use lake update without a specific package name, it might have unexpected result on other packages, and it could become non-trivial to fix manually, unless you know how git and lake work regarding this very clearly.

I think this is outdated advice; if your package only has mathlib as a dependency, then lake update will do the right thing.

[Eric Wieser]

(long ago, this was not the case, and it would update all the dependencies of mathlib to random versions incompatible versions too)

[Rémy Degenne]

I can confirm that I use lake update without any package argument in my projects (well, lake -R -Kenv=dev update more precisely, because of doc-gen) and it works fine.

Although last time it broke everything, but adding mathlib to the command also broke everything. I had to change the toolchain by hand but I have no idea why. See here: https://github.com/RemyDegenne/testing-lower-bounds/pull/28 if somebody want to investigate.

[Utensil Song]

This and this are very recent. :joy:

[Utensil Song]

Personally I do run lake update since I can fix it if anything goes wrong, but mostly as lake update -R -Kenv=dev. I'm just still not so confident to recommend a raw lake update to others.

[Rémy Degenne]

Indeed one should be careful with that command. When I write that "it broke everything", I mean that the only way I could recover was by deleting the local repository and cloning again: never run lake update if your local work is not saved somewhere else.

[Utensil Song]

I can fix them with some git stash, git reset --hard, git cherry-pick -n, git push -f like combos (some are dark magic) without re-cloning, but re-cloning is cleanest to recommend to others.

[Yaël Dillies]

FWIW my script to update LeanAPAP is

curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
lake -R -Kenv=dev update

and it has never failed me so far.

[Utensil Song]

Rémy Degenne said:

I can confirm that I use lake update without any package argument in my projects (well, lake -R -Kenv=dev update more precisely, because of doc-gen) and it works fine.

Although last time it broke everything, but adding mathlib to the command also broke everything. I had to change the toolchain by hand but I have no idea why. See here: https://github.com/RemyDegenne/testing-lower-bounds/pull/28 if somebody want to investigate.

Inspecting the PR, by breaking everything, it seems to mean just that the recent updates of Mathlib will need to change some user-side code to build? That's usually a disrupting process for ongoing work, but if one has some proper time for a bump, when everything builds again, it's pure joy.

[Rémy Degenne]

The breakage is not visible by looking at the PR. I mean that if you get the repo in the state it was before that PR, then try to update without changing the toolchain first, the update command does not even succeed. You get errors mentioning the aesop package (I don't have the precise error messages anymore).

[Utensil Song]

That's similar to this.

[Utensil Song]

Yaël Dillies said:

FWIW my script to update LeanAPAP is

curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
lake -R -Kenv=dev update

and it has never failed me so far.

This script dodged that issue. So, indeed, one must bump toolchain file first before any lake update* commands.

[Eric Wieser]

Utensil Song said:

This and this are very recent. :joy:

This one is a case where there is non-trivial scripting going on in the lakefile.lean, which in mathematical (as opposed to infrastructure) projects is rare.

[Joachim Breitner]

Incidentally, the live.lean-lang.org setup also settled on the delete manifest - download toolchain - build idiom.

I guess if you have only one dependency, and you are upgrading, then there is no useful information in the manifest and the stateless approach works more reliable.

This changes if you have more than one direct dependency and the manifest contains valuable information about a curated combination of versions.

[Patrick Massot]

Eric Wieser said:

I think this is outdated advice; if your package only has mathlib as a dependency, then lake update will do the right thing.

I think it is strategically bad to start teaching people how to update mathlib in one way if they have no other dependency and another way if they have other dependencies. We should only teach the command that work in both cases and makes the intention clear.

[Eric Wieser]

I think if people depend on both mathlib and another package, they are likely to have a bad time whatever we tell them

[Eric Wieser]

(At least, if the other project is just as picky about the Std / toolchain version as mathlib is)

[Utensil Song]

So far, depending on both Mathlib and Duper matches your description.

[Patrick Massot]

Many projects depend on Mathlib and checkdecls (all projects with a modern blueprint). And one can imagine other tiny libs like checkdecls adding one gadget.