bump/v4.4.0

Stream: std4

[Scott Morrison]

Our first Lean adaptation PR under the new combined CI regime is ready to go!

@Mario Carneiro and/or @Joe Hendrix, could you please look at std#383 and merge it (into its base bump/v4.4.0).

[Scott Morrison]

The plan is that the bump/v4.4.0 branch will accumulate already approved changes (unlike the no holds barred nightly-testing), and if all goes well when v4.4.0-rc1 comes out we'll just have a straightforward merge of bump/v4.4.0 into main.

[Eric Wieser]

Something I don't see in the regime document is a mechanism to merge the latest master back into bump/v4.X.0 when they diverge; my suggestion would be that this is handled by making a PR against bump/v4.X.0 from master (i.e. the reverse direction to the final merge) as necessary (i.e., just before opening a "real" PR against bump/v4.X.0). In an ideal world this is a no-op, but the reality is that it will have some downstream fallout that spilled over from the previous merges into the bump branch, and this ensure those are reviewed too.

[Mauricio Collares]

Last time someone opened a PR merging master into another branch, bors got very confused. Is this fixed?

[Eric Wieser]

Ah you're right, that did cause issues. I think it would be easy to hack bors not to do that, but you're right that if we do nothing (and leave the "retarget branches" setting on) then it makes a mess

[Eric Wieser]

I think ease of integration with Lean changes is probably more important than retargetting branches automatically, so would be happy to switch that bors setting back off iff we adopt the workflow above.

[Mario Carneiro]

Scott Morrison said:

The plan is that the bump/v4.4.0 branch will accumulate already approved changes (unlike the no holds barred nightly-testing), and if all goes well when v4.4.0-rc1 comes out we'll just have a straightforward merge of bump/v4.4.0 into main.

Should this be a merge or a squash merge?

[Eric Wieser]

I think a regular merge (done without bors) is best in terms of seeing why things were changed

[Scott Morrison]

@Eric Wieser, if bump/v4.4.0 is regular-merged into master (when its time to update the toolchain), I presume it is still okay to do regular merges of master into bump/v4.4.0 to keep them in sync?

[Mario Carneiro]

I think I would prefer a squash merge, my guess is that the history of bump/v4.4.0 will be somewhat messy

[Scott Morrison]

I'm worried that these will introduce extra commits that will later end up on master, too.

[Scott Morrison]

bump/v4.4.0 will be merged into master via a PR, so the history is all still available at the PR.

[Eric Wieser]

Mauricio Collares said:

Last time someone opened a PR merging master into another branch, bors got very confused. Is this fixed?

Actually, this should be fixed: https://github.com/bors-ng/bors-ng/pull/1715

[Eric Wieser]

Mario Carneiro said:

I think I would prefer a squash merge, my guess is that the history of bump/v4.4.0 will be somewhat messy

Ideally it would consist only of "update bump/v4.4.0 for changes from lean4#XYZ" and "merge latest master into bump/v4.4.0". Being worried about the mess sounds odd to me; the mess is precisely the thing that will have been reviewed.

[Eric Wieser]

Scott Morrison said:

bump/v4.4.0 will be merged into master via a PR, so the history is all still available at the PR.

Maybe GitHub will outlive us all, but my experience with numpy was that anything not recorded in the git history is at risk of becoming inaccessible; references to an old bug/PR tracking system that is offline and not archived anywhere are useless.

[Mario Carneiro]

Eric Wieser said:

Mario Carneiro said:

I think I would prefer a squash merge, my guess is that the history of bump/v4.4.0 will be somewhat messy

Ideally it would consist only of "update bump/v4.4.0 for changes from lean4#XYZ" and "merge latest master into bump/v4.4.0". Being worried about the mess sounds odd to me; the mess is precisely the thing that will have been reviewed.

Note that the mess being difficult to review has been a problem with the last few iterations on this bump process.

[Mario Carneiro]

Eric Wieser said:

Scott Morrison said:

bump/v4.4.0 will be merged into master via a PR, so the history is all still available at the PR.

Maybe GitHub will outlive us all, but my experience with numpy was that anything not recorded in the git history is at risk of becoming inaccessible; references to an old bug/PR tracking system that is offline and not archived anywhere are useless.

We very much rely on PR history as part of the archive, and we would need to take it with us if Github faces some future calamity. We should never have used squash merge if this was a concern.

[Eric Wieser]

Note that the mess being difficult to review has been a problem with the last few iterations on this bump process.

Arguably this is because we weren't able to manage bump/v4.4.0 cleanly last time (I believe Scott said this was because we decided the strategy mid-cycle and it was too late?)

[Scott Morrison]

So far this bump/v4.4.0 is super simple. One PR each on Std and Mathlib, and we're only three days from the next version.

[Scott Morrison]

I think std4#406 (moving bump/v4.4.0 up to nightly-2023-11-29, and adjusting the lakefile for the new syntax for specifying options) is ready to go.

@Joe Hendrix and/or @Mario Carneiro, could one of you please prioritize merging this? It will be necessary for the version bumps, which I'll hopefully be able to start in about +2 hours.

[Scott Morrison]

Okay, std4#409 is now the PR moving Std to v4.3.0 (this is essentially no-op, because v4.3.0 is identical to v4.3.0-rc2, but I want to make sure there is a commit on the master branch on each stable version!

[Scott Morrison]

Again, @Joe Hendrix /@Mario Carneiro, it's helpful if this can be merged soon so downstream repos moving to v4.3.0 can point at the right commit.

[Scott Morrison]

I just did it myself, I think that's okay per previous discussion.

[Scott Morrison]

@Mario Carneiro, could you take another look at fix: DiscrTreeCache.mk init argument should be lazy std4#408?

Without this fix, if the exact? or rw? cache were built on a previous toolchain you get a crash on every file that imports them (as the .olean is eagerly loaded, and rejected because it has the wrong embedded hash).

[Scott Morrison]

Hence I need this in Std before I can move Mathlib's bump/v4.4.0 up to nightly-2023-11-29 (and hence before I can move Mathlib to v4.4.0-rc1).