docs: resolve verified .md to .adoc structural drift (#242) - #393
Merged
Merged
Conversation
Retarget 338 stale path references across 83 files where the AsciiDoc counterpart exists at the identical path. Pure reference swap: 239 insertions / 239 deletions. No file was renamed, created or deleted to clear an alert. Load-bearing fixes beyond navigation: - .github/canonical-references/prover-counts.yml declared canonical_pointer: docs/PROVER_COUNT.md, which does not exist, so the R5a canonical-reference guardrail was pointing at nothing. It now resolves. - The Justfile er-schema-drift-check recipe ran sha256sum against docs/architecture/VERISIM-ER-SCHEMA.md and therefore failed on a missing file. It now hashes the real document. No pinned hash was invalidated: .machine_readable/er-schema.sha256 does not exist. Names that merely contain a migrated basename were left alone (FUTURE_DEVELOPMENT_ROADMAP.md, PROVER_EXPANSION_ROADMAP.md, CORRECTNESS-ARCHITECTURE.md, ECHIDNA-TODO.md). Adds docs/STALE-REFERENCE-TOMBSTONES.adoc, recording each old to new path pair, the references deliberately left in place (dated records, external and cross-repo paths, the playground sub-project) and the targets that were never renames: .machine_readable/6a2/ and src/rescript/ are absent, and all 33 .hypatia-ignore exemptions name deleted .res files. Machine-readable state files stay parseable: every touched .a2ml file has identical line count and identical TOML validity to HEAD. Dangling repository-internal doc targets: 129 -> 112. Refs #242 Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
arena-ai-coding-agent
Bot
requested a review
from hyperpolymath
as a code owner
September 25, 2026 14:28
|
Important Review skippedBot user detected. To trigger a single review, invoke the ⚙️ Run configurationConfiguration used: Organization UI Review profile: ASSERTIVE Plan: Advanced Run ID: You can disable this status message by setting the Use the checkbox below for a quick retry:
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
Second pass over the same structural-drift class as the previous commit. The first pass covered the 16 highest-volume targets; this one sweeps every remaining .md reference that has a verified .adoc counterpart. 151 further sites retargeted across 61 files, bringing the change to 502 references across 109 files. No file was renamed, created or deleted. The sweep is gated on target existence rather than blind rewriting, so two false-positive classes are excluded: - References to files that genuinely exist as .md are left alone. 47 references fall in this class over the 21 tracked .md files (SECURITY.md, CLAUDE.md, GEMINI.md, .github/CONTRIBUTING.md, .github/PROVEN-INTEGRATION.md, docs/wiki/*.md, GitLab templates). SECURITY.md coexists with SECURITY.adoc and is not stale. - Names that merely contain a migrated basename are left alone (FUTURE_DEVELOPMENT_ROADMAP.md, CORRECTNESS-ARCHITECTURE.md, ECHIDNA-TODO.md, PROVER_EXPANSION_ROADMAP.md). Two further guardrail fixes, same species as canonical_pointer: - .github/canonical-references/prover-counts.yml listed AUTHORS.md and CODE_OF_CONDUCT.md in scope.include. Neither exists, so the R5a guardrail was not scanning those surfaces at all. - Justfile er-schema-drift-check and the CREUSOT-SETUP path resolved to missing .md files. docs/STALE-REFERENCE-TOMBSTONES.adoc is updated with the full migration table, the deliberately-preserved sites (dated records, the echidna-playground sub-project, external and cross-repo paths, the dual-spelling fallback probes) and the 100 sites that name a path absent in both spellings, which are follow-ups rather than edits. Machine-readable state files stay parseable: zero TOML-validity regressions across the touched .a2ml files. Dangling repository-internal doc targets: 112 -> 108 (129 before the first pass). Refs #242 Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
hyperpolymath
approved these changes
Sep 25, 2026
This was referenced Sep 25, 2026
hyperpolymath
added a commit
that referenced
this pull request
Sep 25, 2026
…ion (#251) (#395) Two independent pieces of work, one commit each. They are separate from the `#242` change already merged as #393 (that content is byte-identical to `main`; this branch's delta against `main` is exactly the 18 files touched by the two commits below). - `52c5fba` — `feat(chapel): per-prover outcome telemetry for bench_mrr` (#162) - `128fc53` — `fix(docs): reconcile prover counts to the canonical source` (#251) --- ## #162 — `bench_mrr` per-prover outcome telemetry The L2.3 cancellation ADR introduced `exitCode = -5` for preempted losers, distinct from `-3` (timeout) and `-4` (subprocess error), but `bench_mrr` only reported success + winning prover per strategy run — so the wall-clock gain attributable to preemption was not measurable. **Outcome model** (`src/chapel/parallel_proof_search.chpl`, +178/−…) - `enum ProverOutcome` — `completed_success`, `completed_failure`, `not_available`, `timed_out`, `preempted`, `subprocess_error`, `not_attempted` — plus `outcomeLabel`, `categoryLabel`, `classifyOutcome`, mapping the documented exit-code contract: `0` success, `>0` prover rejection, `-1` not on PATH, `-2` temp-file write failure, `-3` timeout, `-4` spawn/IO error, `-5` preempted. `-2` and `-4` both mean "the prover never got a fair hearing", so they collapse into `subprocess_error`. - `NotAttempted` is deliberately **not** an exit code: sequential search returns at the first success, so provers after the winner are reported as `not_attempted` rather than silently vanishing from the breakdown. - Each strategy gets a telemetry variant filling a per-prover `results`/`attempted` table indexed by `provers.domain` — **not** `ProverInfo.id` — so category-filtered registries stay correctly indexed. The existing public procs are now thin wrappers, so what the bench measures and what it reports are the same code path. `coforall (prover, i) in zip(...)` became `coforall i in provers.domain`. **Outputs** (`src/chapel/bench_mrr.chpl`, +274) - stdout wall-clock CSV, columns unchanged. - `--telemetry-out` (default `src/chapel/bench_mrr_telemetry.csv`): `fixture,strategy,prover,prover_id,category,outcome,exit_code,wallclock_s`, one row per prover per fixture × strategy, never omitting rows (360 for the stock 4-fixture × 3-strategy matrix). - `--summary-out` (default `src/chapel/bench_mrr_summary.csv`): per fixture × strategy plus an `ALL` row per strategy aggregating the corpus, with `preemption_rate = preempted ÷ attempted_total` measured against provers that actually ran. - `--telemetry-only=true` suppresses only the stdout wall-clock table; searches still run and the in-file timings stay populated. Also: `just bench-chapel-mrr` now echoes the two output paths to stderr; new `just bench-chapel-mrr-telemetry` prints the per-strategy `ALL` rows; the generated CSVs are gitignored; `docs/bench/README.adoc` documents the column contracts, the outcome table and the re-run procedure. ### Verification — please read **This change could not be compiled or run here: there is no Chapel toolchain in this environment (`chpl` is absent), and `just` is not installed.** What was done instead: - brace balance checked in both files (23/23, 65/65); - every symbol the rewritten `bench_mrr` references was confirmed to exist in `parallel_proof_search.chpl`; - the Justfile recipes were read back by eye only. Consequently **the acceptance criterion "re-run the `docs/bench/` writeup showing preemption rates next to wall-clock" is not satisfied by this PR.** `docs/bench/README.adoc` records the re-run procedure, and `docs/bench/2026-05-30-chapel-mrr-baseline.adoc` is explicitly left un-refreshed rather than filled with estimates that were never produced by a real run. A Chapel-enabled reviewer should run `just bench-chapel-mrr-telemetry` and refresh the readings before this is considered done. Closes #162 once the re-run lands. --- ## #251 — reconcile prover-count drift across surfaces **Premise correction:** the issue names `docs/PROVER_COUNT.md` as canonical. That file does not exist and never has in this checkout (no rename history — the tree is one squashed commit). The canonical file is `docs/PROVER_COUNT.adoc`. Measured against the tree (not against other docs): | Figure | Meaning | Value | |---|---|---| | `V` | `ProverKind` variants in `src/rust/provers/mod.rs` | **141** | | `F` | backend implementation files in `src/rust/provers/` | **105** | | `S` | implementations exposing `suggest_tactics` | **102** | | `D` | variants carrying a type-checker / discipline role | **46** | | `C` | `ProverKind::all_core()` — default REST surface | **12** | `docs/wiki/Home.md` already deferred to canonical, and a run of the R5a guard's own patterns against its own `scope.include` produced **0 violations** — the drift lives where the guard does not look: `docs/`, `.machine_readable/`, `crates/`. **Live surfaces corrected** (each claimed 128 or 30 as today's figure): - `docs/ARCHITECTURE.adoc` — diagram + tier overview. The Tier 1 list also named F*, Idris 2, Alt-Ergo, Dafny, Vampire and E Prover, **none of which are in `all_core()`**; it now lists the actual set (Coq, Lean, Agda, Isabelle, Z3, CVC5, Metamath, HOL Light, Mizar, PVS, ACL2, HOL4). ASCII-art box widths preserved (76 cols). - `docs/ROADMAP.adoc` — endpoint-target row now cites canonical instead of restating denominators; the self-contradictory "91/91 … (5 still heuristic-only)" is gone. - `docs/architecture/VERISIM-ER-SCHEMA.adoc`, `docs-site/content/api/graphql.adoc`, `docs/ECOSYSTEM-INTEGRATION.adoc`, `docs/practice/SOFTWARE-DEVELOPMENT-APPROACH.adoc`, `docs/ASPECT_IMPLEMENTATION_SUMMARY.adoc` ("all 12" → "all Tier 1 (core)"). **Live gates de-numbered** so they cannot drift again (the canonical file's own advice — cite it, don't restate a number): `docs/maintenance/MAINTENANCE-CHECKLIST.adoc` and `.machine_readable/policies/MAINTENANCE-AXES.a2ml` ("All 30 prover backends compile…" → "All prover backends compile…"). **Machine-readable catalogue regenerated:** `.machine_readable/provers.a2ml` declared `count = 113` against a 141-variant enum — a strict subset with zero extras, i.e. plainly stale (dated 2026-04-24). Regenerated with the repository's own `scripts/gen-provers-a2ml.sh`, so slugs come from the same sed pipeline: 141 sections, parses as TOML, and **all 113 pre-existing entries are byte-identical** (diff is 86 insertions / 2 deletions). Its documented consumer, `backend-matrix.yml`, no longer exists anywhere in `.github/workflows/` and nothing else reads the file — so no CI side effects, but it does mean the "one job per prover" matrix CI it was written for is absent rather than merely stale. **Generator:** `scripts/gen-provers-a2ml.sh` emitted a frozen `date = "2026-04-24"`; the date is now evaluated at run time (emitted outside the quoted heredoc, which must stay quoted because the comment block contains backticks). Left alone deliberately: the template's `AGPL-3.0-or-later` header against the committed file's `MPL-2.0` header — the root `LICENSE` is AGPL, so which line is right is a licensing call, and a regeneration must not silently flip it. **Recorded, not edited:** `docs/PROVER_COUNT.adoc` gains a *Surface reconciliation* section listing every counted surface with a disposition — corrected / de-numbered / **record** (release notes, dated audits, `CHANGELOG`, campaign logs, `TEST-NEEDS`, handover snapshots, `descriptiles/STATE.a2ml`, `src/chapel/RESULTS.adoc`, `audits/`) — plus the deferred follow-ups (`crates/echidna-mcp` tool descriptions, `src/rust` doc comments, `tests/` comments, `docs/LEARNING-ARCHITECTURE.adoc`) and the re-check command. Dated snapshots keep their authoring-time figures on purpose. Closes #251. --- ### Review notes - No compiler for either language is available here, so **#162 is unverified by execution** and #251's changes are verified by measurement, TOML parsing and diff inspection only. - `.machine_readable/provers.a2ml` is the largest generated change: review it as a generated artefact (86 added lines = 28 new variant blocks + 2 metadata lines). --------- Co-authored-by: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.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.
Fixes #242 (the verified subset).
What this is
The
SD022/SD007structural-drift alerts are essentially one mechanical class: documentation was converted from Markdown to AsciiDoc, and 32+ files still referenced the.mdspelling of a filename whose.adoccounterpart exists at the identical path. Nothing was renamed to make an alert disappear.502 references retargeted across 109 files, in two passes: the 16 highest-volume targets first, then a systematic sweep for every remaining
.mdreference with a verified.adoccounterpart. No file was renamed, created or deleted to clear an alert.The sweep is gated on target existence, not blind rewriting — which catches two false-positive classes: names that merely contain a migrated basename (
FUTURE_DEVELOPMENT_ROADMAP.md,CORRECTNESS-ARCHITECTURE.md,ECHIDNA-TODO.md), and references to files that genuinely exist as.md(47 sites:SECURITY.md,CLAUDE.md,GEMINI.md,.github/CONTRIBUTING.md,docs/wiki/*.md, GitLab templates).SECURITY.mdcoexists withSECURITY.adocand is not stale — an earlier, looser version of the sweep rewrote it inAUTHORS.adocand was caught by this check.Two load-bearing fixes beyond navigation
.github/canonical-references/prover-counts.ymldeclaredcanonical_pointer: docs/PROVER_COUNT.md, which does not exist (the canonical file isdocs/PROVER_COUNT.adoc). Every "defer to the canonical reference" rule was pointing at nothing. The same file'sscope.includelist also namedAUTHORS.mdandCODE_OF_CONDUCT.md— neither exists, so those two surfaces were outside the scan entirely.er-schema-drift-checkransha256sum docs/architecture/VERISIM-ER-SCHEMA.md— a missing file. It now hashes the real document. No pinned hash was invalidated:.machine_readable/er-schema.sha256does not exist, so there was no stored constant to recompute.Verification
Each of the 16 migration targets was confirmed by existence at the identical path before replacement, so every mapping is verified rather than inferred:
Checks run:
.a2mlfiles have identical line counts and byte-identical TOML validity vsHEAD(checked withtomllibagainst both revisions — no regressions).FUTURE_DEVELOPMENT_ROADMAP.md,PROVER_EXPANSION_ROADMAP.md,CORRECTNESS-ARCHITECTURE.md,ECHIDNA-TODO.md..adocreferences on added lines resolve (the 9 apparent misses are bare basenames in prose, unresolvable in both spellings before and after; the one relative link../PROVER_COUNT.adocresolves correctly).Acceptance: verified path or documented tombstone
docs/STALE-REFERENCE-TOMBSTONES.adocis the receipt. It records the old→new pairs, plus every reference deliberately left alone:docs/tech-debt-2026-05-26.adocCHANGELOG.md: Y) — the name is the subject of the record; rewriting it would falsify the snapshotdocs/reports/audit/2026-03-31-*.adocdocs/DEBT.adocD5/D6docs/ARCHITECTURE.md")echidna-playground/SECURITY.adoc~/Desktop/…,verification-ecosystem/echidna/….machine_readable/bot_directives/methodology.a2mlfallback-fileslist that names both spellings — configuration, not a referenceNot renames — flagged, not touched
.hypatia-ignoreexemptions name deleted.resfiles.src/rescript/andsrc/provers/are gone. The ledger's own header says entries should be removed as files are migrated or deleted. Per Resolve structural drift stale path references as lifecycle hygiene #242's safety note, a policy/state file is not rewritten to clear alerts — recorded for a one-line owner decision..machine_readable/6a2/does not exist, yet contractile configs (dust.k9.ncl,must.k9.ncl,trust.k9.ncl) point at.machine_readable/6a2/DRIFT.a2mlandratification-<session-id>.a2ml. Neither the directory norDRIFT.a2mlexists anywhere.verification/pareto.rs,scripts/retrain_from_verisim.jl,docs/buchholz-plan.adoc, …) — files that never existed, needing a decision rather than a search-and-replace.Out of scope (upstream,
hyperpolymath/standards)Two #242 acceptance criteria belong to Hypatia itself, not this repo: emitting the specific old/new path pair in
SD022output, and displaying the category aslifecycle-hygiene/repository-structure.Note on #251
docs/PROVER_COUNT.md— named as canonical by #251 and byCLAUDE.md— never existed. The canonical file isdocs/PROVER_COUNT.adoc, and it is now correctly referenced. That unblocks the #251 count reconciliation.