lean4#3159

Stream: lean4

[Kim Morrison]

@Marc Huisinga's lean4#3159 has just hit the latest nightly. This will break a lot of downstream repository that interact with InfoTree. The patches are mostly all ready to go, but there's going to be some coordination required to get them all in place.

[Kim Morrison]

I've just merged Std's lean-pr-testing-3159 branch into its nightly-testing branch; compiles and tests locally, so I'll send it off.

[Kim Morrison]

Next up, I'll turn Std's lean-pr-testing-3159 into a PR to bump/v4.6.0.

[Kim Morrison]

Okay, that is up at std4#557. @Marc Huisinga, if you could give a thumbs up that I got that right, I'm happy to go ahead and merge it, too.

[Marc Huisinga]

Looks good. The original PR where the branch was accidentally deleted was identical.

[Kim Morrison]

Next, over at Aesop, no changes are required, but nevertheless I've bump nightly-testing, and aesop#97 (the latest adapation PR) up to nightly-2024-01-23 to verify that no changes are required.

Looks good!

[Kim Morrison]

Next up is ProofWidgets. There, we have lean-pr-testing-3159 ready to go, and I just opened a PR from that: ProofWidgets4#39. However ProofWidgets runs a bit differently from everything else, and we won't actually merge that to anything until v4.6.0-rc1 is out and we're ready to include this in master.

In the meantime, however, we've already made a release v0.0.26-pre. (If multiple breaking changes affect ProofWidgets within a month, I guess we're going to have pre2 and so on...)

The Mathlib lean-pr-testing-3159 branch is already using that release, so I think we can move on to Mathlib now.

[Kim Morrison]

So I've merged Mathlib's lean-pr-testing-3159 branch into nightly-testing, and set the std and aesop branches to nigthly-testing, and verified ProofWidgets is on v0.0.26-pre.

I've pushed that, and am compiling locally to see if I can keep ahead of CI. :-)

[Kim Morrison]

It's looking good though, we're already past everything that might be affected by lean4#3159.

[Kim Morrison]

I won't actually make a PR for all these changes to Mathlib's bump/v4.6.0 branch tonight, as I'm waiting for a maintainer to approve #9930 (the last batch of changes) first.

[Kim Morrison]

Still coming up: there are outstanding patches @Marc Huisinga prepared for @Mac Malone's alloy, and for LeanInk and the REPL. As these are slower moving projects I think it will be fine to just wait until the end of the month when v4.6.0-rc1 comes out before merging any of these. These patches are all linked from lean4#3159.

[Marc Huisinga]

It's also worth remembering that we had to adjust the CI with a reference to the LeanInk PR to make it pass. When the release candidate is released, we need to re-adjust this to reference main again.

[Kim Morrison]

Oof, thanks for the reminder, I had missed that. So many moving pieces. :-)