Bumps of PhysLean.

Stream: PhysLean

[Joseph Tooby-Smith]

I thought it was worth making a chat regarding bumping PhysLean.

For those new to Lean: Bumping PhysLean means updating either the Lean version or the Mathlib version that PhysLean depends on, or both.

Firstly I want to open the following discussion: Currently I only bump PhysLean for every stable release of Lean (about once a month). Kevin said that over on FLT they bump weekly. The advantage of bumping more often is that it is easier: less has changed in Mathlib, so there is less to change downstream - and it is easier to pinpoint what has changed. The disadvantage is that it requires a more sustained time commitment, which I personally can't commit to alone. I would also be happy if we can make things somewhat predictable. What are our options are here?

Secondly: I think using this thread to notify when a bump of PhysLean has taken place will be useful.

[Anne Baanen]

Hi! This post has some great timing actually, since one of my goals for the coming months is to improve the process of bumping Lean projects. I was calling @Pietro Monticone on the topic right at the moment you posted this :)

One option you might want to consider is to install the lean-update action, which runs the lake update command at a scheduled interval and will make a PR / issue / commit (configurable) whenever the build succeeds. So the easy updates become automatic and you get notified for the difficult ones.

I see that right now you're making good use of the versioning tag system, so e.g. the Lakefile for the PhysLean tag v4.18.0-rc1 requires Mathlib v4.18.0-rc1, which is great! If all Lean projects had version tags like this, there would be no issues with version mismatches between dependencies. So I would like to ask to keep making those tags too. (Another goal is to have lean-update or similar making this tag automatically for you. Perhaps that will need some lake improvements though, so that will have to wait a bit longer.)

[Joseph Tooby-Smith]

Hey @Anne Baanen ! Thanks for this.

lean-update looks great - I had heard about it before but forgot it was an option so thanks!

If I set the frequency to 1 week for updates, will I still need to do special manual bumps to make sure one is on the tagged version of Mathlib and Lean? I'm guessing the answer is yes, but this should be easy if weekly bumps are also done.

[Anne Baanen]

Yes, if you use lean-update right now you would still need to do the tagged bumps manually, unfortunately. That should become automated in some way in the next few months :)

[Anne Baanen]

And if you have any other ideas for how to make lean-update more useful, please let me know!

[Joseph Tooby-Smith]

Great thanks Anne! For reference, I made an GitHub issue c.f. adding lean-update to physlean here.

[Joseph Tooby-Smith]

@Anne Baanen I did have one thought of something which would be very nice: It would be nice if when a bump fails it tells you which specific commit(s) to Mathlib or Batteries etc caused it to fail.

I think this would be practically unfeasible to do though without a very large computation time.

[Tomas Skrivan]

@Anne Baanen What is the recommended setup if I have package A that depends on mathlib and package B that depends on A. Ideally, the automation tries to update A and if that succeeds it tries to update B.

Do I just set up automatic update for A on Monday and B on Tuesday?

[Anne Baanen]

Joseph Tooby-Smith said:

Anne Baanen I did have one thought of something which would be very nice: It would be nice if when a bump fails it tells you which specific commit(s) to Mathlib or Batteries etc caused it to fail.

Hmm, maybe to get more fine grained feedback, you could try running the automatic bumping in the background every day, but set up so it only reports an error on failure and doesn't do anything on success. This would then be in addition to the bumping script that actually commits/PRs the results every week, so you get an early warning if things start to go wrong, but you don't force users to update their dependencies every day.

[Anne Baanen]

Tomas Skrivan said:

Do I just set up automatic update for A on Monday and B on Tuesday?

Staggering the build times is exactly how lean/batteries/mathlib do it: Lean builds a nightly at 7AM UTC, Batteries at 9:45AM and Mathlib at 10AM.

[Kevin Buzzard]

Right, we have this auto-bumping on FLT I think (if I'm talking about the same thing as Anne). Indeed one hour ago a machine opened FLT#402 which is telling me amongst other things that FLT.GaloisRepresentation.Cyclotomic is not compiling any more, and I can guess exactly why: Andrew's PR to mathlib adding more stuff about the cyclotomic character just got merged, so now we have stuff in FLT which is also in mathlib which needs to be deleted. I will try to get to this bump today.

[Pietro Monticone]

Yes, we are using the lean-update action in FLT

[Pietro Monticone]

I’ve not thought about it deeply enough but here is rough idea.

Given two packages A and B such that:

• A depends on Mathlib
• B depends on Mathlib
• A depends on B

a potentially convenient update workflow (that would require a relatively small extension of lean-update) could be roughly the following:

On B (every 1-3 days):

1. If the Mathlib lean-toolchain version is higher than the B lean-toolchain version, then pin the new version in the B lakefile.toml andlake update. If it succeeds, open a PR and create release after merge; if it fails, open an issue with the relevant information in the description (i.e. changes in the lakefile.toml) which would be useful to the maintainer for the manual bump.
2. If the Mathlib lean-toolchain version is the same as the B lean-toolchain version, then pin the latest Mathlib commit in the B lakefile.toml and lake update. If it succeeds, open a PR; if it fails, open an issue with the relevant information in the description (i.e. changes in the lakefile.toml) which would be useful to the maintainer for the manual bump.

On A (every 1-3 days, shifted by an hour or so):

1. If the B lean-toolchain version is higher than the A lean-toolchain version, then pin the new version in the B lakefile.toml and lake update. If it succeeds, open a PR and create a release after merge; if it fails, open an issue with the relevant information in the description (i.e. changes in the lakefile.toml) which would be useful to the maintainer for the manual bump.
2. If the B lean-toolchain version is the same as the A lean-toolchain version, then pin in the A lakefile.toml the latest commit in the B lakefile.toml and the Mathlib commit pinned in B, then lake update. If it succeeds, open a PR; if it fails, open an issue with the relevant information in the description (i.e. changes in the lakefile.toml) which would be useful to the maintainer for the manual bump.

It might work decently and it seems generalizable enough…

[Pietro Monticone]

NB: The maintainer can always decide not to merge the PR immediately, but at least they would have full control.

[Anne Baanen]

I agree with your vision! A great bonus functionality would be to specifically pin B to the first Mathlib version with a newer lean-toolchain. That way we can be sure all the releases of various projects agree on their dependency versions. I think that would be possible to find out using git log, right?

[Tomas Skrivan]

Do I understand it correctly that in my lakefile.lean I should depend on mathlib's master branch? Otherwise lean-update action would not do anything useful.

[Kevin Buzzard]

That's what I do in FLT except when we do a bump to a tag.

[Joseph Tooby-Smith]

(I've just bumped PhysLean to v4.18.0 and set up lean-update.)

[Tomas Skrivan]

I wasn't as successful as you yesterday :( I tried bumping SciLean to v4.18.0 but the compiler seems broken. For some reason, you can't compile binary that imports Batteries.Tactic.Lint.Misc and most of Mathlib does. It seems to be fixed on v4.19.0-rc2 but ffi is getting an overhaul and I can't get ffi functions to evaluate in the editor.