Skip to content

fix(docs): README back-links + real LICENSE section (unblocks 2 red CI gates) #677

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 1 commit into from
Jul 7, 2026
+9 −4
Merged

fix(docs): README back-links + real LICENSE section (unblocks 2 red CI gates) #677

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 9 additions & 4 deletions README.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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.
Loading