Skip to content

Commit 2a3da6c

Browse files
fix(docs): README back-links + real LICENSE section (unblocks 2 red CI gates) (#677)
## Problem README failed **two** CI doc-governance gates (both in `.github/workflows/ci.yml`): 1. **`check-soundness-ledger.sh`** (property 2, back-links) — README pointed at `SOUNDNESS-LEDGER.adoc`, a filename that **does not exist**. The gate greps for `SOUNDNESS.adoc`; the old string didn't match → RED. 2. **`check-doc-truthing.sh`** (DOC-04) — README did **not** mention the authoritative status matrix `CAPABILITY-MATRIX.adoc` anywhere → RED. Both were pre-existing reds on `main` (verified against pristine `origin/main`). ## Fix (README.adoc only) - Repoint the 3 soundness-ledger references → `docs/SOUNDNESS.adoc` - Add `docs/CAPABILITY-MATRIX.adoc` (feature readiness) in Status + Documentation - Replace the stale *"state the license and add a LICENSE file"* TODO with a real License section (`LICENSE` + `LICENSES/` already exist: MPL-2.0 code, CC-BY-SA-4.0 docs) ## Verification (real toolchain — dune 3.24.0, OCaml 4.14.1 + opam) ``` BUILD_EXIT=0 OK: doc-truthing intact — presence invariants + over-claim ratchet (DOC-04/05/08/09). (TRUTH_EXIT=0) OK: soundness ledger — all 5 properties hold. (GATE_EXIT=0) ``` ## Supersedes #675 #675 fixed only the soundness link, so it could not turn the doc-truthing gate green on its own (that gate is required, so #675 was unmergeable alone). This PR fixes both. **#675 will be closed as superseded.** Also unblocks the descriptiles migration #676 (blocked only by these same README gates). 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
1 parent 255c0b4 commit 2a3da6c

1 file changed

Lines changed: 9 additions & 4 deletions

File tree

README.adoc

Lines changed: 9 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,8 @@ 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`; per-feature
31+
readiness is tracked in `docs/CAPABILITY-MATRIX.adoc`.
3132

3233
== What you get
3334

@@ -142,7 +143,7 @@ risk here, and it is not yet solved.
142143
Soundness is *partially mechanised, and honestly tracked.* An initial,
143144
axiom-free, machine-checked result for code-generation preservation exists
144145
(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
146+
-- in `docs/SOUNDNESS.adoc`, which states for each claim whether it is
146147
mechanised or still argued in prose.
147148

148149
The ledger is the source of truth for what currently holds. This README
@@ -192,8 +193,12 @@ totality cut, and a WebAssembly target -- rather than any one ingredient.
192193
== Documentation
193194

194195
// TODO: link the design notes and the examples directory once locations are stable.
195-
* Soundness status: `SOUNDNESS-LEDGER.adoc`
196+
* Soundness status: `docs/SOUNDNESS.adoc`
197+
* Feature readiness: `docs/CAPABILITY-MATRIX.adoc`
196198

197199
== License
198200

199-
// TODO: state the license and add a LICENSE file.
201+
Code is licensed under the Mozilla Public License 2.0 (`MPL-2.0`); prose and
202+
documentation under Creative Commons Attribution-ShareAlike 4.0
203+
(`CC-BY-SA-4.0`). Full texts are in `LICENSE` and `LICENSES/`; per-file
204+
provenance is declared with SPDX headers.

0 commit comments

Comments
 (0)