Keep the link.
Recheck the judgment.
A port needs two kinds of memory: which declarations correspond, and which exact versions someone reviewed. Covmap helps with the first. Its content hashes give us a way to build the second without writing labels into rapidly changing code.
This experiment imports the existing Atlas’s approximate matches into real covmap segments and links. The graph still comes from coqdep and dpdgraph; covmap does not infer those dependencies or prove that Lean matches Coq.
The whole snapshot, mapped
Segments partition lines, so several generated declarations on the same line share one segment. Only the first candidate for each declaration was imported. “Unmatched” means the matcher found no candidate, not a confirmed omission from the port.
In the native report, green means linked, not reviewed or proved equivalent. The explorer retains the original Atlas review colors.
Four small, replayable experiments
Loading executed test receipts…
The snippets below are deliberately tiny synthetic fixtures, not changes to FloatSpec. No Lean or Rocq compilation is claimed for these mutation tests; they test covmap’s drift and linking behavior.
What I would build on this
- Stable correspondence: retain named links when declarations move or are rewritten.
- Version-bound review: store a separate verdict with both source hashes, the reviewer, and evidence.
- Invalidate, don’t erase: when either hash changes, keep the historical verdict but mark it “needs re-review.”
This site demonstrates that freshness check; it does not yet provide manual review editing. That remains the separately requested future tool.
Reproduce it
cargo test --locked
cargo build --release --locked
node scripts/covmap-import.mjs
node scripts/test-covmap.mjs
node scripts/test-covmap-data.mjsRun Cargo inside the pinned covmap checkout. The importer seeds a fresh .covmap and refuses to overwrite an existing mapping. The test harness creates isolated temporary repositories; no live port files are edited.
OathTech/covmap source ↗ · Full mutation receipts ↓ · Apache 2.0 license