Skip to content

Commit 9b87ef4

Browse files
hyperpolymathclaude
andcommitted
chore(docs): tidy — stale Idris module count 22→24 + drop CODEOWNERS template residue
Safe-auto items from the repo tidy-up audit (#7): - docs/proof-debt.md + docs/wiki/Proof-Debt-Status.md: "22/22 modules" / "22 Idris2 modules" → 24 (verified: find src/abi -name '*.idr' | wc -l = 24; AFFIRMATION.adoc already records 24 — these were the laggards). - .github/CODEOWNERS: remove the dead "Replace hyperpolymath with..." scaffold comment (the substantive owner rules below it are correct). Purely factual / dead-comment edits; no renames, dates, or licence/owner lines touched. Larger findings are owner-gated and listed separately. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
1 parent cef36e4 commit 9b87ef4

3 files changed

Lines changed: 4 additions & 5 deletions

File tree

.github/CODEOWNERS

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,6 @@
22
# CODEOWNERS - Define code review assignments
33
# See: https://docs.github.com/en/repositories/managing-your-repositorys-settings-and-features/customizing-your-repository/about-code-owners
44
#
5-
# Replace hyperpolymath with your GitHub username or team
65

76
# Default owners for everything
87
* @hyperpolymath

docs/proof-debt.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
1212

1313
**Zero soundness-relevant escape hatches** in this repo as of 2026-05-26;
1414
**re-confirmed 2026-06-16** (`idris2 --build src/abi/typed-wasm.ipkg` → exit 0,
15-
22/22 modules; marker grep for `believe_me` / `assert_total` / `postulate` /
15+
24/24 modules; marker grep for `believe_me` / `assert_total` / `postulate` /
1616
`sorry` / `Admitted` / `assert_smaller` / holes returns only docstring
1717
disclaimers).
1818

docs/wiki/Proof-Debt-Status.md

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -18,11 +18,11 @@ This page is for readers asking _"where is the theorem?"_ when faced with typed-
1818
- **0 `assert_smaller`** in the checked package
1919
- **`%default total`** everywhere
2020

21-
Verified by `tests/proof/regression.mjs` (107 named-theorem grep assertions) and by `idris2 --build src/abi/typed-wasm.ipkg` (22/22 modules under Idris2 0.8.0).
21+
Verified by `tests/proof/regression.mjs` (107 named-theorem grep assertions) and by `idris2 --build src/abi/typed-wasm.ipkg` (24/24 modules under Idris2 0.8.0).
2222

2323
## The proof package
2424

25-
22 Idris2 modules. Per-module status is in `LEVEL-STATUS.md` §"Proof inventory"; the headline:
25+
24 Idris2 modules. Per-module status is in `LEVEL-STATUS.md` §"Proof inventory"; the headline:
2626

2727
| Module | Role |
2828
|---|---|
@@ -181,7 +181,7 @@ The agreement records introduced in PR #79 close the loop: a drift between the R
181181
```bash
182182
# Build the proof package
183183
IDRIS2_PREFIX=$IDRIS2/0.8.0 idris2 --build src/abi/typed-wasm.ipkg
184-
# expects: 22/22 modules, rc=0
184+
# expects: 24/24 modules, rc=0
185185

186186
# Run the proof regression
187187
PATH=$IDRIS2/0.8.0/bin:$PATH \

0 commit comments

Comments
 (0)