Skip to content

Commit 3d25fb6

Browse files
hyperpolymathclaude
andcommitted
docs(#176): restore the DOC-04 status banner and fix 3 dead ledger links
3661d98 removed the DOC-04 banner from README's "Status" section, which tools/check-doc-truthing.sh requires. That failure has held the `build` job red on main since 2026-06-28. Also repoints three references to `SOUNDNESS-LEDGER.adoc` -- a file that does not exist -- at docs/SOUNDNESS.adoc. tools/check-doc-truthing.sh now exits 0. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
1 parent 8abeaaa commit 3d25fb6

1 file changed

Lines changed: 13 additions & 3 deletions

File tree

‎README.adoc‎

Lines changed: 13 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -23,11 +23,21 @@ delivery mechanism. They _are_ the product.
2323

2424
== Status
2525

26+
[IMPORTANT]
27+
====
28+
Authoritative per-feature status lives in
29+
link:docs/CAPABILITY-MATRIX.adoc[docs/CAPABILITY-MATRIX.adoc]; soundness-hole
30+
status lives in link:docs/SOUNDNESS.adoc[docs/SOUNDNESS.adoc]. Where this
31+
README and those documents disagree, *they win* --
32+
`.machine_readable/descriptiles/STATE.a2ml` mirrors the matrix and does not
33+
lead it.
34+
====
35+
2636
Early and experimental. This is *v0.2*: the architecture is settled, the
2737
implementation and the metatheory are partial and still moving. It is suitable
2838
for experimentation, teaching, and small sound components -- not yet for
2939
production. What is proven, what is implemented, and what is still prose are
30-
stated plainly below and tracked in `SOUNDNESS-LEDGER.adoc`.
40+
stated plainly below and tracked in link:docs/SOUNDNESS.adoc[docs/SOUNDNESS.adoc].
3141

3242
== What you get
3343

@@ -142,7 +152,7 @@ risk here, and it is not yet solved.
142152
Soundness is *partially mechanised, and honestly tracked.* An initial,
143153
axiom-free, machine-checked result for code-generation preservation exists
144154
(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
155+
-- in link:docs/SOUNDNESS.adoc[docs/SOUNDNESS.adoc], which states for each claim whether it is
146156
mechanised or still argued in prose.
147157

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

194204
// TODO: link the design notes and the examples directory once locations are stable.
195-
* Soundness status: `SOUNDNESS-LEDGER.adoc`
205+
* Soundness status: link:docs/SOUNDNESS.adoc[docs/SOUNDNESS.adoc]
196206

197207
== License
198208

0 commit comments

Comments
 (0)