docs: repo-wide documentation refresh — counts, paths, licence status, debt register - #352
Merged
Merged
Conversation
…, debt register Reconciles the documentation surface (human, machine-readable, wiki) against the tree, and publishes what could not be reconciled as measured debt rather than leaving it unstated. Prover counts (issue #251). Five different figures were in circulation — 48, 105, 128, 138, 141 — because four different things are all called 'the number of provers'. Re-measured: 141 ProverKind variants, 105 backend implementation files, 102 with suggest_tactics, 12 default- exposed core. docs/PROVER_COUNT.md is now canonical, explains the denominators, and ships the command that reproduces each figure; all five commands were run and reproduce exactly. Present-tense claims elsewhere now cite it. Dated historical records (release notes, completed-milestone entries) were deliberately left at their authoring-time numbers — they are records, not claims about today. Wiki. docs/wiki/ is the source and had drifted ahead of the live wiki, which had never been synced. Corrected and pushed: the Tier-1 core list named six backends that are not in ProverKind::all_core() (Idris 2, F*, Alt-Ergo, Dafny, Vampire, E Prover — actually Metamath, HOL Light, Mizar, PVS, ACL2, HOL4); the licence was stated as MPL-2.0. The note claiming the wiki is not pushable from automation was wrong and is replaced with a working sync recipe. Stale paths (issue #242). .machine_readable/6a2/ no longer exists; its six descriptiles moved to descriptiles/. Repaired 17 documents. The contractile .ncl write-destinations still naming 6a2/ were left alone deliberately — 6a2 is a concept name there, and repointing an evidence sink is a semantic decision. Recorded as D7. Broken links: 19 -> 13. The 13 remaining are dated release notes and the playground sub-project, both recorded as D4/D5 rather than silently rewritten. Root scaffold. ARCHITECTURE.md and GOVERNANCE.md contained generic template text with zero project-specific words, while the real documents sat at docs/ARCHITECTURE.md and GOVERNANCE.adoc. Since GitHub surfaces the .md member, the document most readers landed on described no particular project. Both are now explicit pointers. OpenSSF badge removed: it was a hardcoded green shields.io label linking to the project registration form, so it would have read 'passed' whatever the real standing — including now, unregistered. Restore the genuine dynamic badge once registered. docs/DEBT.md (new) carries the rest, every item with the command that measures it. P0 is licensing: the repository states four different licences, and 590 source files carry MPL-2.0 headers while LICENSE and Cargo.toml declare AGPL-3.0-or-later. Because per-file headers are themselves a grant, that is live exposure, not an inconsistency of record. NOT ACTED ON — re-licensing is an owner decision; the entry sets out a sequence and stops. README and the wiki now warn readers not to rely on any surface but LICENSE until it is resolved. Verified: R5a bare-count rule clean across all scoped top-level docs; every PROVER_COUNT command reproduces its stated figure; DEBT.md's own measurements re-run and corrected (588 -> 590) before commit. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
![gitar-bot[bot]](https://avatars.githubusercontent.com/in/827041?s=60&v=4){kind=small}
| | Surface | States | | ||
| |---|---| | ||
| | `LICENSE`, `Cargo.toml`, README badge | AGPL-3.0-or-later | | ||
| | Per-file `SPDX-License-Identifier` headers (588 source files) | MPL-2.0 | |
There was a problem hiding this comment.
💡 Quality: FAQ.md states 588 SPDX files; canonical DEBT.md says 590
docs/wiki/FAQ.md's licence table reads "Per-file SPDX-License-Identifier headers (588 source files)", but the canonical figure re-measured in this same PR is 590 (584 plain MPL-2.0 + 6 dual with Palimpsest-0.6), and the PR description explicitly notes the 588→590 correction. I reproduced 590 from the tree. Since FAQ.md is a synced live-wiki page presenting licensing debt, leaving the stale 588 recreates exactly the cross-surface count drift this PR sets out to eliminate. Update it to 590 to match docs/DEBT.md.
Align FAQ.md with the canonical 590 figure (584 plain + 6 dual) from DEBT.md.:
| Per-file `SPDX-License-Identifier` headers (590 source files) | MPL-2.0 |
Was this helpful? React with 👍 / 👎
|
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 refresh correcting prover counts, wiki drift, stale paths, and introducing a measured technical debt register. Update FAQ.md to match the canonical 590 SPDX files reported in DEBT.md.
💡 Quality: FAQ.md states 588 SPDX files; canonical DEBT.md says 590📄 docs/wiki/FAQ.md:60 📄 docs/DEBT.md:36 📄 docs/DEBT.md:44-46 docs/wiki/FAQ.md's licence table reads "Per-file SPDX-License-Identifier headers (588 source files)", but the canonical figure re-measured in this same PR is 590 (584 plain MPL-2.0 + 6 dual with Palimpsest-0.6), and the PR description explicitly notes the 588→590 correction. I reproduced 590 from the tree. Since FAQ.md is a synced live-wiki page presenting licensing debt, leaving the stale 588 recreates exactly the cross-surface count drift this PR sets out to eliminate. Update it to 590 to match docs/DEBT.md. Align FAQ.md with the canonical 590 figure (584 plain + 6 dual) from DEBT.md.🤖 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 |
There was a problem hiding this comment.
Configure merge blocking · Maintainers can dismiss this review.
…ailures Both observed while verifying this PR's own CI. Recorded with what was actually confirmed and no more: the K9 error text is quoted verbatim; the Rust CI failure is identified as a genuine post-build test failure (exit 101 under llvm-cov) rather than the lockfile-pin startup failure that masked it until the dtolnay/rust-toolchain relock, but the individual failing tests are not enumerated and the entry says so. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
Aug 7, 2026
) Every Rust-touching workflow currently fails at startup, on `main` and on every PR: ``` Lockfile pin 4cda84d5c5c54efe2404f9d843567869ab1699d4 for `dtolnay/rust-toolchain` does not match ref `stable` ``` `stable` is a **moving ref** — dtolnay re-points it at each Rust release — so a lockfile pin against it goes stale on upstream's schedule, not ours. Upstream now resolves to `4360b525…`. **Affected while stale:** Cargo Audit, MVP Smoke, Server Boot Gate, Live Provers, Rust CI, S4 Loop, Chapel CI, Formal Verification — all fail *before running a step*. ### Worth knowing for the estate sweep `gh actions-lock --relock` **alone does not fix this.** A plain `--relock` leaves pins whose recorded commit is no longer reachable upstream as errors; **`--accept-moved` is required** to re-resolve them. Two tool side-effects were reverted rather than committed: - it re-inserted its `managed by gh actions-lock` marker at **line 1** of all 31 workflows — duplicating the marker already at line 2 and displacing the SPDX identifier, which the Workflow Security Linter requires on line 1 (it greps `head -1`). Deduped and restored. - it added a lockfile entry for `main-estate-audit.yml`, an untracked scratch file that is not part of the repository. Removed. The result is a **one-line diff**. ### Recurrence This will happen again every time upstream moves `stable`. The durable fix is either pinning a released tag instead of a moving ref, or scheduling a periodic relock. Not done here — this PR restores CI and nothing more. Split out of #352 (documentation refresh) deliberately: that PR changes no CI behaviour, and this one changes nothing but. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
Aug 7, 2026
…t split (#354) Applies your ruling — **AGPL for echidna** — and implements the two boundary decisions: the playground stays MPL-2.0, and the documentation surface normalises to CC-BY-SA-4.0. **Stacked on #352** (base is `docs/full-documentation-refresh`, not `main`) because it retires that PR's P0 debt entry and rewrites the licence warnings it added. Merge #352 first; this then targets `main` automatically. ## Answer to the compatibility question **Yes — and in exactly the direction needed.** MPL-2.0 §3.3 designates the GNU licences, *including AGPL-3.0+*, as "Secondary Licenses": MPL files can be combined into an AGPL work and the combined work distributed under AGPL, while those files individually remain available under MPL. I verified no file carries the Exhibit B `Incompatible With Secondary Licenses` notice that would break this — the only match in the tree is inside `LICENSES/MPL-2.0.txt`, which is the licence's own boilerplate. ## What I found looking for the components you expected You anticipated borrowed code from gossamer, snifs and similar. In this repo there is essentially none: | Check | Result | |---|---| | `crates/` shared with other estate repos | none — all five are echidna-only | | gossamer / snifs code | absent; the gossamer mention is a *pattern* reference ("same ABI/FFI pattern that runs in `proven`, `burble`, `gossamer`") | | vendor / third_party dirs | none | | Institutional or corporate copyrights | none | | Copyright holders asserted | all you / ECHIDNA — **except 7 files** | The only externally-attributed code is **`echidna-playground/src/*.res`** ("Coq-Jr Contributors"). So the MPL headers everywhere else were historical residue from the MIT/Palimpsest → MPL migration, not a marker of borrowed code — which is what makes relicensing them straightforward: you hold the copyright. ## The split | Part | Licence | Files | |---|---|---| | Code — `src/`, `crates/`, `ffi/`, `proofs/`, `spark/`, `verification/`, build system, CI, machine-readable metadata | **AGPL-3.0-or-later** | 594 + 6 dual | | Documentation — `docs/`, top-level `.md`/`.adoc` | **CC-BY-SA-4.0** | 92 + 1 dual | | `echidna-playground/` | **MPL-2.0**, untouched | 35 | ## Method — why this isn't the sweep that went wrong before Identifiers were **replaced in place on `SPDX-License-Identifier:` lines only, never inserted**. A previous estate sweep mis-licensed files by imposing a header where a different one already sat further down the file. Consequences: - prose mentioning MPL is untouched - the **7 files granting `Palimpsest-0.6` keep that grant** (`AGPL-3.0-or-later OR/AND Palimpsest-0.6`) — dropping half of a dual withdraws a permission you granted, which isn't a documentation decision - 3 workflows carrying `PMPL-1.0-or-later` folded into AGPL - **SPDX stays on line 1 of all 30 workflows** (the linter greps `head -1`) Excluded deliberately: `LICENSES/` and `docs/legal/` — restating the licensing *of a licence text* is confusing. ## Supporting files - **`NOTICE`** rewritten. It previously said "licensed under the Mozilla Public License" while citing `LICENSE` — which is AGPL — as its full text. Now states the split, the §3.3 argument, and the licence history. - **`.reuse/dep5`** rewritten; it claimed `PMPL-1.0 AND Palimpsest-0.6` for everything. - **`LICENSE`**: dropped two prepended SPDX lines, making it byte-identical to `LICENSES/AGPL-3.0-or-later.txt`. That prepend is why GitHub reported the licence as **"Other"**; expect it to detect AGPL-3.0 after merge. ## Verification (all re-run before commit) | Check | Result | |---|---| | MPL outside playground / LICENSES / docs-legal | **0** | | Code identifiers | AGPL-3.0-or-later (+ preserved Palimpsest duals) | | Playground still MPL-2.0 | **35 files** | | SPDX on line 1 of every workflow | **clean** | ## One thing left for you **`Palimpsest-0.6` has no licence text** — not in this repo, not in `standards/LICENSES/`. Seven files grant it, so REUSE cannot resolve the identifier. I kept the grants and recorded it as the residual P0 entry. Either supply `LICENSES/Palimpsest-0.6.txt`, or decide the grant is retired and remove it deliberately. (Note `PMPL-1.0-or-later` *does* have a text — different identifier.) 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Reconciles the documentation surface — human, machine-readable, and the wiki — against what the tree actually contains, and publishes what could not be reconciled as measured debt rather than leaving it unstated.
Prover counts (#251)
Five figures were in circulation — 48, 105, 128, 138, 141 — because four different things are all called "the number of provers". Re-measured:
ProverKindvariantssuggest_tacticsall_core())docs/PROVER_COUNT.mdis now canonical, explains the denominators, and ships the command that reproduces each figure — all five were run and reproduce exactly. Present-tense claims elsewhere cite it. Dated historical records (release notes, completed milestones) keep their authoring-time numbers: they are records, not claims about today.Wiki — corrected and synced
docs/wiki/is the source and had drifted ahead of the live wiki, which had never been synced. Two substantive errors fixed:The in-repo note claiming the wiki isn't pushable from automation was wrong; it's replaced with a working sync recipe (note: the wiki's default branch is
master).Licence — P0, identified and deliberately NOT acted on
The repository states four different licences:
LICENSE,Cargo.toml, README badgeNOTICELICENSE(which is AGPL) for its text.reuse/dep5PMPL-1.0 AND Palimpsest-0.6GitHub reports the licence as "Other" — likely the SPDX line prepended above the GNU text in
LICENSE, which stops its detector matching.This matters beyond tidiness: MPL is file-level weak copyleft with no network clause; AGPL reaches users served over a network. An integrator reading the headers would conclude they may host a modified ECHIDNA without publishing changes. Because per-file headers are themselves a licence grant, that is live exposure.
I have not changed any licence. Re-licensing is an owner decision affecting existing recipients and contributors.
docs/DEBT.mdsets out a suggested sequence and stops. Meanwhile the README and wiki now tell readers not to rely on any surface butLICENSE.Also in this PR
.machine_readable/6a2/no longer exists (descriptiles moved todescriptiles/) — 17 documents repaired. The contractile.nclwrite destinations naming6a2/were left alone deliberately:6a2is a concept name there, and repointing an evidence sink is a semantic decision (recorded as D7).ARCHITECTURE.mdandGOVERNANCE.mdcontained generic template text with zero project-specific words while the real documents sat elsewhere. GitHub surfaces the.md, so the page most readers landed on described no particular project. Both are now explicit pointers.VersisimDB) and the stale 48; topics dropped languages GitHub already surfaces (agda/coq/julia), a duplicate (theorem-prover vs theorem-proving) and a generic (artificial-intelligence), replaced with capability terms —proof-assistants,proof-search,premise-selection,proof-certificates,smt-solvers.New:
docs/DEBT.mdLive debt register — P0 licensing, seven documentation items, four code items. Every entry carries the command that measures it, so entries can be retired on evidence rather than on feeling. Supersedes
tech-debt-2026-05-26.md, which is kept and banner-marked as a dated snapshot.Verification
PROVER_COUNT.mdcommands run and reproduce their stated figures.DEBT.md's own measurements re-run before commit; one corrected (588 → 590).Known unrelated red:
Governancefails onmainfor a hypatia scanner error (#314), not doc drift.🤖 Generated with Claude Code