v4.3.0-rc2

Stream: mathlib4

[Scott Morrison]

The next Lean version bump for Mathlib is going to be a bit spicy: master and nightly-testing have already diverged a fair bit. Next time, I think we'll be able to progressively merge adaptation PRs into a bump/v4.X.0 branch. But because ... complicated CI related things I can explain elsewhere ... that wasn't possible this time.

So: #8366 will move Mathlib to v4.3.0-rc2 (it doesn't actually exist yet, but probably will tomorrow). It is the supremum of

• #8284
• #8056 (this is the one that can no longer be built separately)
• #8023
• #8332
• #8226 (already approved)
  along with some manual changes to nightly-testing as Mathlib master changes have been merged in.

If anyone if available to look at this one, this would be extremely helpful! Once this is in, master and nightly-testing will resynchronize, and hopefully the new CI scheme will make everything easier next time.

[Mauricio Collares]

#8056 probably built before because of the simp decide changes. You can try adding decide := false to the offending simps in the meantime (norm_num doesn't have such a knob but I think you can replace it with simp in the few cases where it fails now)

[Scott Morrison]

I'm not sure that getting #8056 to build serves any purpose. It can't be merged into anything, because it is using a Lean version that is not comparable to any nightly release.

[Mauricio Collares]

Was just about to write that :)

[Scott Morrison]

(The point of the new scheme is that all adaptation PRs will be mergable into a branch that always stays on a nightly release, and only contains approved changes.)

[Mario Carneiro]

BTW, can we not be doing bumps on a Scott-monday? This always seems to happen when I'm out of town on a weekend :)

[Scott Morrison]

Haha, still Scott-sunday here.

[Scott Morrison]

But sure, I can go for Australia-tuesday in future.

[Mauricio Collares]

Judging from the diff I think the supremum includes #7834 (which Scott already approved) too :partying_face:

[Eric Wieser]

Some of these PRs are awfully large, especially #8023 which touches over 200 files! Maybe it's too late on this round, but can we try harder in future to split them into "cleanup of master" (in this case using comp_def) and "fixes for the nightly branch" (everything else)?

[Scott Morrison]

Yes. The PRs made based on the pre-release toolchain will be merged into a bump branch. Only fixes made on nightly-testing because of subsequent breakages introduced by changes in master will need to be reviewed serparately.

[Scott Morrison]

Oh, sorry, I missed the point.

[Eric Wieser]

I'm requesting something stronger where the bits of the patch that work on master are PR'd directly to master

[Scott Morrison]

You're asking that all the comp_def changes be done separately, because they can be merged into master first.

[Eric Wieser]

Not necessarily that we actually do that now, but that we try to do things in that way in future

[Scott Morrison]

Hmm... not making any promises I can do that. Perhaps when I notice the possibility to do that I can ask for someone to do it.

[Eric Wieser]

The smaller the bump PRs are the fewer conflicts they have to manage

[Scott Morrison]

We'll see.

[Eric Wieser]

I tried to do something similar with Kyle's PR, but the response was "we don't have a process for merging master back into the bump branches, so this makes things worse". Maybe that's a discussion for another thread

[Scott Morrison]

Oh, yeah.

[Scott Morrison]

The lean-pr-testing-NNNN branches cannot necessarily receive further changes from master.

[Scott Morrison]

They (as of about a week ago) are always based of a nightly-testing-YYYY-MM-DD branch, and they don't keep up with master once nightly-testing itself has advanced to a more recent nightly releasse.

[Eric Wieser]

Can their base nightly-YYYY-MM-DD branch receive (manual) merges from master directly?

[Scott Morrison]

They can, but there is no automation that attempts to do this.

[Eric Wieser]

Edited, I meant manual merges

[Eric Wieser]

Or a manual PR that requests a merge

[Scott Morrison]

So if you want to do it by hand for a particular one, that is fine. (As long as you maintain the invariant that nightly-testing-YYYY-MM-DD stays on the nightly-YYYY-MM-DD toolchain and passes CI.)

[Notification Bot]

32 messages were moved from this topic to #mathlib4 > v4.3.0-rc2 - comp_def and #8023 by Eric Wieser.

[Eric Wieser]

To summarize the thread above; I pushed to #8023 (and the bump PR) some commits that use @[eqns] instead of comp_def. The fallout on master can be seen in #8371 (which we can safely merge before the bump, if we want this change). If we think the fallout is worse than writing comp_def everywhere, we should revert my pushes to #8023

[Kyle Miller]

For anyone who wants a up-to-date summary, it looks like the current status is

• #8366 (the bump PR) passes CI
• #8371 can be merged to master right now (I don't see why not, so I just merged it )
• #8023 can be ignored since it's already been incorporated into the bump PR

[Kyle Miller]

For #8366, we've only got ~450 changed files to review :smile:

I've scrolled through the changes and did the "spin the globe and stop it with your finger" game a number of times. If we each do enough rounds of that, we'll almost certainly have reviewed the whole thing. :upside_down:

[Eric Wieser]

#8373 knocks 3 files off that list, which is hardly significant, but it's green already so :shrug:

[Eric Wieser]

#8332 is an easy review for anyone who remembers what destruct means for aesop

[Eric Wieser]

We're now down from ~450 files to =450 files!

[Johan Commelin]

@Scott Morrison Should I be reviewing the PRs that #8366 depends on?

[Johan Commelin]

What exactly is that status?

[Scott Morrison]

#8366 is the main PR, that we want to get approval form. It depends on:

#8284
#8056 (this is the one that can no longer be built separately)
#8023
#8226 (already approved)

Because of the problem with #8056, unfortunately #8366 is an all-or-nothing affair.

[Scott Morrison]

Ideally in future I will be able to present a list of PRs which can be reviewed separately, along with a pinky promise that the main PR is just their supremum.

[Scott Morrison]

But I think at this point the right thing to do is just look at #8366.

[Eric Wieser]

I pulled off some instances change to #8380, just since I think it's useful to be able to see the statement changes in a blame in future without going through a four-hundred-file diff