mathlib4

Stream: lean4

[Jeremy Avigad]

Mathlib4 is just starting to get big enough to be useful. How hard it is to import one project from another when using Lean 4, and what is the right way to do it?

Mathlib4 is currently small enough that I don't mind cutting and pasting the files that I need, but if there's a better way, I'll be happy to try it out.

[Wojciech Nawrocki]

Putting the following in your leanpkg.toml should do it:

[dependencies]
mathlib4 = { path = "/path/to/mathlib4" }

or to fetch from git:

[dependencies]
mathlib4 = { git = "https://github.com/leanprover-community/mathlib4", rev = "5212f0c" }

This should work in VSCode, while on the command line leanpkg build must be used (lean used directly will not know where to find the dependencies).

If you are feeling particularly adventurous, you could also try the new build system - Lake. Note that Lean 4 only imports .oleans and ignores .leans, so if errors happen it's useful to check if the .oleans are present.

[Meow]

Are there some interesting progress in Lean about analytical number theory?

[Jeremy Tan]

Hi, how do I correctly start a mathlib4 project in VS Code on Ubuntu?

[Jeremy Tan]

I mean, I just downloaded Lean 4 through VS Code and I would like to get up and running contributing to mathlib, but only using Lean 4

[Jeremy Tan]

After I run lake init ringel what next?

[Jeremy Tan]

because "leanproject only supports Lean 3. If you are using Lean 4, the information on this page is not relevant."

[Logan Murphy]

You can make a new project depending on mathlib4 with lake new <project_name> math. Or if you have an existing project with a lakefile, you should be able to just add

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"

to the lakefile right above the line containing@[default_target] and run lake update to download mathlib.

[Arthur Paulino]

Note: lake new <project_name> math has to be called with a reasonably recent toolchain or there is a high chance it will start your project with the wrong toolchain

[Arthur Paulino]

https://github.com/leanprover-community/mathlib4#using-mathlib4-as-a-dependency

[Arthur Paulino]

Btw @Gabriel Ebner I just noticed that you added a new step 6:

6. Run cp lake-packages/mathlib/lean-toolchain . to make sure your new project uses the same Lean version as mathlib4.

This isn't necessary due to step 2

[Gabriel Ebner]

@Arthur Paulino No that's not true. "Sufficiently recent" is not enough.

[Arthur Paulino]

Is "at least as recent as ..." enough then?

[Gabriel Ebner]

No, of course not. It needs to be the exact same version.

[Arthur Paulino]

That's not true. Recent toolchains have a fix on Lake that downloads the correct toolchain file for a project that uses the math template

[Arthur Paulino]

https://github.com/leanprover/lake/pull/152

[Gabriel Ebner]

Ah, I forgot about that. However step (5) says to use lake update which does not know about lean-toolchain.

[Arthur Paulino]

What do you mean? lake update should pick the correct toolchain for lake

[Gabriel Ebner]

Last time I checked it didn't touch the file at all.

[Arthur Paulino]

lake update shouldn't touch lean-toolchain. It's the lake new command that creates a project with a correct lean-toolchain file out of the box

[Gabriel Ebner]

Which then becomes incorrect as soon you do lake update (because the new mathlib4 version might require a different Lean version).

[Arthur Paulino]

It's the master version regardless

[Gabriel Ebner]

Which changes regularly?

[Arthur Paulino]

Yes, but then the problem is something else. It's a generalized issue due to pinning master

[Arthur Paulino]

But if you do lake new and then lake update within the same day, it shouldn't be a problem

[Gabriel Ebner]

Pinning mathlib to master and having lake update always get the latest mathlib version is what we want though.

[Gabriel Ebner]

But if you do lake new and then lake update within the same [minute], it shouldn't be a problem

Sure, if you do it quickly enough then both lake new and lake update will see the same version.

[Arthur Paulino]

"quickly enough" = a time window of 24-48 hours

[Gabriel Ebner]

But we need to teach people to set the correct Lean version. Because they'll run lake update themselves later. (Or change lake update to do that.)

[Arthur Paulino]

If that's the case, doing it via cp is a very bad UX

[Gabriel Ebner]

"quickly enough" = a time window of 24-48 hours

Not really. It doesn't matter how frequently we update Lean, if you're unlucky you pick exactly the time where the bump PR lands. (And one minute before bump PR = old version, one minute after = new version.)

[Gabriel Ebner]

If that's the case, doing it via cp is a very bad UX

I agree.

[Arthur Paulino]

Gabriel Ebner said:

"quickly enough" = a time window of 24-48 hours

Not really. It doesn't matter how frequently we update Lean, if you're unlucky you pick exactly the time where the bump PR lands. (And one minute before bump PR = old version, one minute after = new version.)

How realistically likely is that? :joy:

[Arthur Paulino]

Anyways, maybe lake new shouldn't pin to master

[Gabriel Ebner]

That's what people want though.

[Arthur Paulino]

It should pin to the most recent commit when lake new runs

[Gabriel Ebner]

Do you mean set up lake-manifest.json automatically? That seems like a good idea as well.

[Arthur Paulino]

No I mean have a placeholder in the lakefile template that should be replaced by the most recent mathlib4 commit on master

[Arthur Paulino]

If we're gonna talk about teaching people, I believe we should teach them to mindfully update their mathlib4 hashes to get updates. Pinning to master is a flaky idea. It's very prone to errors

[Gabriel Ebner]

But then what's the point of having the lake update command?

[Arthur Paulino]

When you update the hash in the lakefile, run lake update and it will update the manifest and download the correct dependency repo version

[Gabriel Ebner]

How does this make things any easier? With this proposal, you'd need to manually update both the git revision as well as the lean-toolchain file.

[Arthur Paulino]

It's less flaky

[Arthur Paulino]

It's one of the lessons I've learned from managing a less trivial DAG of dependencies

[Gabriel Ebner]

That's the situation we've had before lake update. If you don't want to use lake update, that's perfectly fine and you can still edit everything manually.

[Gabriel Ebner]

I'm so happy that I no longer need bespoke shell scripts that update lakefile.lean using sed.

[Arthur Paulino]

Nah, lake update does git clones for me

[Gabriel Ebner]

There's also lake resolve-deps which iirc does git clones but without the version bumps.

[Arthur Paulino]

IMO, the current behavior of lake update needs to update lean-toolchain according to the most recent lean-toolchain across all dependencies

[Arthur Paulino]

(and don't touch it if the most recent toolchain isn't newer than the current one)

[Sebastian Ullrich]

At one point I was thinking about whether it should be legal for a lean-toolchain to simply refer to another toolchain file as in

$ cat lean-toolchain
./lake-packages/mathlib4/lean-toolchain

... but that's a bit problematic when lake-packages does not exist yet

[François G. Dorais]

@Sebastian Ullrich It should be the other way around where things in lake-packages grab lean-toolchain from the root and then inspect it for suitability. As far as I can tell, lake currently ignores all other lean-toolchain files and only uses the one in root for everything. Maybe the lakefile should contain a kind of toolchain range statement to check compatibility.

[Andrés Goens]

I imagine once things stabilize and lean-toolchain points to a tagged version and not a nightly (and also in mathlib), this issue will not come up as often, but the underlying reason is that we'll probably need a full-fledged package manager at some point, to solve version dependencies, right?

[Sebastian Ullrich]

François G. Dorais said:

Sebastian Ullrich It should be the other way around where things in lake-packages grab lean-toolchain from the root and then inspect it for suitability. As far as I can tell, lake currently ignores all other lean-toolchain files and only uses the one in root for everything. Maybe the lakefile should contain a kind of toolchain range statement to check compatibility.

That doesn't work when you have a dependency like mathlib that a) contains a vast majority of the code of the package tree and so is the most likely point of breakage, and b) comes with an olean cache for a specific Lean version

[Sebastian Ullrich]

@Andrés Goens previously, previously

[François G. Dorais]

Sebastian Ullrich said:

That doesn't work when you have a dependency like mathlib that a) contains a vast majority of the code of the package tree and so is the most likely point of breakage, and b) comes with an olean cache for a specific Lean version

True. Fortunately, "a dependency like mathlib" is a singleton and I can't imagine anything comparable forthcoming. IMHO, that use case is pretty clearly a mathlib problem and not a lake problem. Lean's Pareto Principle is more 99/1 than 80/20. Tough situation indeed!