docs(roadmap): truthfulness audit — sync §2/§3/§4 to actual state#129
Merged
Conversation
The 2026‑04‑20 ROADMAP revision had drifted from reality on five rows.
This commit syncs each row to what `handover/TODO.md`, `handover/STATE.md`,
`docs/PROVER_COUNT.md`, and the actual commit history say.
Corrections:
* §2 stage 1c "residual extractor gaps fixed [in progress, 28 to go]"
→ "[done 2026‑04‑26 ✓ — 50/50 named extractors]".
TODO.md documents three S1 batches (12 + 20 + 6) landing the full 50.
* §2 stage 4c "86/91 done; 5 suggest_tactics stubs remain"
→ "91/91 real impl ✓; 5 still heuristic-only — GNN-ranking is the
end-state target".
PROVER_COUNT.md is the canonical source: 91 of 91 have real impl;
the "5" are heuristic-only (not stubs) and GNN-ranking is what would
promote them.
* §3 row "Every important solver" Today column: same fix as 4c —
"5 suggest_tactics stubs" → "91 / 91 with real `suggest_tactics`
(5 still heuristic-only)".
* §4 row S1 status: "in flight" → "done 2026‑04‑26 ✓ (50/50)".
* §4 row S4 status: "design pending — needs Verisim schema"
→ "wired 2026‑04‑27 ✓" with the actual current state (read paths,
write path, end-to-end test, runbook). The same section's "Sprint
critical path" subsection already documented this; the table row was
the stale piece.
* §4 row S5 status: updated to reflect that `gnn_augment_tactics` is
wired into the 5 pilot backends per c4bc272, and that the remaining
work is precisely the 5 heuristic-only backends from PROVER_COUNT.md.
* "Last revised" bumped to 2026‑05‑30, prior date preserved.
No new claims are added; this is a pure stale-row sync.
Refs: §7 "How to update this roadmap" sub‑item — "When a stage sub‑item
lands, mark its line `[done YYYY‑MM‑DD ✓]` in §2 and update the
corresponding row of §3."
hyperpolymath
force-pushed
the
docs/roadmap-truthfulness-audit
branch
from
3273edb to
0ce9aa4
Compare
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
Targeted sync of five drifted rows in
docs/ROADMAP.mdto whathandover/TODO.md,handover/STATE.md,docs/PROVER_COUNT.md, and the commit history actually say. No new claims, no scope change — pure stale-row cleanup.Corrections
[in progress, 28 to go][done 2026‑04‑26 ✓ — 50/50 named extractors][86/91 done; 5 suggest_tactics stubs remain][91/91 real impl ✓; 5 still heuristic-only — GNN-ranking is end-state]5 suggest_tactics stubs91/91 with real suggest_tactics (5 still heuristic-only)in flightdone 2026‑04‑26 ✓ (50/50)design pending — needs Verisim schemawired 2026‑04‑27 ✓(read paths + write path + tests/s4_loop_closure.rs)partly done — 86/91 already realmostly done — 91/91 real; gnn_augment_tactics wired into 5 pilots per c4bc272Why now
Found during a wider triage of open issues + active CI work. The 5 rows above conflict with documents/commits/code that explicitly disagree; per §7 ("When a stage sub-item lands, mark its line [done YYYY‑MM‑DD ✓]"), they were due for an update.
Test plan
Notes
This PR addresses only the truthfulness drift. The broader CI red on
main(compile errors from the dependabot major bumps) is being addressed in PR #128.