tagged releases?

Stream: mathlib4

[Siddhartha Gadgil]

As courses using Lean 4 will start in a couple of weeks (including mine), I would like to suggest having periodic tagged commits. Just a lightweight tag is fine. This is so lakefile.lean in a course repository can point to tagged versions to ensure compatibility.

Specifically, what would be nice is for coordinated labels for mathlib, Std, Qq, docgen4 and aesop so that any project that uses versions with the same tags and has the same lean-toolchain as the tagged mathlib should have compatible dependencies.

My main concern is that students will run lake update and break their clones. I can point to specific commits in the lakefile but that is more fiddly.

[Sebastian Ullrich]

My main concern is that students will run lake update and break their clones

Is that a reasonable concern? You are effectively trying to reinvent the manifest file inside lakefile.lean.

[Sebastian Ullrich]

I support the general idea though, this would best be coordinated with sufficiently frequent Lean stable releases

[Sebastian Ullrich]

It would be great of course if lake update simply updated you to the next coordinated tag if you already use them

[Siddhartha Gadgil]

What I meant is that each time I update to a newer mathlib, I have to update all commits in the manifest file and check that the setup works. Also my course page will depend on other repositories of mine and I have to fix those as well.

Not that there is any fundamental problem with this, but if instead I could point to commits with the same name it will be easier and I am less likely to make an error. But besides this, if say 4 courses are being taught each of us teaching will have to do this every time we update.

[Kevin Buzzard]

Whenever I've taught, I've never updated mathlib at all during the course. It seemed to me that this was asking for trouble.

[Siddhartha Gadgil]

That's a lot easier to do with mathlib3. With mathlib4 we want to use things as they come online

[Sebastian Ullrich]

You can't ask for coordinated releases and "things as they come online" at the same time :) . I would expect coordinated releases to happen about very month or so. If you want to update mathlib4 more frequently, there's no way around coordinating stuff manually, but at least your students won't be exposed to that.

[Sebastian Ullrich]

An "update only these specific packages" Lake command would be helpful though

[Siddhartha Gadgil]

I agree. I meant with a modest delay as they come online, not a whole semester. And I meant some intermediate stability, like lean's nightly builds, not necessarily M-x` level.

[Siddhartha Gadgil]

Sebastian Ullrich said:

My main concern is that students will run lake update and break their clones

Is that a reasonable concern? You are effectively trying to reinvent the manifest file inside lakefile.lean.

Some empirical data (nothing serious but in case it is amusing) - two students did indeed run lake update and break their builds.

[Sebastian Ullrich]

Perhaps upgrade would be a more destructive-sounding name

[Siddhartha Gadgil]

Many of these are mathematics students so they may find upgrade more positive even. The group is small enough that I just fix for those who make mistakes instead of defending against their creativity. But here the issue is that a warning that it may be good to run lake update is given.

[Sebastian Ullrich]

Then you have some conflict between your lakefile and manifest

[Siddhartha Gadgil]

I believe it just has to do with docgen4 and the mode when it is on and off. Everything is running fine, just emitting this warning.

[Sebastian Ullrich]

I don't think mathlib4 currently has this warning, so it can definitely be avoided

[Siddhartha Gadgil]

Or maybe some inconsistency between direct and transitive dependencies, not causing an error but a warning.

[Siddhartha Gadgil]

Actually I think only I see this warning, and only when I run lake -Kdoc=on build PnP2023:docs.

[Siddhartha Gadgil]

So it may have been actual errors of students that gave them the warning. Or maybe they updated seeing some README.

[Heather Macbeth]

@Siddhartha Gadgil I am teaching in Lean 4 at the moment and have already needed to update my mathlib; I expect to do this regularly. My setup (which I copied from @Rob Lewis who is also doing this) doesn't seem difficult for the students. Here's how it works:

• when I want to bump mathlib I change the commit listed in the lakefile
• then I locally run lake update and it changes the commits of all dependencies in the lake-manifest to the versions of those dependencies used in that version of mathlib
• then the students just have to pull and run lake exe cache get; they never run lake update themselves. (Actually instead of pulling directly they run this script Rob wrote which tries to deal with local changes)

[Siddhartha Gadgil]

Thanks @Heather Macbeth
I have broadly a similar system, with students having private repositories for which they have instructions to set upstream to my repository. The intention is exactly that only I do updates and these propagate when they pull from upstream and merge.

What happened is a couple of students ran lake update anyway. In one case I have no idea what prompted this - I noticed the break in the students CI, told him and fixed it. The other case there was some other installation problem and the student thought lake update will help.

[Heather Macbeth]

Maybe at some point the students ran lake build? This emits a warning that you should lake update if you're not on the latest version of everything (that warning is super confusing and I think it should be changed).

[Siddhartha Gadgil]

That is quite likely.

[Heather Macbeth]

I have not had the students run lake build (partly for this reason). My file hierarchy is only a few files deep so I can get away without it, just doing lake exe cache get for the mathlib build.

[Siddhartha Gadgil]

They are indeed required to run lake build directly or indirectly.

[Heather Macbeth]

It might be too late now, but maybe you can write a script which does lake build but suppresses the output :-)

[Heather Macbeth]

Or maybe just PR a change to lake to rephrase that confusing message!

[Siddhartha Gadgil]

I got the students to run a command line program in the first lab (not write it, just edit the imports). I am mixing programming with proofs and matheematics, so I have taken the view that students should learn to deal with low-level issues at least a bit.

[Siddhartha Gadgil]

It is a small enough group and I help them when needed. And many are smart with such things already.

[Sebastian Ullrich]

@Heather Macbeth I don't get that warning when running lake build on your repo. It really should be shown only when you've changed the lakefile without running lake update afterwards

[Heather Macbeth]

I'm not sure exactly the circumstances when this happens, but I have seen it a few times. Here was one last month, if you remember:
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/aesop/near/317587174

[Heather Macbeth]

I believe I also saw it recently when temporarily working off a fork of Std (not sure I am exactly remembering the circumstances)

[Sebastian Ullrich]

Kevin, that sounds great for teaching, but should probably be discussed in another topic - if a warning make sense on the command line, it should make sense in VS Code as well

[Sebastian Ullrich]

Heather Macbeth said:

I'm not sure exactly the circumstances when this happens, but I have seen it a few times. Here was one last month, if you remember:
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/aesop/near/317587174

Yes, that was such an unsynchronized change where the warning should indeed be shown

[Kevin Buzzard]

(moved -- thanks)

[Yaël Dillies]

I get the lake update warning every single time because I'm on Windows.

[Sebastian Ullrich]

Ah, I think someone mentioned that before, but we don't have a Lake issue for it yet afaics

[Siddhartha Gadgil]

Siddhartha Gadgil said:

As courses using Lean 4 will start in a couple of weeks (including mine), I would like to suggest having periodic tagged commits. Just a lightweight tag is fine. This is so lakefile.lean in a course repository can point to tagged versions to ensure compatibility.

Specifically, what would be nice is for coordinated labels for mathlib, Std, Qq, docgen4 and aesop so that any project that uses versions with the same tags and has the same lean-toolchain as the tagged mathlib should have compatible dependencies.

My main concern is that students will run lake update and break their clones. I can point to specific commits in the lakefile but that is more fiddly.

Indeed the student whose clone broke yesterday (fixed easily) was no windows.
Just to revive my suggestion, perhaps it will be good to have "fortnightly" tags (just lightweight tags to point to) for the major repositories, say on the 10th and 25th of the month, so that they work. And a corresponding tag for the lean-toolchain - just an alias to the nightly actually used in the coordniated tagged versions.

The idea is to point our lakefiles to these tags only, and periodically shift to the next tag. This is not essential (my course is going fine for example) but may help all those teaching.

[Floris van Doorn]

On Windows I see the "manifest out of date" warning every single time I run lake build or lake exe cache get.