Setting up "modern" lean with a nonstandard repo layout

Stream: general

[Mario Carneiro]

I'm trying to upgrade the lean part of the MM0 repo, https://github.com/digama0/mm0/tree/master/mm0-lean . Currently it is set up in a completely nonportable way, using leanpkg.path directly, but lean/mathlib breakage has been pretty high in the last 10 versions or so and now I want to explicitly declare the version of lean that I compile to so that other people can at least load it (and also so that I can see how it used to build so that I can fix the proofs). But leanproject seems to not want to even touch my setup unless I put it in its own repo, and I don't want to do that. Is there a way to set up leanpkg.toml to select the right version of lean and mathlib, get a _target directory and so on, without also getting the version control stuff?

[Bryan Gin-ge Chen]

mathlib-tools#42 is related, I guess.

[Mario Carneiro]

Do I need leanproject?

[Mario Carneiro]

or is plain lean just completely useless now

[Mario Carneiro]

aha, leanproject works as long as I put the toml file at the root of the repo

[Rob Lewis]

I think you can probably just drop a leanpkg.toml in the root, no?

[Mario Carneiro]

is there an easy way to switch to a version of mathlib from the past? I want to check out mathlib as of a year ago to see if it builds

[Rob Lewis]

Copy the commit sha into leanpkg.toml and change the Lean version

[Rob Lewis]

I guess in principle there could be a command that takes a sha and figures out the Lean version from that, but I don't think it exists.

[Rob Lewis]

leanproject will find you olean caches for most mathlibs since March, and before then anything that was a nightly

[Rob Lewis]

But that's kind of hard to identify

[Rob Lewis]

Oh no, I guess it's not so hard, anything here: https://github.com/leanprover-community/mathlib-nightly/releases

[Julian Berman]

⊙  git show e79396731:leanpkg.toml | toml2json | jq .package.lean_version                                                                                                                                                                                                                                                                                        julian@Home
"3.4.1"

[Rob Lewis]

Julian Berman said:

⊙  git show e79396731:leanpkg.toml | toml2json | jq .package.lean_version                                                                                                                                                                                                                                                                                        julian@Home
"3.4.1"

Nice, sounds like the core of a new leanproject set-mathlib command.

[Rob Lewis]

Oh, @Mario Carneiro , a simpler way would be just to change the Lean version to 3.4.1 and leanpkg configure should set mathlib to the last commit compatible with that

[Rob Lewis]

If that's old enough for you.

[Mario Carneiro]

I picked a random commit from the end of 2019 and used whatever was in its toml file

[Mario Carneiro]

unfortunately I don't get oleans so now I have to build mathlib

[Mario Carneiro]

and it's exactly as slow as I remember

[Reid Barton]

reproducibly slow builds

[Mario Carneiro]

fun fact, file not found errors abort the build even if there are other nondependent files that can be built

[Mario Carneiro]

i.e if B.lean imports A.lean (which doesn't exist) and C.lean imports nothing, C.lean won't be compiled because of the file not found error in B