From a82d3093430d3cb411975747b787bdd9ebc64b6f Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 7 Jul 2026 00:50:55 +0100 Subject: [PATCH] fix(docs): README back-links + real LICENSE section (unblocks 2 red CI gates) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit README failed two CI doc-governance gates in .github/workflows/ci.yml: 1. tools/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 did not match -> RED. 2. tools/check-doc-truthing.sh (DOC-04): README did not mention the authoritative status matrix `CAPABILITY-MATRIX.adoc` anywhere -> RED. Fixes, all in README.adoc: - repoint the 3 soundness-ledger references to `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) Supersedes #675 (which fixed only the soundness link). Verified (dune 3.24.0, system OCaml 4.14.1 + opam switch as-verify): BUILD_EXIT=0 OK: doc-truthing intact (TRUTH_EXIT=0) OK: soundness ledger — all 5 properties hold (GATE_EXIT=0) Co-Authored-By: Claude Opus 4.8 (1M context) --- README.adoc | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/README.adoc b/README.adoc index e2177c5..9b1c10a 100644 --- a/README.adoc +++ b/README.adoc @@ -27,7 +27,8 @@ 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`; per-feature +readiness is tracked in `docs/CAPABILITY-MATRIX.adoc`. == What you get @@ -142,7 +143,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,8 +193,12 @@ 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` +* Feature readiness: `docs/CAPABILITY-MATRIX.adoc` == License -// TODO: state the license and add a LICENSE file. +Code is licensed under the Mozilla Public License 2.0 (`MPL-2.0`); prose and +documentation under Creative Commons Attribution-ShareAlike 4.0 +(`CC-BY-SA-4.0`). Full texts are in `LICENSE` and `LICENSES/`; per-file +provenance is declared with SPDX headers.