instructions?

Stream: nightly-testing

[Kevin Buzzard]

My understanding of what's going on here is that the FRO has decided that they need to move fast and break things when developing lean, and one of the things which they will break is mathlib. This means that occasionally there needs to be some work done to bump mathlib to lean master, and that the previous set-up (one thread in #general plus the interminable warning thread in one of the private streams) was too inconvenient to manage all this well, now we've understood the size of the problem.

Keeping mathlib up to date with core lean is a really important job and it seems to me that it's turning out to be a big job (perhaps unsurprisingly) which needs frequent attention. I thank Scott heartily for what he's done so far keeping the show on the road but he can't do this forever, we need him writing more game-changing stuff like omega, not fixing lemmas in random parts of the library he never normally goes in.

I'm still stuck in teaching hell until the beginning of April but one thing which has really struck me with reading the old thread is that I'm just confused about the actual details of what's happening. When I have teaching off my back and when I'm maintaining my own repo which will need to keep up with mathlib, I will need to be much more engaged with this process. So I'm hoping that someone will somewhere write some kind of explanation of the typical scenario (mathlib doesn't compile with some nightly) and then exactly which branches users like me are supposed to be pushing or not pushing to, and how we can help rather than (a) hinder or (b) redo work which has already been done.

I definitely think a stream for this is a step in the right direction.

[Ruben Van de Velde]

There's two or three relevant branches at any point:

• There's a bump/v4.x.x branch which is supposed to work at all times, and which will become a PR into master when v4.x.x is released
• There's a nightly-testing branch which is automatically updated every day to run against the latest nightly, and will therefore often break. We try to fix errors here as they come in, but we don't always finish before new breakage comes in from the automated bump
• There is sometimes a bump/nightly-YYYY-MM-DD branch with a PR into bump/v4.x.x; this is how bump/v4.x.x is kept up to date. Unlike nightly-testing, this is locked to a specific nightly, so we have some hope to get it passing CI even if there's new nightlies that break mathlib some more.

We should focus either on the bump/nightly-YYYY-MM-DD branch, if there is an active one, and on nightly-testing if there isn't one

[Kim Morrison]

Further, I'm hoping that 90% of the time the bump/nightly-YYYY-MM-DD branch will not actually need much work after the branch has been created. It will be created once nightly-testing is already working, and all that needs to be done is a little review and merging.

[Kim Morrison]

However, in the 10% of the time when Lean is moving too fast for us, the problem is going to be that nightly-testing will move on to a new nightly before we've finished catching up with the previous one. We can either do the Red Queen's race: "Now, here, you see, it takes all the running you can do, to keep in the same place.", and continue working on nightly-testing, or we can create a bump/nightly-YYYY-MM-DD branch that still needs work, and that branch will not be bumped to further nightlies.

[Kevin Buzzard]

So what is the workflow for "I've had a hard day at work, I fancy doing some lean this evening, I have an hour, how can I help"? That's the situation I'll find myself in. Or "I'm at work, I can't face reading emails, I'm eating lunch at my desk and I have ten minutes to try and be helpful"?

[Kim Morrison]

Getting there. :-)

[Kim Morrison]

The two main pieces of written instruction available at present are:

• https://leanprover.zulipchat.com/#narrow/stream/345428-mathlib-reviewers/topic/bump.20PRs/near/422136792 (Caveat: it doesn't explain that sometimes a bump/nightly-YYYY-MM-DD will exist that still needs work, and if that is the case we should prioritize fixing that ahead of working on nightly-testing)
• https://leanprover-community.github.io/contribute/tags_and_branches.html, a more detailed background on how the version tags and branches currently operate.

Neither of these sources is final! If you think we can be doing things differently and better, please make it happen. :-)

[Kim Morrison]

So, additional to what's explained in those sources, I would say the main task list is:

• If there is a bump/nightly-YYYY-MM-DD PR branch pointing at a bump/v4.X.0 branch, getting that ready for review / reviewed is the highest priority. (It's clear we need a better automatic indicator of whether such a PR exists right now!)
• Such PR branches are aiming at "master quality". Any FIXMEs need to be resolved. It's fine to write an Adaptation note: nightly-YYYY-MM-DD. <Explanation goes here>, but this should be detailed enough that someone can pick it up later without much context.
• When there is such a branch, it's always okay to merge it into nightly-testing.
• When there isn't such a branch, or you know there are problems in nightly-testing from even more recent nightlies than such a branch is on, you can work on nightly-testing!
• This is a lower quality branch. It's nice to get this running asap, even if this means putting sorries. But please make sure they are annotated clearly so we can find them. I have been writing FIXME nightly-testing.
• Usually I do a first pass, fixing the easy stuff, and sorrying the hard stuff. Then I start writing in this thread asking for help on the harder stuff. (Big stuff can have a new thread. If there's a bunch of smaller stuff, just individual posts in the main thread for that nightly are fine. One post per problem, please, so people can use emojis to claim and release work.)
• Anytime nightly-testing is working or near to working, we need to create a new bump/nightly-YYYY-MM-DD branch:
  • Checkout bump/v4.X.0, merge master, and push.
  • checkout -b bump/nightly-YYYY-MM-DD
  • git merge --squash nightly-testing
  • resolve conflicts if there are any
  • git push
  • open a PR from this branch, making sure to set the target branch to bump/v4.X.0.

and that gets us back to the start of the cycle. :-)

[Kim Morrison]

And note also: when nightly-testing is first moved to a new nightly, it's worth checking if there are any relevant lean-pr-testing-XXXX branches with existing adaptation work. Ideally, we would post about the existence of such branches ahead of time on this stream for visibility.

Maybe a good way to say this is that a very early step of dealing with any seriously broken nightly-testing is to go to https://github.com/leanprover/lean4-nightly/releases, see which Lean commits were part of that nightly, and then post in a thread here that we expect lean4#XXXX and or lean4#YYYY to be the sources of problems. This is a good moment to check for existing lean-pr-testing-XXXX branches and merge them.

[Kim Morrison]

Finally, all these instructions also hold for Std, except that usually it has fewer, easier, problems. So typically it is safe to not pay any attention to Std, unless on Mathlib's nightly-testing branch you are getting failures in Std. If that's happening, apply this whole routine to Std, and then make sure to run lake update std after you've pushed to Std's nightly-testing.

[Ruben Van de Velde]

And also that most people can't push to Std branches

[Kim Morrison]

Oh, hmm. Okay, if I'm on holiday make PRs to fix Std, and/or recruit @Joe Hendrix and @Mario Carneiro!

[Ruben Van de Velde]

(Maybe the bot should also post to a thread in the #std4 stream?)