docs+ci+bot: post-PR#100 hygiene sweep (docs, wiki, CI, machine-readable)#101
Merged
Conversation
- Justfile: build-coq now builds all 14 theories (CNO+OND) via coq_makefile; add build-mizar/build-idris/verify (canonical gate → verify-all-provers.sh) + verify-mizar/verify-idris; drop banned rescript/typescript from build-all; fix verify-z3 (cno_properties.smt2 → verify.sh + ond/OND_checks.smt2). - .machine_readable/6a2/STATE.a2ml: refresh proof state to the six-prover completion — tech-stack, per-prover components, working-features, milestones, blockers, next-actions, and a 2026-07-06 session-history entry. - README.md: OND no longer "design/roadmap stage" (OND-1..5 proved); fix directory tree (ond/, verify-all-provers.sh); rewrite prerequisites/build to the real toolchains (drop banned npm/rescript, add all six provers + Idris). - ROADMAP.adoc: rewrite "Honest Current State" to the reproduced reality; flip OND status to OND-1..5 landed / OND-6 open. - docs/OND-PILLAR-STRUCTURE.adoc, docs/MACHINE_VERIFICATION.adoc: dated status banners; OND modules authored, examples marked historical. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Human docs:
- AUDIT.adoc: move AUDIT-2026-05-20-A (Idris Types.idr) to Resolved; log the
three unsound-axiom removals + six-prover completion; fix stale META.scm paths.
- CHANGELOG.md: Unreleased entries for the two-pillar completion, proofs CI,
unsound-axiom fixes, Idris ABI repair.
- docs/{VERIFICATION_RESULTS,PROOF-COMPLETION-PLAN,PROOF-CLASSIFICATION}.adoc,
docs/{proof-debt,proof-debt-triage}.md: dated status banners (historical
content preserved; current state → PROOF-STATUS.adoc).
- docs/wiki/{Home,Proof-Systems,Verification,Roadmap,FAQ}.md: refresh proof
numbers (11/11→14/14, +OND, +six provers), fix stale META.scm path.
Bot docs (.machine_readable/6a2/):
- AGENTIC.a2ml: correct dangerously-stale directives — lean4-sorry 18→0,
coq-admitted 19→0; Lean/Idris now safe to edit; no-new-axiom rule.
- META.a2ml: ADR-011..014 (OND model, OND-1..5 landed, unsound removals,
class-A acceptance); ADR-005 accepted.
- NEUROSYM.a2ml, PLAYBOOK.a2ml: refresh prover list + build/verify procedures.
CI:
- .github/workflows/proofs.yml: new — Coq (14 theories) + Z3 proof verification
on PRs touching proofs/ (lightweight provers feasible on standard runners).
Note: docs/wiki (13 pages) is NOT published to the live GitHub wiki (a 1-line
stub, no sync workflow) — flagged for an owner decision, not pushed here.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
Jul 7, 2026
## Summary Follow-up to the completed docs sweep (#101), doing the two things flagged there plus the wiki publish (already pushed live — see below). ### 1. `6a2/` → `descriptiles/` (estate naming mandate) The machine-readable metadata family is `descriptiles`; `6a2` is fully deprecated (estate mandate 2026-06-30, `standards/CANONICAL-NAMES.adoc`). This renames `.machine_readable/6a2/` → `.machine_readable/descriptiles/` (as git renames, history preserved) and migrates **every** `6a2` reference across the repo (21 files: docs, wiki, AUDIT, GOVERNANCE, RSR_COMPLIANCE, the contractile `Mustfile` validation invariants, `.well-known/ai.txt`, and the metadata files' own cross-references). Zero residual `6a2`. ### 2. Harden the proofs CI (`.github/workflows/proofs.yml`) - Three **independent** jobs — Coq (14 theories, both pillars), Agda (CNO + OND), Z3 (CNO + OND bounded) — so one flaking never reds the others. - Pinned to **`ubuntu-24.04`** (ships Coq 8.18 — exactly what the proofs need) to stop apt version drift; `concurrency` cancel-in-progress; SHA-pinned checkout; `contents: read`. - Heavy provers (Lean+Mathlib, Isabelle, Mizar, Idris) stay on the local gate `proofs/verify-all-provers.sh`, documented in-file. ### Wiki (done, live) The 13-page `docs/wiki` — previously **never published** (the live wiki was a 1-line stub) — has been published to the GitHub wiki, with repo-relative links rewritten to `blob/main` URLs and sibling links to wiki-style. `docs/wiki` remains the in-repo source of truth. (Wiki push is separate from this PR.) ## Test `just build-coq` → 14/14; `proofs.yml` validates; `git grep 6a2` → empty. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Estate-hygiene follow-up to PR #100 (the CNO+OND six-prover completion). Brings
the human docs, machine-readable/bot docs, CI, and wiki into line with the
now-completed two pillars. No proof code changes.
Human documentation
toolchains in prerequisites (dropped banned npm/rescript); fixed directory tree
and the
.gitlab-ci.yml→ GitHub Actions reference.reality; OND status → OND-1..5 landed / OND-6 open.
AUDIT-2026-05-20-A(Idris errors, fixed in feat(proofs): complete CNO + OND pillars, verified across six provers #100);logged the three unsound-axiom removals + completion; fixed stale
META.scmpaths.(VERIFICATION_RESULTS, PROOF-COMPLETION-PLAN, PROOF-CLASSIFICATION, proof-debt,
proof-debt-triage); OND-PILLAR-STRUCTURE + MACHINE_VERIFICATION updated.
Machine-readable / bot docs (
.machine_readable/6a2/)next-actions, session-history).
lean4-sorry 18→0,coq-admitted 19→0, "never touch Lean/Idris" removed (they now build); added ano-new-axiom rule.
class-A acceptance).
Build / CI
build-coqnow builds all 14 theories viacoq_makefile; addedbuild-mizar/build-idris/verify(canonical gate) +verify-mizar/-idris;fixed
verify-z3; dropped banned rescript/typescript frombuild-all.PRs touching
proofs/. Lightweight provers only (Lean+Mathlib/Isabelle/Mizarare too heavy for standard runners; the full gate runs via
proofs/verify-all-provers.sh).Owner decisions flagged (not actioned)
docs/wiki(13 rich pages, updated here) is not publishedto the GitHub wiki, which is a 1-line stub with no sync workflow. Wire a
publish workflow or do a one-time push? (Not pushed here — outward-facing.)
6a2/→descriptiles/: the machine-readable dir still uses thedeprecated
6a2name (estate-wide rename, led by rsr-template-repo — left as-is).proofs.ymlruns on every matching PR (Actions minutes).Test
just build-coq→ 14/14;.github/workflows/proofs.ymlvalidates; no proof code touched.🤖 Generated with Claude Code