From a48dc4e1731965e993076a5ef5eb04de71fd43f4 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 7 Jul 2026 00:31:14 +0100 Subject: [PATCH] fix(docs): repoint README soundness-ledger refs to docs/SOUNDNESS.adoc MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- README.adoc | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/README.adoc b/README.adoc index e2177c5..6fdfb92 100644 --- a/README.adoc +++ b/README.adoc @@ -27,7 +27,7 @@ Early and experimental. This is *v0.2*: the architecture is settled, the implementation and the metatheory are partial and still moving. It is suitable for experimentation, teaching, and small sound components -- not yet for production. What is proven, what is implemented, and what is still prose are -stated plainly below and tracked in `SOUNDNESS-LEDGER.adoc`. +stated plainly below and tracked in `docs/SOUNDNESS.adoc`. == What you get @@ -142,7 +142,7 @@ risk here, and it is not yet solved. Soundness is *partially mechanised, and honestly tracked.* An initial, axiom-free, machine-checked result for code-generation preservation exists (Coq/Rocq). A number of residuals remain open; they are recorded -- not hidden --- in `SOUNDNESS-LEDGER.adoc`, which states for each claim whether it is +-- in `docs/SOUNDNESS.adoc`, which states for each claim whether it is mechanised or still argued in prose. 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. == Documentation // TODO: link the design notes and the examples directory once locations are stable. -* Soundness status: `SOUNDNESS-LEDGER.adoc` +* Soundness status: `docs/SOUNDNESS.adoc` == License