workflow

Stream: nightly-testing

[Johan Commelin]

In the past few days I have tried to document and automate the workflows involved in keeping mathlib in sync with new Lean releases.

For starters, please take 30s to read tags and branches > mathlib nightly and bump branches on the community website. (This is a new section that I wrote a few days ago.)

Tl;dr: Lean publishes new nightly releases every day. At the end of the month this becomes a new release. Mathlib adapts to the nightlies on the bump/v4.x.y. At the end of the month, this branch is merged into master without further review.

TL;DR: The branch bump/v4.x.y is part of our "trusted code base". Mathlib maintainers are responsible for reviewing changes to that branch.

---

About automation:

chore: add workflow for merging master into bump/v4.x.y branches #17081

This :this: PR adds a workflow that merges master into bump/v4.x.y several times per day. Usually, there are no problems. If there are problems, it creates a PR and posts it to zulip.

Mathlib maintainers are responsible for reviewing the resulting PR, because it's contents will end up in mathlib without further review.
Of course this is only a merge conflict, so the PR should be uncontroversial.

ci(.github/workflows): add discover-lean-pr-testing.yml #17399

This :this: PR adds a workflow that finds branches of the form lean-pr-testing-NNNNcorresponding to core PRs that have been merged into the latest nightly. These branches should be merged into the nightly-testing branch of
mathlib. The workflow only reports branches that have a non-trivial diff.

In the future, I plan to automate this further. If the merge is trivial, just do it. Otherwise, create a PR and ask for help.

NB: These branches are not part of the TCB. Anything that happens here will be reviewed again at some point, before landing in master.

TODO

Add a workflow that automatically creates PRs for merging nightly-testing into bump/v4.x.y. At the moment there is still a manual step involved in the form of a bot asking us to run a script. See #nightly-testing > Mathlib bump branch reminders .

Whether automated or not. These PRs must be reviewed. Because these changes to bump/v4.x.y will end up in mathlib without further review.
Of course these are only adaptations to changes in Lean. So the PRs should be mostly uncontroversial.

[Yaël Dillies]

I assume by "maintainers" everywhere in your documentation, you mean "maintainers and reviewers"?

[Yaël Dillies]

Btw this :green: looks very close to :orange_circle: to colorblind me, and the :cross_mark: is making me think that it is supposed to be corresponding to a possible github status (ie :check:, :orange_circle: or :cross_mark:), but it is not :check:. Can someone confirm/infirm my understanding of how we are supposed to read this graphic and fix it?

[Yaël Dillies]

In this image, I mean

[Johan Commelin]

There is only the green one. But also, that picture is a bit out-dated in some parts.

[Johan Commelin]

The text should be accurate though

[Johan Commelin]

Yaël Dillies said:

I assume by "maintainers" everywhere in your documentation, you mean "maintainers and reviewers"?

Yes, sorry.