RQ-61-EXTRACT (#1080): delete 98 stale extraction snapshot files + the dune tree nothing runs; docs stop contradicting their own headers

[avrabe]

RQ-61-EXTRACT: delete the checked-in extraction snapshots nothing reads, and un-contradict the docs that cited them

Refs #1080. Executes the issue's option 1 with the scope the maintainer measurement enlarged to all four directories — after an independent consumer census that confirmed it (and widened the file count once more).

Independent consumer census (re-verified, not trusted)

Checked every workflow, every *.bazel/*.bzl, the only Makefile (coq/Makefile), coq/_CoqProject, every dune/dune-project, scripts/, claims.yaml, and a repo-wide text search for the snapshot basenames. No consumer exists:

• coq/BUILD.bazel's rocq_library(name = "extraction") consumes only Synth/Extraction/CompilerExtract.v — the .v source, never the committed .ml. That target is untouched and still a dep of rocq_proofs.
• dune appears in no workflow, bazel file, Makefile, or script. The dune tree was self-contained (compiler/dune copy_files'd from validation/).
• One near-miss the issue census did not name: root BUILD.bazel had a filegroup(name = "test_data") globbing validation/**/*.wat. Zero consumers of //:test_data anywhere (the renode tests use //examples/wat:simple_add.wat, a different file), and with validation/ gone the empty glob would error under Bazel 8 — so the filegroup is deleted with the directory.
• claims.yaml pins glob only coq/**/*.v paths — no pin names the snapshots. claim_check is 54/54 green on the branch.

Spot-checks of the issue numbers: staleness confirmed (BrIf — 2 hits in WasmInstructions.v, 0 in the committed WasmInstructions.ml); the 61-.ml census confirmed exactly (19/18/23/1); one addition — coq/ also carried 19 .mli siblings the census missed, same class, deleted with the rest.

Commit 1 — the deletion (107 files, −12,488 lines)

path	what went
coq/*.ml + coq/*.mli	19 + 19 snapshots, up to nine months stale
extracted/	18 .ml + 18 .mli + dune — a library nothing links
validation/	23 .ml, dune files, poc_validator.md, README.md, test_cases/simple_add.wat — three executables nothing executes
compiler/	synth_compile.ml + dune
dune-project	root
BUILD.bazel	the unconsumed //:test_data filegroup

Commit 2 — the docs stop arguing with their own headers

• docs/validation/VALIDATION_STATUS.md — body rewritten. It opened with "has not been implemented … do not exist" and then said "Successfully implemented", "40 files total, ~80KB", "Status: Complete and ready for use ✅". It now describes only what exists: extraction as a CI Bazel target re-run every proof build, and the validation machinery that actually ships.
• docs/validation/COMPREHENSIVE_VALIDATION_REPORT.md — historical-record header (it reports a real 2025-11 run of the now-removed executables; reproduce commands no longer apply).
• docs/build-systems/COQ_DUNE_SETUP_GUIDE.md — "historical proposal — NOT adopted" header; the repo built proofs under Bazel/rules_rocq, the opposite of this guide's recommendation.
• examples/pid-controller/COMPILER_DEMO.md — historical-demo header (synth_compile.exe no longer exists).
• validation/poc_validator.md went with its directory.

The three analysis/research docs (LOOM_SYNTH_INTEGRATION_PLAN.md, RECOMMENDED_BUILD_ARCHITECTURE.md, BAZEL_INTEGRATION_RESEARCH.md) reference dune only as plan/research content in the future tense and were left as records.

Commit 3 — ledger

RQ-61-EXTRACT.yaml: fields.landed records this PR (stays proposed for the release-close status pass, per the R4 convention #1118 fixed).

Gates

• python3 scripts/claim_check.py claims.yaml — 54/54 hold
• python3 scripts/status_evidence_check.py — green after commit 3
• cargo test --workspace --features riscv — result stated in the PR thread
• bazel test //coq:verify_proofs — the load-bearing one (the .v extraction target must survive its outputs' deletion) — result stated in the PR thread

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

[avrabe]

Gate results (local, exit-code gated)

gate	result
bazel test //coq:verify_proofs	PASS — rc=0, 2/2 tests (//coq:rocq_proofs, //coq:vcr_sel_rules_coverage); the .v extraction target compiled and the proof test ran on the post-deletion tree
cargo test --workspace --features riscv	PASS — rc=0 (no Rust touched; proven, not assumed)
python3 scripts/claim_check.py claims.yaml	PASS — 54/54 claims hold (no pin names the snapshots; all coq globs are *.v-scoped)
python3 scripts/status_evidence_check.py	PASS — 0 failures (R4 acknowledged via fields.landed: PR #1121)

One history note: the branch was force-pushed once, pre-review, to correct a miscount in commit 1's own subject (105 → 98 snapshot files: 61 .ml + 37 .mli). Same content, corrected message.

🤖 Generated with Claude Code

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!