Waiting for nightly-testing-2023-11-24

Stream: mathlib4

[Joachim Breitner]

I am waiting for the nightly-testing-2023-11-24 branch to be created, so that I can test some lean PRs against it. The lean nightly release has happened, and mathlib nightly is on 2023-11-24. But the branch nightly-testing-2023-11-24 is not created.

I think what’s happening is that the .github/workflows/nightly_detect_failure.yml workflow, which will push to the branch (and thus create it), only runs after CI completes on the nightly-testing branch. But whenever something is pushed to master, that gets merged into nightly-testing, and that cancels the running CI, as one can see here. So the daily branch is only created when there wasn’t activity on master in a while. Does that sound right?

Not sure what solution to offer. Pinging poor @Scott Morrison about this…

[Scott Morrison]

Yes, that's a correct description of what is happening.

[Scott Morrison]

A few workarounds / solutions.

1. Check ahead of time which nightly-testing-YYYY-MM-DD branches exist already, and based your Lean PRs off a corresponding nightly, rather than the latest one.
2. We can automate that so that there's a tracking branch at leanprover/lean4 for the latest Mathlib-tested nightly.
3. We add automation so that at Mathlib we only merge master into nightly-testing either every X hours, or explicitly once the previous CI is done.
4. We create a staging-nightly-testing-YYYY-MM-DD which has nightly-testing merged into it either every X hours, or when CI is done.

[Scott Morrison]

I think 3 is the best immediate solution, perhaps with X=2 or 3.

[Scott Morrison]

Option 2 can also be implemented independently. Perhaps at Lean we can have nightly tracking the latest nightly release and nightly-tested fire the latest nightly release on which Mathlib's nightly-testing branch has succeeded?

Happy to have a name suggestion there.

[Joachim Breitner]

Do even need to update nightly-testing more than once per day? If the purpose is to test lean, it doesn't matter a lot of you have a few more mathlib commits in or not, does it?
(So option 2, but “daily”)

nightly-with-mathlib might be a descriptive name?

[Scott Morrison]

There is some value in more frequent updates, to make it easier to work out which Mathlib commit may have caused a problem. But it's not a lot of value.

[Joachim Breitner]

Yeah, I guess it depends on how often that is, and how annoying to have to git bisect manually if it does break.

[Scott Morrison]

#8627 (only bump nightly-testing every 3 hours)

[Scott Morrison]

And #8628 for the nightly-with-mathlib branch on the Lean repository.