Skip to content

Finish main default-branch migration #15

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
fraware merged 1 commit into from
Jul 26, 2026
Merged

Finish main default-branch migration #15

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .github/workflows/ci.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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/**"]

Expand Down
11 changes: 5 additions & 6 deletions STATUS.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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) |
Expand Down Expand Up @@ -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**
6 changes: 3 additions & 3 deletions docs/program/admin-actions.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
6 changes: 3 additions & 3 deletions docs/program/board.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 |
Expand All @@ -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
Loading