std4#470

Stream: std4

[Scott Morrison]

std4#470 is the PR containing @Kyle Miller's fix to Std for the nightly-2023-12-19 toolchain (changes from lean4#2973). This is a PR to the bump/v4.5.0 branch.

If @Joe Hendrix or @Mario Carneiro could review and merge this soon that would be great, so we can make the corresponding update on Mathlib's bump/v4.5.0 branch, and then be all ready for v4.5.0 in two days time! :-)

[Patrick Massot]

Scott, could you remind us where we can find the explanations about the release process?

[Scott Morrison]

@Patrick Massot, https://leanprover-community.github.io/contribute/tags_and_branches.html

[Scott Morrison]

Criticisms / suggestions / rewriting of that document very welcome!

[Scott Morrison]

There's a diagram at the bottom.

[Patrick Massot]

Thanks. The motivation here was to check that now is the right time to beg for a PR merge in the Lean 4 repo so that Mathlib gets good stuff in a couple of days instead of one month later (assuming there is only one release candidate). This is correct right?

[Patrick Massot]

The PRs I have in mind are the widget ones.

[Scott Morrison]

Yes, today is definitely the day. :-)

[Patrick Massot]

@Wojciech Nawrocki :pleading_face:

[Patrick Massot]

By the way, is there an official explanation of the will-merge-soon label?

[Scott Morrison]

I don't think so.

[Patrick Massot]

It appears for instance on lean4#3054

[Scott Morrison]

I think it shouldn't be there: my understanding of the intent is that only people with permission to merge should be putting it on PRs.

[Scott Morrison]

It should indicate that they intend to come back soon and merge it themselves if there are no objections.

[Scott Morrison]

And thus implicitly that it's okay to ping them if it hasn't been merged after a few days.

[Patrick Massot]

But Wojciech has permission to merge that, right?

[Scott Morrison]

And probably that others with permission to merge should free invited to merge if there is reason to do so.

[Patrick Massot]

https://github.com/leanprover/lean4/blob/master/CODEOWNERS#L21

[Scott Morrison]

Indeed! I had missed that, and wasn't sure.

[Scott Morrison]

lean4#3054 looks fine to me, so it would be great if it can go in soon. The cutoff is essentially 2023-12-21T18:00:00+11:00 for v4.5.0-rc1. But obviously the sooner the better so things can be tested against Mathlib and still have time to put out fires.

[Scott Morrison]

The other PR that you are after, @Patrick Massot, is presumably lean4#2964. This looks like it is still breaking Mathlib, so there is work to do if we want this in v4.5.0-rc1.

[Scott Morrison]

The Mathilb failures look to be not the fault of that PR, however, which is bad news (for me, as this isn't meant to happen anymore). I'll investigate.

[Patrick Massot]

Yes, that one is probably too late :sad:

[Patrick Massot]

The PR description mentions a missing Mathlib PR.

[Scott Morrison]

I'm still fixing the latest Std bump (which is needed to get nightly-testing working again): #9155

[Scott Morrison]

Once that is done I can investigate whether we can get lean4#2964 over the line.

[Scott Morrison]

I'm afraid I can't really do anything. @Wojciech Nawrocki will need to rebase lean4#2964 onto Lean's nightly-with-mathlib before I can do much to get Mathlib CI working. Unfortunately this PR is based off a quite old version of Lean, even the lakefile.lean in Mathlib won't parse with lean4#2964.

[Scott Morrison]

Ah scratch that, I was mislead by the fact that our CI setup no longer builds toolchains for all platforms unless you add the full-ci label, and so I was running on an ancient toolchain generated for lean4#2964.

[Scott Morrison]

Unfortunately Github won't build while there is a merge conflict with master, so this will have to wait for @Wojciech Nawrocki.

[Wojciech Nawrocki]

I put lean4#3054 on the merge queue.

[Wojciech Nawrocki]

As for lean4#2964, for the mathlib4 fix I was pushing commits to lean-pr-testing-2964 as per an earlier recommendation. However, that build eventually started to fail with some errors that seemed completely unrelated. 2964 does break mathlib, and the commits are meant to fix that, but it seemed difficult to test them in isolation so I gave up temporarily. I can try rebasing the lean4 PR branch to see if it helps with those unrelated failures.

[Scott Morrison]

Yes, rebasing is going to be essential at this point.

[Scott Morrison]

Make sure you rebase onto a commit corresponding to a nightly release, ideally rebase onto nightly-with-mathlib, which is the most recent nightly for which Mathlib CI completed successfully (usually, but not always, the most recent nightly!)

[Wojciech Nawrocki]

That's what I was doing! I did get caught by the lack of CI, e.g. the Windows PW4 build failed. Is adding the full-ci label sufficient to get all platforms?

[Wojciech Nawrocki]

Uh, the diff between master and nightly-with-mathlib includes stage0 updates, and I also have one in this PR. I don't think you can just merge them, you have to run the whole pipeline (build Lean, rewrite the stage0/ folder). But then a merge conflict with master seems unavoidable so long as I rebase on nightly-with-mathlib.

[Scott Morrison]

Oh, that is unfortunate.

[Scott Morrison]

We have just had a longer than usual delay getting an update for nightly-with-mathlib.

[Wojciech Nawrocki]

I can skip the stage0 changes in this PR and make them on the master branch later: they are not essential.

[Scott Morrison]

I'm hoping that in about an hours time nightly-with-mathlib will advance successfully.

[Scott Morrison]

Oh! Definitely do that then.

[Scott Morrison]

There is actually a bot that will do it for you now.

[Scott Morrison]

(The bot will do the stage0 update, that is.)

[Eric Wieser]

Scott Morrison said:

The motivation here was to check that now is the right time to beg for a PR merge in the Lean 4 repo

Yes, today is definitely the day. :-)

lean4#3060 would be particularly nice to get in from my perspective :)

[Scott Morrison]

What is this one affecting?

[Eric Wieser]

This indirectly makes ~q matching more effective

[Eric Wieser]

As you can now write match u, t, e with | 0, ~q(Nat), ~q($x + $y) in norm_num and positivity extensions, which would previously give an unhelpful error

[Wojciech Nawrocki]

How can I merge newer mathlib into lean-pr-testing-2964? Essentially I would like to add another "Trigger CI" commit.

[Scott Morrison]

I recommend either:

• merge nightly-testing-YYYY-MM-DD for whichever is the latest Lean nightly in your PRs history
• or push an actual empty commit

[Scott Morrison]

(Merging nightly-testing-YYYY-MM-DD is meant to happen automatically, but we broke it a few days ago. The fix in the Lean merge queue now!)

[Wojciech Nawrocki]

How can I determine which is the latest nightly in my PRs history? I rebased it on nightly-with-mathlib, but the commits there don't seem to be tagged with versions.

[Scott Morrison]

There used to be a script for precisely this, but @Joachim Breitner recently inlined it into the github workflow. :-)

[Wojciech Nawrocki]

Well, I found it by looking at nightly releases :)

[Scott Morrison]

git remote add nightly https://github.com/leanprover/lean4-nightly.git
git fetch nightly '+refs/tags/nightly-*:refs/tags/nightly-*'
git tag --merged HEAD --list "nightly-*" | sort -rV | head -n 1

does the job, but it pollutes your local checkout with all the tags from lean4-nightly.

[Scott Morrison]

If someone know how to run that step without fetching the tags, please let me know!

[Joachim Breitner]

You can fetch the tags without adding nightly as a remote, then the next normal fetch will remove them again, I think. Not pretty.