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.

[Joseph Tooby-Smith]

I just bumped PhysLean to v4.19.0 with the PR #539, will also create a tag.

This means that if you merge with master or create a new branch from master you will have to update your local version of Mathlib.

[ZhiKai Pong]

May I ask when will the next bump be? I'm working with lots of inner which will be impacted by #24499, and Tomas's #24056 will probably reduce a lot of differentiability assumptions as well, so I'm wondering whether I should work on my current code first then refactor later or wait for the update

[Joseph Tooby-Smith]

I don't think there is much harm to bumping now. I made a bump-issue for v4.20.0-rc5 here: https://github.com/HEPLean/PhysLean/issues/565.

I think this will cover #24499, but may not cover #24056. But after bumping to v4.20.0-rc5, and tagging the release we can bump to a nightly version of mathlib for the time being, so that #24056 is covered.

If you or anyone else wants to have a go at this - please be my guest :). The hardest part of bumping is fixing all the things that may have changed in mathlib - usually not so difficult but a bit annoying.
If not, I can have a go at it tomorrow morning.

[Joseph Tooby-Smith]

More generally I'm currently only really bumping for stable lean releases.

There is this lean-update thing discussed above, but I haven't got this fully up and running yet - basically because I'm worried people having to rebuild the whole of physlean everytime it updates which is not ideal.

[ZhiKai Pong]

I'll try to follow the list and hopefully I don't break anything :)

[ZhiKai Pong]

Joseph Tooby-Smith said:

I think this will cover #24499, but may not cover #24056.

Is there a simple way to check which ones are in the stable release?

[Joseph Tooby-Smith]

I'm not aware of any :(. I just looked at the dates when they were merged and the date of the tagged releases.

[Kevin Buzzard]

FWIW we tend to bump FLT to mathlib master about once a week

[Joseph Tooby-Smith]

PhysLean has now had the following two bumps committed:

• #566 to the version of mathlib and lean tagged as v4.15.0-rc5. (Thanks @ZhiKai Pong !). There is now a corresponding PhysLean tag for this.
• #568 to a rev of mathlib from today.

Thus, if you merge with master or create a new branch you will have to update your local versions of mathlib and lean. I do this by running: rm -rf .lake; lake update; lake build, which is pretty fail-safe I think.

[Joseph Tooby-Smith]

I created a bump tracker issue for v4.20.0 here.

If anyone wants to have a go at this, let me know - otherwise I should be able to find time later this week.

[Joseph Tooby-Smith]

I have bumped physlean in

• #591 to v4.20.0
• #593 to v4.20.1

Tags have been created for each of these.

Thus, as usual, if you merge with master or create a new branch you will have to update your local versions of mathlib and lean (rm -rf .lake; lake update; lake build).

[Joseph Tooby-Smith]

I have bumped PhysLean in

• #629 to v4.21.0

A tag has been created for this.

My standard message here applies:

If you merge with master or create a new branch you will have to update your local versions of Mathlib and Lean. Use:

rm -rf .lake; lake update; lake build

This may take up to 30 minutes to run.

I had to update my elan also with elan self update.

[Kevin Buzzard]

Why is your message not "if you merge your branch with master or create a new branch off master then you will have to update your local versions of mathlib and Lean. Use lake exe cache get; lake build. This may take a few minutes to run"?

[Kevin Buzzard]

Oh I see -- you are pinning versions of everything? I would not encourage my users to run lake update in FLT because it might randomly bump mathlib and break their build (we're typically on bleeding-edge mathlib, I don't want the hassle of just bumping once a month). But you're using lake update as a proxy for lake exe cache get it seems. And the 30 minutes is how long it's just taking PhysLean to build with an up-to-date mathlib on a computer which is much slower than the one I just built it on in 5 minutes?

[Kevin Buzzard]

I usually only recommend rm -rf .lake when things are broken. This is putting up your compilation time because everything (incl mathlib) has to be recloned from github, rather than just bumped.

[Eric Wieser]

Oh I see -- you are pinning versions of everything?

This is a good idea (at least, in the way Joseph has done it), but indeed there is no need to make anyone else suffer through a fresh build

[Eric Wieser]

Kevin Buzzard said:

I usually only recommend rm -rf .lake when things are broken.

Strictly speaking you should only rm -rf .lake/build, it's possible to commit configuration inside .lake

[Eric Wieser]

Of course really lake clean should do, but I guess we all have trust issues

[Joseph Tooby-Smith]

Yeah, I've pinned versions.

But I think I just understood something I never understood before :), which is the following: as long as the lake-manifest.json file is updated (e.g. from merging with master) then lake exe cache get does all of the work. Is this correct?

Thus on FLT do people then have to run lake exe cache get everytime they merge with master? (But if I now understand correctly this should be fast).

The 30 min does come from the time to build PhysLean - which is a bit of an overestimate, the github workflows build it in about 20-25min. I just didn't want people to worry if it takes a long time. So really my message should be:

If you merge with master or create a new branch off master you will have to update your local versions of Mathlib and Lean. Use: 

lake exe cache get; lake build

Depending on your computer this can take anywhere between 5 to 30 minutes to run.

[Eric Wieser]

Perhaps the surprise here is that lake update is calling lake exe cache get behind the scenes

[Eric Wieser]

(because mathlib tells it to do that)

[Joseph Tooby-Smith]

Am I correct that lake update does little else? I.e. it just updates the lake-manifest.json and the lean-toolchain, and then lake exe cache get does the rest?

[Pietro Monticone]

Eric Wieser said:

Perhaps the surprise here is that lake update is calling lake exe cache get behind the scenes

Yes https://github.com/leanprover-community/mathlib4/blob/ede775853cc9f271a9fcf1475dec887f82544e30/lakefile.lean#L166-L176

[Joseph Tooby-Smith]

Thanks for the link Pietro, I think I understand things now. Many thanks for explaining everyone :slight_smile:.

[Kevin Buzzard]

Joseph Tooby-Smith said:

Thus on FLT do people then have to run lake exe cache get everytime they merge with master? (But if I now understand correctly this should be fast).

No. They only need to do this every time they merge master into their work, and master has bumped mathlib since they last merged. But I think in general people don't merge master into their branches? Apart from the last couple of weeks when I've been busy, I am usually merging stuff pretty quickly (and I am back on top of things now, I think essentially all PRs are waiting for people other than me right now)

[Joseph Tooby-Smith]

As per the announce channel:

• #announce > v4.22.0

v4.22.0 of Lean has being released, which means we should update PhysLean to this version and the corresponding tagged version of Mathlib and doc-gen. I have made a tracking issue for this bump :

• Bump: tracking issue

If someone would want to volunteer to do this, it would be great! If not I will likely be able to do it at some point, but there will likely be a delay.

[Joseph Tooby-Smith]

PhysLean has now been bumped (here) to v4.22.0 of Lean and the corresponding tagged version of Mathlib. The upside we get a bunch of new features from Lean and new theorems and definitions from Mathlib, the downside is:

If you merge with master or create a new branch off master you will have to update your local versions of Mathlib and Lean. You can use: 

lake exe cache get; lake build

Depending on your computer this can take anywhere between 5 to 30 minutes to run.

If you have any issues feel free to comment here and we can help.

[Joseph Tooby-Smith]

PhysLean has now been bumped, at PhysLean#741, to v4.23.0 of Lean and the corresponding tagged version of Mathlib.

If you merge with master or create a new branch off master you will have to update your local versions of Mathlib and Lean. You can use: 

lake exe cache get; lake build

Depending on your computer this can take anywhere between 5 to 30 minutes to run.

If you have any issues feel free to comment here and we can help.

[Joseph Tooby-Smith]

I have made a tracking issue for bumping PhysLean to v4.24.0 PhysLean#773. I will not get chance to do this until early next week, so if anyone wants to have a go at this please do.

[Alfredo Moreira-Rosa]

On my side i already made a bump in lean-units. The main impact i got is that induction' disappeared, and other minor changes. Was a 30 mn work.

[Joseph Tooby-Smith]

PhysLean is now bumped to v4.24.0 (in PhysLean#776), and the corresponding tagged version of Mathlib. This means

If you merge with master or create a new branch off master you will have to update your local versions of Mathlib and Lean. You can use: 

lake exe cache get; lake build

Depending on your computer this can take anywhere between 5 to 30 minutes to run.

[Joseph Tooby-Smith]

Alfredo Moreira-Rosa said:

On my side i already made a bump in lean-units. The main impact i got is that induction' disappeared, and other minor changes. Was a 30 mn work.

induction' never actually appeared in PhysLean :), the main thing I had to modify was add open Matrix or open MatrixOrder in places, otherwise this time it was very simple.

[Joseph Tooby-Smith]

Of a similar variety to a bump so posting this here: In PhysLean#778 I have improved the linters so lake exe lint_all should run a lot quicker locally. (I basically changed how the sorry axiom is being looked for)

[Joseph Tooby-Smith]

PhysLean has been bumped to v4.25.0 (in PhysLean#814), and the corresponding version of Mathlib.

If you merge with master or create a new branch off master you will have to update your local versions of Mathlib and Lean. You can use: 

lake exe cache get; lake build

Depending on your computer this can take anywhere between 5 to 30 minutes to run.

The biggest change in this Bump is that: The definition of EuclideanSpace has changed and consequently the definition of Space d, which is currently just an abbreviation of EuclideanSpace. It is a TODO to move Space d from been an abbreviation of EuclideanSpace to its own structure.

[Joseph Tooby-Smith]

I've restructured Space d to its own structure at: PhysLean#819

[Joseph Tooby-Smith]

PhysLean has been bumped to v4.26.0 (in PhysLean#836), and the corresponding version of Mathlib.

If you merge with master or create a new branch off master you will have to update your local versions of Mathlib and Lean. You can use: 

lake exe cache get; lake build

Depending on your computer this can take anywhere between 5 to 30 minutes to run.

There was one tricky aspect of this Bump which remains unresolved, and was circumvented by making two results @[sorryful].

This is discussed here

#lean4 > Fin.find? and decide in v4.26.0