Using stable release with math project template

Stream: general

[Peiran Wu]

Since mathlib4 has monthly stable releases now, is there a way to create a new project using the latest stable release / a specified release of mathlib with lake? Right now, I have a bash script to which I pass the tag (e.g. "v4.2.0") and which runs lake new <project_name> math, modifies <project_name>/lean-toolchain and adds @"<tag>" to the mathlib reference in<project_name>/lakefile.lean.

Edit: I was confused about what my own script does as it's been a while since I wrote it.

[Peiran Wu]

lake new <project_name> math currently creates a project that uses the latest unstable release of Lean and master branch of mathlib4. Would it not make more sense now to have lake use the latest stable release by default?

[Eric Rodriguez]

I think stability is currently not considered a key feature of Lean, and I think that math by default chooses unstable is okay; on the other hand, I think instructions for pinning stable should be much more clear.

[Peiran Wu]

Sure. I think we shouldn't stop at "instructions". I was trying to find out if I could pin to stable with a single command (e.g. with a command line argument). If not, I think we should make that possible.

[Peiran Wu]

I'll dig up the source code for the math template later. But if someone familiar with the matter could point me there, I would appreciate it.

[Patrick Massot]

Pinning to stable is a very unusual requirement for a math project. Why do you want to do that?

[Eric Rodriguez]

Pinning is useful in many applications, I'm not sure about specifically stable.

[Peiran Wu]

Patrick Massot said:

Pinning to stable is a very unusual requirement for a math project. Why do you want to do that?

Because I want as few Lean toolchains on my machine as possible. If I pin to stable, then I only need that toolchain and another one for working in mathlib4 itself. And I'm not working on anything that needs the latest commits in mathlib4. (Lean's toolchain management is a fork of that of Rust, and I only ever have one Rust toolchain installed at any point. Mathlib is a bit different, so I can tolerate having another toolchain for it.)

[Eric Wieser]

Eric Rodriguez said:

Pinning is useful in many applications, I'm not sure about specifically stable.

The type of pinning that's useful for mathlib is already done automatically by lake-manifest.json though?

[Peiran Wu]

(Why do we have stable releases of mathlib if they are not meant to be used?)

[Patrick Massot]

Peiran, if you want few toolchains then you shouldn't update. The best pinning is to not run lake update.

[Shreyas Srinivas]

If the idea is that an rc toolchain is meant to beta test new changes before making it to the next stable release, it is sensible that people should not have to update to an rc toolchain if they don't wish to test these changes, until they appear in a stable form

[Peiran Wu]

I know this is not a priority for most people and I'm happy to keep using my bash script. My question hasn't been answered yet, but I guess the answer is no, lake doesn't support that yet. In that case, I might do a PR that makes this possible for people who are toolchain-minimliastic like me.

[Shreyas Srinivas]

It is not supported yet and I wish it were

[Shreyas Srinivas]

something like lake update stable which excludes RC releases and lake update latest which will update to the latest release including rc "pre-releases"

[Peiran Wu]

Patrick Massot said:

Peiran, if you want few toolchains then you shouldn't update. The best pinning is to not run lake update.

The problem is that I have projects that start at different points in time and the current toolchain at those times are different. So I'd end up having to update everything when I create a new project

[Eric Wieser]

You can always roll back a new project to the same version you were using in an old project

[Peiran Wu]

Eric Wieser said:

You can always roll back a new project to the same version you were using in an old project

Yes, but that would require the same amount of effort as just pinning the project to stable manually

[Scott Morrison]

There is no lake command for this. It is agnostic about versions of dependencies, and doesn't provide any commands at all for controlling them: you edit lakefile.lean.

The only time lake does anything with a version as far as I know is when you run lake new MyProject math, where the math template is setup to point to mathlib @ master, as that it is most common setup.

[Scott Morrison]

I appreciate that editing lakefile.lean is a difficult requirement for many users, especially as the lakefiles become complicated...