Repository navigation
Decide: protect main branches and require the bar check #10
Description
Item 7 of verified bar v2 (#2) needs each library's default branch to require the bar / bar check. Today no main in the org requires anything, so the check reports item 7 as open on tar#6 and codec#1. Only a repo or org admin can change this.
Proposed rules on main
| Repo | Rule | When |
|---|---|---|
mission |
Require a pull request with an approving review. Then require the self-test, lean-self-test and template / bar checks. |
The review now. The checks once #2 merges, because main has no CI before that. Every library runs the checker from this repo, so a push to mission's main changes every library's verdict. |
codec |
Require bar / bar. |
Now. codec#1 already runs it. |
tar |
Require the check of the PR set that merges: bar / bar for Set B, Proofs and differential tests for Set A. |
After that set merges (tar#7). tar#4 and tar#5 carry no workflow, so a required check would block them for good. |
Also
- Once Verified bar v2: pin reviewed statements and claims, check by machine #2 merges, tag a release from
main, for examplebar-v2. tar and codec then pin the workflow andbar-refto that tag instead of the commit they use now. - Optional, from Verified bar v2: pin reviewed statements and claims, check by machine #2: an org ruleset that requires the verified-bar workflow in every library repo, so a library PR cannot edit its own check away.
- tar's repo settings still overstate it. Its description says "Lean-verified tar (ustar) extractor…", which the audit (Audit the tar pilot against the verified bar; correct its status #1) found it is not yet. Its website field points at the old
proven-commonsrepo. (Noted in tar#1.)
Current work
The protection policy and reconciliation tool are prepared. Live settings remain pending review and application; tar is deferred until its workflow lands.
Awaiting independent review: #27.
Activity