From f7afa5c7959bff99b542dd77b8fd0575a18fcec4 Mon Sep 17 00:00:00 2001 From: fraware Date: Sun, 26 Jul 2026 07:08:12 -0700 Subject: [PATCH] Point default branch docs and CI push triggers at main. Drop master from push triggers after the default-branch switch; keep it on pull_request while legacy PRs drain. --- .github/workflows/ci.yml | 2 +- STATUS.md | 11 +++++------ docs/program/admin-actions.md | 6 +++--- docs/program/board.md | 6 +++--- 4 files changed, 12 insertions(+), 13 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 2553903..1dbc2b5 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -2,7 +2,7 @@ name: CI on: push: - branches: ["main", "master", "recovery/**", "feature/**", "fix/**", "test/**", "docs/**", "release/**"] + branches: ["main", "recovery/**", "feature/**", "fix/**", "test/**", "docs/**", "release/**"] pull_request: branches: ["main", "master", "recovery/**"] diff --git a/STATUS.md b/STATUS.md index 4d27615..45b2bcc 100644 --- a/STATUS.md +++ b/STATUS.md @@ -19,7 +19,7 @@ Everything else formerly advertised under FormalVerifML (neural nets, transforme | Stage | State | |-------|-------| | Truth reset (LV-00) | Complete in working tree | -| Governance templates | Complete in tree; GitHub `master`→`main` rename + remote ruleset **blocked** (admin) | +| Governance templates | Complete in tree; default branch is **`main`**; remote ruleset still **blocked** (admin / CODEOWNERS) | | Build baseline (LV-01) | Lean 4.32.1 + mathlib `v4.32.1` pinned; SHA-pinned CI; Docker elan checksummed | | Affine kernel (LV-02) | Implemented; repeated-weight score equalities via `norm_num`; classify via kernel `decide` after rewrite (F-002; no `native_decide`) | | L∞ theorem + axiom audit (LV-03) | Library + generated `#print axioms` path; leanchecker job (F-001/F-020 addressed in R-01) | @@ -73,8 +73,7 @@ Exit code `0` / status `verified` means the generated Lean module compiled under ## Blockers (do not fabricate completion) 1. Mateo confirmation that Critical/High are closed on the integration tip; Mediums resolved or explicitly accepted (`docs/program/findings-F001-F020.md` + authorization checklist) -2. GitHub default branch rename `master` → `main` (admin) -3. Remote branch ruleset + real multi-party CODEOWNERS reviewers (pending handles in `docs/program/admin-actions.md`) -4. External LV-11 reviewer recruitment, packet completion, and findings resolution -5. Three independent reproductions + artifacts regenerated after final code change -6. RC tag `v0.1.0-rc1`, PyPI publish, and public “released” language **only** after the signed checklist — **not before** +2. Remote branch ruleset + real multi-party CODEOWNERS reviewers (pending handles in `docs/program/admin-actions.md`) +3. External LV-11 reviewer recruitment, packet completion, and findings resolution +4. Three independent reproductions + artifacts regenerated after final code change +5. RC tag `v0.1.0-rc1`, PyPI publish, and public “released” language **only** after the signed checklist — **not before** diff --git a/docs/program/admin-actions.md b/docs/program/admin-actions.md index 8d077ba..9ed7be6 100644 --- a/docs/program/admin-actions.md +++ b/docs/program/admin-actions.md @@ -2,10 +2,10 @@ ## GitHub repository settings (Mateo / org admin) -1. Rename default branch `master` → `main` on https://github.com/fraware/leanverifier +1. ~~Rename default branch `master` → `main` on https://github.com/fraware/leanverifier~~ **Done** (default is `main`) 2. Update local remotes: `git fetch origin` and set upstream tracking to `origin/main` -3. Confirm `origin/HEAD` → `refs/remotes/origin/main` -4. After rename is confirmed and push CI is green on `main`, remove `master` from `on.push.branches` in `.github/workflows/ci.yml` (R-00 keeps both until then) +3. Confirm `origin/HEAD` → `refs/remotes/origin/main` (`git remote set-head origin -a`) +4. ~~After rename, remove `master` from `on.push.branches` in `.github/workflows/ci.yml`~~ **Done** (`master` remains on `pull_request` only while legacy PRs drain) 5. Activate a branch ruleset on `main` **only after** real multi-party CODEOWNERS handles exist: - Required PR reviews (implementer ≠ sole formal reviewer) - Require CODEOWNERS review diff --git a/docs/program/board.md b/docs/program/board.md index 1f7a0de..3ad9c3f 100644 --- a/docs/program/board.md +++ b/docs/program/board.md @@ -5,7 +5,7 @@ | ID | Title | Owner | Status | Blocker | |----|-------|-------|--------|---------| | LV-00 | Truth reset | Mateo | done (in tree) | | -| gov-main | Rename + ruleset + CODEOWNERS | Mateo / admin | templates done | GitHub rename + remote ruleset | +| gov-main | Rename + ruleset + CODEOWNERS | Mateo / admin | default branch `main` done | Remote ruleset + real CODEOWNERS handles | | LV-01 | Build baseline | Mateo | done (in tree) | Local Lean reinstall may need SSL workaround | | LV-02 | Affine kernel | Mateo | done | | | LV-03 | Margin robustness | Mateo | done | Formal reviewer sign-off pending | @@ -21,7 +21,7 @@ ## Admin actions (GitHub) -- [ ] Rename default branch `master` → `main` (requires admin) -- [ ] Set `origin/HEAD` to `main` +- [x] Rename default branch `master` → `main` +- [x] Set `origin/HEAD` to `main` - [ ] Activate branch ruleset on `main` (required reviews, CODEOWNERS, no force-push) - [ ] Confirm CODEOWNERS usernames include non-implementer formal + security reviewers