Skip to content

Commit a48dc4e

Browse files
hyperpolymathclaude
andcommitted
fix(docs): repoint README soundness-ledger refs to docs/SOUNDNESS.adoc
README referenced `SOUNDNESS-LEDGER.adoc` (a filename that does not exist) in three places. The soundness single-source-of-truth is `docs/SOUNDNESS.adoc`. This was not cosmetic: `tools/check-soundness-ledger.sh` Property 2 (back-links) does `grep -q "SOUNDNESS.adoc"` over the pointer docs, and the old string did not match, so the soundness-ledger gate (wired into `just check` + CI) was RED: ERROR (property 2): README.adoc no longer links to docs/SOUNDNESS.adoc After the fix the full gate passes (built off system OCaml 4.14.1 + opam, dune 3.24.0): "OK: soundness ledger — all 5 properties hold". Docs-only; no build/behaviour change. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
1 parent 255c0b4 commit a48dc4e

1 file changed

Lines changed: 3 additions & 3 deletions

File tree

README.adoc

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ Early and experimental. This is *v0.2*: the architecture is settled, the
2727
implementation and the metatheory are partial and still moving. It is suitable
2828
for experimentation, teaching, and small sound components -- not yet for
2929
production. What is proven, what is implemented, and what is still prose are
30-
stated plainly below and tracked in `SOUNDNESS-LEDGER.adoc`.
30+
stated plainly below and tracked in `docs/SOUNDNESS.adoc`.
3131

3232
== What you get
3333

@@ -142,7 +142,7 @@ risk here, and it is not yet solved.
142142
Soundness is *partially mechanised, and honestly tracked.* An initial,
143143
axiom-free, machine-checked result for code-generation preservation exists
144144
(Coq/Rocq). A number of residuals remain open; they are recorded -- not hidden
145-
-- in `SOUNDNESS-LEDGER.adoc`, which states for each claim whether it is
145+
-- in `docs/SOUNDNESS.adoc`, which states for each claim whether it is
146146
mechanised or still argued in prose.
147147

148148
The ledger is the source of truth for what currently holds. This README
@@ -192,7 +192,7 @@ totality cut, and a WebAssembly target -- rather than any one ingredient.
192192
== Documentation
193193

194194
// TODO: link the design notes and the examples directory once locations are stable.
195-
* Soundness status: `SOUNDNESS-LEDGER.adoc`
195+
* Soundness status: `docs/SOUNDNESS.adoc`
196196

197197
== License
198198

0 commit comments

Comments
 (0)