Zulip Chat Archive

Stream: new members

Topic: Lean package release policy?

Michał Dobranowski (Sep 17 2025 at 12:41):

Hi, I was wondering what the release policy for a Lean package should be. When I create a new project using lake new ... math, Lake sets up some GitHub actions that automatically create tags and releases matching the Lean and mathlib releases (like v4.23.0 or v4.24.0-rc1).

But there’s also a version field in lakefile.toml (default is v0.1.0), which shows up in Reservoir. It seems natural to make a GitHub release (and add a git tag) whenever I bump this version, but that would conflict with the tags created by the default actions.

So what’s the recommended approach here?

Emily Riehl (Sep 17 2025 at 13:08):

A related question. When a new Lean version is announced, what do I need to do?

Specifically:

  1. I have a fork of mathlib. What do I need to do there?
  2. I have a Lean project using @Pietro Monticone's Lean Project template. What do I need to do there?

We've been through this before but long enough ago that I've totally forgotten.

Riccardo Brasca (Sep 17 2025 at 13:37):

lake update takes care of updating all the dependencies of your project. You only need to do lake build and fix the proofs that broke.

Ruben Van de Velde (Sep 17 2025 at 13:38):

For 1- nothing

Riccardo Brasca (Sep 17 2025 at 13:39):

You can essentially ignore new releases of Lean, just do lake update often to update mathlib, and sometimes Lean will also be updated, but you don't need to care.

Riccardo Brasca (Sep 17 2025 at 13:39):

Sorry, after lake update you need lake exe cache get

Riccardo Brasca (Sep 17 2025 at 13:39):

Otherwise you recompile everything

Ruben Van de Velde (Sep 17 2025 at 13:40):

Doesn't lake update do that by default now?

Riccardo Brasca (Sep 17 2025 at 13:40):

Ah it's possible

Ruben Van de Velde (Sep 17 2025 at 13:41):

Still, better to run it once too many than not enough

Riccardo Brasca (Sep 17 2025 at 13:42):

Yes, it does it automatically

Michał Dobranowski (Sep 17 2025 at 13:54):

Do you know the answer to my original question?

Ruben Van de Velde (Sep 17 2025 at 13:56):

"We're thinking about it", is my most recent understanding

Emily Riehl (Sep 17 2025 at 14:34):

In the fork, does lake update subsume git pull followed by lake exe cache get? And does it make a difference whether I run this from master or from another branch?

Emily Riehl (Sep 17 2025 at 14:34):

This is usually what I do when (I think) I'm bumping mathlib.

Ruben Van de Velde (Sep 17 2025 at 14:36):

No, within mathlib, you should never run lake update

Emily Riehl (Sep 17 2025 at 14:39):

Got it. So this is just something for Lean projects then.

Emily Riehl (Sep 17 2025 at 14:40):

While we're here. What is lake? I've always imagined it's some sort of make for Lean. (Disclosure: I don't really know what make files are supposed to do.

Riccardo Brasca (Sep 17 2025 at 14:47):

Suppose that you have your project BigTheorem, that depends on mathlib. Inside the BigTheorem forlder, lake update will update mathlib (and Lean if needed) but it will not do anything to your project. After this you have to run lake build to make sure your project works with the new version, and once everything works you commit and push as usual (you will notice that lake changed the lakefile, you have to commit this change, but otherwise you can ignore it). There is no need to pull anything during this process.

Riccardo Brasca (Sep 17 2025 at 14:48):

On the other hand, if someone else (or yourself with another computer) modifies something in your project you need git pull to get the new version.

Riccardo Brasca (Sep 17 2025 at 14:49):

One think to keep in mind is that, if the modification you get with git pull is a bump, done by someone else, you need lake exe cache get, otherwise you have red bars everywhere.

Riccardo Brasca (Sep 17 2025 at 14:50):

You can think to lake as the software that allows you to handle Lean projects.

Michał Dobranowski (Sep 17 2025 at 14:59):

Ruben Van de Velde said:

"We're thinking about it", is my most recent understanding

Do you know of any actively developed projects that use the version field and have solved this problem?

Ruben Van de Velde (Sep 17 2025 at 15:00):

I don't

Eric Wieser (Sep 17 2025 at 15:18):

Note that just running lake update is bad advice if you think there is any chance anyone else wants to use your project

Eric Wieser (Sep 17 2025 at 15:19):

You should instead do the following:

  • modify your lakefile to pin mathlib to @ "git#v4.23.0" (or whatever the version is)
  • run lake update
  • fix everything and commit
  • Optionally remove the @ "git#v4.23.0" and re-run lake update, if you want to go to the bleeding edge

Jakub Nowak (Sep 18 2025 at 00:23):

Eric Wieser said:

  • modify your lakefile to pin mathlib to @ "git#v4.23.0" (or whatever the version is)

Isn't lake-manifest.json supposed to pin mathlib to the latest version? What's the difference if I pin it manually in lakefile?

Eric Wieser (Sep 18 2025 at 01:19):

That won't pin any of the dependencies to the right versions

Eric Wieser (Sep 18 2025 at 01:20):

You could manually pin every dependency in the manifest, which is fragile; but if you do it in the lakefile instead, lake update will do the work for you.

Jakub Nowak (Sep 18 2025 at 11:10):

What is right version? You mean it will pin to latest commit, instead of release version?

Eric Wieser (Sep 18 2025 at 11:12):

"right version" means that if you depend on A and A depends on B, then you get a version of B that A claims works with it

Last updated: Dec 20 2025 at 21:32 UTC