docs: truth pass across human, machine, and wiki documentation + DEBT register - #159
Conversation
The repository's prose had drifted badly from a well-maintained codebase.
Corrections, all verified against the tree rather than assumed:
LICENCE SAFETY
- PALIMPSEST.adoc asserted the project is licensed PMPL-1.0, contradicting
LICENSE (MPL-2.0). The repo migrated off PMPL on 2026-05-26 per estate
audit standards#196. Rewritten as a historical note; four dead path
references dropped.
STRUCTURAL
- CONTRIBUTING.md was broken: it opened mid-code-block (line 7 rendered as
an H1), ended unterminated, carried TWO conflicting SPDX identifiers, and
described a 'Perimeter 1-3' layout that does not exist. Rewritten against
the real 15-crate workspace, with the real signing requirement (the main
ruleset enforces required_signatures — not DCO as the .adoc twin claimed)
and a proof-obligations section.
FACTUAL
- ROADMAP.adoc was a mint-time placeholder ('Initial development phase',
every box unchecked, 'to be determined by community feedback') against a
0.2.0 tree with 221 passing tests and a working LLVM pipeline. Replaced
with real rung state and an explicit 'Not planned' section.
- README.adoc contradicted README.md on test count (137 vs 221), proof phase,
dialect structure and layout → short accurate pointer.
- EXPLAINME.adoc claimed .hypatia-baseline.json is 'an intentionally empty
array' — it has 7 entries expiring 2026-10-27 (#145). Also corrected the
stale test count, the four-co-equal-dialects framing, a dead contractiles/
path, and the ReScript→AffineScript survivals.
- Wiki understated proof status on three pages ('preservation in progress');
preservation is machine-checked, axiom-free and CI-gated since F1.4.
HONESTY BANNERS
- 11 wiki pages document unimplemented behaviour (an installer and package
registry that do not exist, a retracted std:: module tree, async/await,
live AI queries). Each now carries a warning banner naming the debt item
rather than being silently deleted.
MACHINE-READABLE
- STATE.a2ml: head commit 8636e15 → e68bb3d; 'FULLY GREEN' board corrected;
the Idris ?todo_preservation note contradicted proofs/STATUS.md and the
tree (zero holes remain).
- STATE.a2ml recorded S3c.3-choice as pending while proofs.yml:319 already
gates it axiom-free — the CI was ahead of its own records.
- ECOSYSTEM.a2ml (two months stale): gaps G1/G2/G3/G5 were all closed;
'four dialects' retracted to the nested-subset model.
NEW
- DEBT.md: 34 items across licence, documentation, code, proof, test, CI/CD
and metadata — 8 high, 21 medium, 5 low. Each records the command that
produced its evidence so it can be re-measured. Unverified items are
labelled DIAGNOSIS rather than asserted.
- .gitignore: .claude/worktrees/ was untracked and doubling every scan.
Verified: 221 tests pass (0 failures); code fences balanced; SPDX on line 1.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
4c8d7d9 to
367565e
Compare
![gitar-bot[bot]](https://avatars.githubusercontent.com/in/827041?s=60&v=4){kind=small}
| ### P-3 — Proof registry is 8 weeks stale · MEDIUM | ||
| `proofs/STATUS.md` says *"Last verified: 2026-06-14"*, and it outranks every | ||
| other document by its own terms. Meanwhile `proofs.yml` already gates | ||
| S3c.3-choice, which `STATE.a2ml` still lists as `pending`. | ||
| **Next:** re-verify and re-date. The workflow is ahead of both registries. |
There was a problem hiding this comment.
💡 Quality: S3c.3-choice status inconsistent across files in this PR
This PR updates STATE.a2ml to mark S3c.3-choice as status = "done" (2026-08-07), but two other files edited in the same commit still treat it as unfinished, undermining the PR's stated truth-pass goal. DEBT.md P-3 asserts "proofs.yml already gates S3c.3-choice, which STATE.a2ml still lists as pending" — now false, since STATE.a2ml was changed to done in this very commit. ROADMAP.adoc lists S3c.3-choice under "Next / remaining n-party safety" and omits it from the "Done" section, contradicting STATE.a2ml (which ROADMAP itself declares authoritative). Reconcile: move S3c.3-choice into ROADMAP's Done list and update DEBT.md P-3 to reflect that STATE.a2ml now records it as done (the residual point being proofs/STATUS.md staleness).
Was this helpful? React with 👍 / 👎
There was a problem hiding this comment.
Configure merge blocking · Maintainers can dismiss this review.
|
Note Automatic reviews are paused because your trial's included automatic processing has been used for this period. Upgrade now, or comment "Gitar review" to run a review anytime. Code Review 👍 Approved with suggestions 0 resolved / 1 findingsComprehensive documentation truth pass aligning human, machine, and wiki records with the actual 0.2.0 tree and introducing a 34-item DEBT register. Consider resolving the minor S3c.3-choice status inconsistency between STATE and proofs files.
💡 Quality: S3c.3-choice status inconsistent across files in this PR📄 DEBT.md:240-244 📄 ROADMAP.adoc:69-77 📄 .machine_readable/6a2/STATE.a2ml:92 This PR updates STATE.a2ml to mark S3c.3-choice as 🤖 Prompt for agentsOptionsDisplay: compact → Showing less information. Comment with these commands to change the behavior for this request:
Important Your trial ends in 3 days — upgrade now to keep code review, CI analysis, auto-apply, custom automations, and more. Was this helpful? React with 👍 / 👎 | Gitar |
#162) Follow-up to #161. That PR normalised every SPDX identifier and `license` declaration, but a licence is also what the prose *tells a reader* — and five passages in subtrees still said something different: - `frontier-practices/README.adoc` — *"licensed under the Palimpsest-MPL License v3.0 (PMPL-1.0)"*, plus a badge whose alt-text read `PMPL-1.0` while the image itself said MPL-2.0 - `frontier-practices/tabletop/README.adoc` — *"Licensed under MIT + Palimpsest v0.8"* - `playground/hives/me/CONTRIBUTING.md` — told contributors their work would be licensed under **the MIT License**, which is the passage most likely to actually mislead someone - `playground/PALIMPSEST.adoc` — asserted PMPL-1.0, mirroring the root file already converted in #159; given the same historical-note treatment All now state **MPL-2.0** for code and **CC-BY-SA-4.0** for documentation. **Verified:** no `.md`/`.adoc` asserts a non-MPL/CC licence · the tree contains exactly two SPDX identifiers (426 MPL-2.0 / 206 CC-BY-SA-4.0) · `hooks/validate-spdx.sh` passes. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
1 participant
The code is in good shape; the prose describing it was not. This pass makes the documentation true, and catalogues what it can't fix in one place.
Everything below was verified against the tree, not assumed — including re-running the test suite (221 pass, 0 failures — the README's long-published number reproduces exactly).
Licence safety (highest priority)
PALIMPSEST.adocasserted "This project is licensed under the Palimpsest-MPL License 1.0", contradictingLICENSE(MPL-2.0). The repo migrated off PMPL on 2026-05-26 per estate auditstandards#196— so this was a leftover creating genuine licensing ambiguity. Rewritten as a clearly-marked historical note.Six further licence inconsistencies are catalogued but not unilaterally fixed, because they need your decision — notably
dialects/solo/compiler/Cargo.tomldeclaringlicense = "MIT OR Palimpsest-0.8"(not a valid SPDX identifier) and twoLICENSEfiles whose SPDX tag says MPL-2.0 while their body is Palimpsest text copyrighted to a different party.Structural
CONTRIBUTING.mdwas broken: it opened mid-code-block (so line 7 rendered as an H1 "# Clone the repository"), ended unterminated, carried two conflicting SPDX identifiers, and described a "Perimeter 1-3" layout that doesn't exist here. Rewritten against the real 15-crate workspace — including the actual signing requirement (themainruleset enforcesrequired_signatures; the.adoctwin claimed DCO sign-off) and a section on proof-affecting changes.Factual corrections
ROADMAP.adoc: "Initial development phase", every box unchecked, "to be determined based on community feedback"README.adoc: 137 tests, F1.0, four co-equal dialects, proof CI "future"README.md(it contradicted it on every load-bearing number)EXPLAINME.adoc: ".hypatia-baseline.json is an intentionally empty array"Honesty banners, not deletions
11 wiki pages document behaviour that doesn't exist — an installer at
mylang.org, Homebrew/apt packages, anmlbinary (it'smy), a retractedstd::module tree,async/await, live AI queries. Rather than delete ~13k lines unilaterally, each now carries a warning banner naming the specific debt item. A reader can no longer be misled; you can still decide what to keep.Machine-readable
STATE.a2ml: head commit8636e15→e68bb3d; the "FULLY GREEN" board claim corrected; the "Idris?todo_preservationdeliberately open" note contradicted bothproofs/STATUS.mdand the tree (zero holes remain).STATE.a2mllisted S3c.3-choice aspendingwhileproofs.yml:319already gates it axiom-free — the proof work was ahead of its own records.ECOSYSTEM.a2ml(two months stale): gaps G1/G2/G3/G5 all closed; "four dialects" retracted to the nested-subset model.New:
DEBT.md34 items across licence · documentation · code · proof · test · CI/CD · metadata — 8 high, 21 medium, 5 low. Each records the command that produced its evidence, so items can be re-measured rather than re-argued. Unverified items are labelled DIAGNOSIS (unconfirmed) rather than asserted.
Highlights beyond the licence issues:
src/+lib/— unbuilt, divergent, and documented by the wiki as if it were the compilerproofs.ymltriggers only onproofs/verification/**, so changing the checker never re-runs the proof gate — exactly the change most likely to break the spec↔implementation correspondencetests/property_tests.rsare wired to no target and never compileWiki + repo metadata
The GitHub wiki was a 29-byte stub while 26 pages sat unpublished. It's now five pages (Home, Getting-Started, Architecture, Formal-Verification, Project-Status) plus a sidebar — deliberately a navigational layer linking to in-repo docs so it can't drift. Live and rendering.
Description and topics replaced. The old topics (
development,hyperpolymath,open-source,rust,software,tooling) either named you or duplicated GitHub's own language detection. The new nine are concept-level and chosen for discoverability:quantitative-type-theory,affine-types,linear-types,mechanized-metatheory,session-types,verified-compiler,programming-language-design,proof-engineering,type-systems.🤖 Generated with Claude Code