From 5b7aff404d02b3a1cd890f68b132bbabbbc2bc13 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 20 Jun 2026 04:57:54 +0000 Subject: [PATCH 1/2] chore(rsr): standards compliance + adoc-first root cleanup MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Aligns arghda-core to the hyperpolymath standards / RSR baseline and tidies the root. Docs/scaffolding only — no source changes, CI gate unaffected. - README.md -> README.adoc (adoc-first; README is not one of the four GitHub-required .md community-health files). Refreshed to the feature-complete v0.1 status (all seven lints, config, dag headlines). No duplicate doc formats. - New EXPLAINME.adoc (orientation pointer: humans -> README.adoc, status -> STATE.a2ml, agents -> 0-AI-MANIFEST.a2ml), mirroring the estate convention. - New LICENSE (full MPL-2.0 text, copied from standards). - New CODE_OF_CONDUCT.md (Contributor Covenant 2.1). - Licence headers per estate policy (LICENCE-POLICY.adoc Rule 1): new prose docs carry CC-BY-SA-4.0; code/config/state stay MPL-2.0. - Refreshed machine-readable artefacts: STATE.a2ml (v0.1 feature-complete, 85%, accurate milestones + maintenance pass), META.a2ml (ADR-005..007 for the unused-import shell-out, config precedence, dag-headlines decisions), 0-AI-MANIFEST.a2ml read-order (README.md -> README.adoc, EXPLAINME first). - Removed local dist-newstyle/ build cruft (agda-unused build output; already gitignored). Deliberately NOT done (owner-manual only, per LICENCE-POLICY.adoc A2 — an agent must never bulk-sweep SPDX): per-file MPL-2.0 SPDX headers on src/*.rs. Flagged in STATE.a2ml as the one remaining compliance gap. Also deliberately did NOT scaffold the maximalist rsr-template tree (build/just, verification/ proofs, container/, hundreds of placeholder dirs) — that would be the vestigial cruft this cleanup removes. `just validate-rsr` passes; `cargo build` + `cargo fmt --check` green. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_019GiSiEfgZCte35dyykgBHs --- .machine_readable/6a2/META.a2ml | 5 +- .machine_readable/6a2/STATE.a2ml | 39 ++-- 0-AI-MANIFEST.a2ml | 5 +- CHANGELOG.md | 12 + CODE_OF_CONDUCT.md | 7 + EXPLAINME.adoc | 21 ++ LICENSE | 375 +++++++++++++++++++++++++++++++ README.adoc | 141 ++++++++++++ README.md | 108 --------- 9 files changed, 587 insertions(+), 126 deletions(-) create mode 100644 CODE_OF_CONDUCT.md create mode 100644 EXPLAINME.adoc create mode 100644 LICENSE create mode 100644 README.adoc delete mode 100644 README.md diff --git a/.machine_readable/6a2/META.a2ml b/.machine_readable/6a2/META.a2ml index 347bb70..29bf9c3 100644 --- a/.machine_readable/6a2/META.a2ml +++ b/.machine_readable/6a2/META.a2ml @@ -6,7 +6,7 @@ [metadata] version = "0.1.0" -last-updated = "2026-06-18" +last-updated = "2026-06-20" [project-info] type = "library" # library | binary | monorepo | service | website @@ -20,6 +20,9 @@ author = "Jonathan D.A. Jewell (hyperpolymath)" # - { id = "ADR-002", title = "Triage transitions are file moves; ground truth is the filesystem", status = "accepted", date = "2026-05-30" } # - { id = "ADR-003", title = "Dependency-free RFC 3339 timestamps (hermetic build, no chrono)", status = "accepted", date = "2026-06-18" } # - { id = "ADR-004", title = "Orphan reachability is the union of discovered CI roots (All.agda/Smoke.agda)", status = "accepted", date = "2026-06-18" } +# - { id = "ADR-005", title = "unused-import is an agda.rs-style external shell-out (per-file, local mode, LC_ALL=C.UTF-8), not a per-file LintRule", status = "accepted", date = "2026-06-20" } +# - { id = "ADR-006", title = "Headline pattern is operator-configurable; precedence default < .arghda/config.toml < CLI flag (on the rule instance, not LintContext)", status = "accepted", date = "2026-06-20" } +# - { id = "ADR-007", title = "DAG node `headlines` reuses the unpinned-headline extractor with the configured pattern", status = "accepted", date = "2026-06-20" } [development-practices] build-tool = "just" diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 9a97dbe..93ad619 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -6,13 +6,13 @@ [metadata] project = "arghda-core" version = "0.1.0" -last-updated = "2026-06-18" +last-updated = "2026-06-20" status = "active" # active | paused | archived [project-context] name = "arghda-core" purpose = "Lightweight proof-workspace manager for Agda — the language-agnostic engine half of arghda. A four-state triage workspace (inbox/working/proven/rejected) as file moves, a lint pack targeting the silent-failure class, a first-class import-graph DAG, and a JSON + event-stream contract a visual layer (arghda-studio) consumes. It never proves anything; Agda does." -completion-percentage = 55 +completion-percentage = 85 [position] phase = "implementation" # design | implementation | testing | maintenance | archived @@ -21,37 +21,46 @@ maturity = "alpha" # experimental | alpha | beta | production | lts [route-to-mvp] milestones = [ { name = "Workspace scaffold + filesystem watcher", completion = 100 }, - { name = "Lint pack (missing-safe-pragma, orphan-module, unjustified-postulate, escape-hatch, tab-mix)", completion = 100 }, - { name = "First-class import graph + `dag` JSON command", completion = 100 }, + { name = "Hard-block lint pack (missing-safe-pragma, orphan-module, unjustified-postulate)", completion = 100 }, + { name = "Warn lint pack (escape-hatch, tab-mix, unpinned-headline, unused-import)", completion = 100 }, + { name = "First-class import graph + `dag` JSON command (nodes incl. headlines, edges, blocked)", completion = 100 }, { name = "State machine (claim/promote/reject/requeue/invalidate) + events.jsonl", completion = 100 }, { name = "`check` command (Agda typecheck + lint verdict)", completion = 100 }, { name = "Multi-root reachability (union of discovered CI roots)", completion = 100 }, - { name = "Content-hash invalidation of proven (file-level; +imports deferred)", completion = 75 }, - { name = "Remaining lint rules (unpinned-headline, unused-import)", completion = 0 }, - { name = "Groove service manifest (/.well-known/groove)", completion = 0 }, - { name = "RSR retrofit (.machine_readable, Justfile, .well-known)", completion = 60 }, + { name = "Content-hash invalidation of proven (file-level; transitive imports deferred)", completion = 75 }, + { name = "Operator config (.arghda/config.toml + --headline-pattern + --config)", completion = 100 }, + { name = "RSR / standards alignment (.machine_readable, README.adoc, EXPLAINME, LICENSE, .well-known)", completion = 100 }, + { name = "Groove service manifest (/.well-known/groove) for PanLL discovery", completion = 0 }, ] [blockers-and-issues] -# No active blockers. `unpinned-headline` needs Smoke.agda parsing + a -# configurable headline regex; `unused-import` shells out to `agda-unused`. +# No active blockers. v0.1 lint set + DAG schema (arghda-spec.adoc) are complete. +# Known compliance gap (owner-manual only, per LICENCE-POLICY A2 — never an +# agent sweep): src/*.rs lack per-file `// SPDX-License-Identifier: MPL-2.0` +# headers. The repo is declared MPL-2.0 (Cargo.toml, LICENSE); applying the +# per-file headers is owner-driven manual work. [critical-next-actions] actions = [ - "Add unpinned-headline (needs config + headline regex) + unused-import (agda-unused) lint rules", - "Extend content-hash to cover transitive imports (needs include-root tracking)", - "Serve /.well-known/groove for PanLL discovery", + "Owner-manual: apply MPL-2.0 SPDX headers to src/*.rs (no agent bulk sweep — LICENCE-POLICY A2)", + "Extend content-hash invalidation to cover transitive imports (needs include-root tracking)", + "Serve /.well-known/groove for PanLL discovery (Groove protocol)", "Scaffold arghda-studio (AffineScript visual layer consuming the dag JSON)", ] [maintenance-status] -last-run-utc = "never" -last-result = "unknown" # unknown | pass | warn | fail +last-run-utc = "2026-06-20" +last-result = "pass" # unknown | pass | warn | fail open-warnings = 0 open-failures = 0 +# `just check` (fmt-check + clippy -D warnings + build + test) green; ~50 lib +# tests + integration suites pass. Dogfooded against echo-types + a live +# agda-unused build. [ecosystem] part-of = ["arghda"] depends-on = [] +# Build deps: anyhow, clap, notify, regex, serde, serde_json, toml, walkdir. +# Optional external tools: agda, agda-unused (both degrade gracefully). # Downstream consumers: arghda-studio (planned), arghda-panll (planned). # Dogfood workspaces: echo-types, absolute-zero. diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml index e4fa9bf..6e6e2f3 100644 --- a/0-AI-MANIFEST.a2ml +++ b/0-AI-MANIFEST.a2ml @@ -5,7 +5,7 @@ [metadata] version = "0.1.0" -last-updated = "2026-06-18" +last-updated = "2026-06-20" [project] name = "arghda-core" @@ -13,9 +13,10 @@ purpose = "Language-agnostic proof-workspace engine for the arghda visual proof- [entry] read-order = [ + "EXPLAINME.adoc", ".machine_readable/6a2/STATE.a2ml", ".machine_readable/6a2/META.a2ml", - "README.md", + "README.adoc", "docs/arghda-spec.adoc", "docs/arghda-vision.adoc", ] diff --git a/CHANGELOG.md b/CHANGELOG.md index 839a1e9..371ad8e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,6 +7,18 @@ All notable changes to arghda-core are documented here. The format follows ## [Unreleased] +### Changed + +- Standards / RSR alignment and root cleanup: `README.md` → `README.adoc` + (adoc-first; refreshed to the feature-complete v0.1 status), no duplicate + doc formats. Added `EXPLAINME.adoc` (orientation pointer), `LICENSE` (full + MPL-2.0 text), and `CODE_OF_CONDUCT.md` (Contributor Covenant 2.1). Prose + docs carry `CC-BY-SA-4.0`; code/config/state stay `MPL-2.0` (per the estate + licence policy). Refreshed `.machine_readable/6a2/STATE.a2ml` + `META.a2ml` + and the `0-AI-MANIFEST.a2ml` read-order; removed local `dist-newstyle/` + build cruft. (Per-file SPDX headers on `src/*.rs` remain owner-manual by + policy — never an agent bulk sweep.) + ### Added - `dag` command emitting the dependency-DAG JSON contract (nodes with diff --git a/CODE_OF_CONDUCT.md b/CODE_OF_CONDUCT.md new file mode 100644 index 0000000..999b538 --- /dev/null +++ b/CODE_OF_CONDUCT.md @@ -0,0 +1,7 @@ + + +# Code of Conduct + +This project follows the [Contributor Covenant 2.1](https://www.contributor-covenant.org/version/2/1/code_of_conduct/). + +Reports go to `j.d.a.jewell@open.ac.uk`. Reports are confidential by default. diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc new file mode 100644 index 0000000..4585808 --- /dev/null +++ b/EXPLAINME.adoc @@ -0,0 +1,21 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += arghda-core: explain me + +This file is a pointer, not a second README — it routes you to the one source +of truth for each concern. + +* *Humans* start at link:README.adoc[`README.adoc`]: what arghda-core is, the + lint rules, the command surface, build and usage. +* *Live status of record* is + link:.machine_readable/6a2/STATE.a2ml[`.machine_readable/6a2/STATE.a2ml`] — + phase, milestones, next actions. The README does not duplicate it. +* *AI agents* start at link:0-AI-MANIFEST.a2ml[`0-AI-MANIFEST.a2ml`], then read + the six A2ML files under + link:.machine_readable/6a2/[`.machine_readable/6a2/`] (`STATE`, `META`, + `ECOSYSTEM`, `AGENTIC`, `NEUROSYM`, `PLAYBOOK`). +* *Design* lives in link:docs/arghda-spec.adoc[`docs/arghda-spec.adoc`] (the v0 + contract) and link:docs/arghda-vision.adoc[`docs/arghda-vision.adoc`] (the + wider arghda picture). + +Human prose in `README.adoc`; machine state in `.machine_readable/6a2/`. No +duplicated status snapshots. diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..2a8b960 --- /dev/null +++ b/LICENSE @@ -0,0 +1,375 @@ +SPDX-License-Identifier: MPL-2.0 + +Mozilla Public License Version 2.0 +================================== + +1. Definitions +-------------- + +1.1. "Contributor" + means each individual or legal entity that creates, contributes to + the creation of, or owns Covered Software. + +1.2. "Contributor Version" + means the combination of the Contributions of others (if any) used + by a Contributor and that particular Contributor's Contribution. + +1.3. "Contribution" + means Covered Software of a particular Contributor. + +1.4. "Covered Software" + means Source Code Form to which the initial Contributor has attached + the notice in Exhibit A, the Executable Form of such Source Code + Form, and Modifications of such Source Code Form, in each case + including portions thereof. + +1.5. "Incompatible With Secondary Licenses" + means + + (a) that the initial Contributor has attached the notice described + in Exhibit B to the Covered Software; or + + (b) that the Covered Software was made available under the terms of + version 1.1 or earlier of the License, but not also under the + terms of a Secondary License. + +1.6. "Executable Form" + means any form of the work other than Source Code Form. + +1.7. "Larger Work" + means a work that combines Covered Software with other material, in + a separate file or files, that is not Covered Software. + +1.8. "License" + means this document. + +1.9. "Licensable" + means having the right to grant, to the maximum extent possible, + whether at the time of the initial grant or subsequently, any and + all of the rights conveyed by this License. + +1.10. "Modifications" + means any of the following: + + (a) any file in Source Code Form that results from an addition to, + deletion from, or modification of the contents of Covered + Software; or + + (b) any new file in Source Code Form that contains any Covered + Software. + +1.11. "Patent Claims" of a Contributor + means any patent claim(s), including without limitation, method, + process, and apparatus claims, in any patent Licensable by such + Contributor that would be infringed, but for the grant of the + License, by the making, using, selling, offering for sale, having + made, import, or transfer of either its Contributions or its + Contributor Version. + +1.12. "Secondary License" + means either the GNU General Public License, Version 2.0, the GNU + Lesser General Public License, Version 2.1, the GNU Affero General + Public License, Version 3.0, or any later versions of those + licenses. + +1.13. "Source Code Form" + means the form of the work preferred for making modifications. + +1.14. "You" (or "Your") + means an individual or a legal entity exercising rights under this + License. For legal entities, "You" includes any entity that + controls, is controlled by, or is under common control with You. For + purposes of this definition, "control" means (a) the power, direct + or indirect, to cause the direction or management of such entity, + whether by contract or otherwise, or (b) ownership of more than + fifty percent (50%) of the outstanding shares or beneficial + ownership of such entity. + +2. License Grants and Conditions +-------------------------------- + +2.1. Grants + +Each Contributor hereby grants You a world-wide, royalty-free, +non-exclusive license: + +(a) under intellectual property rights (other than patent or trademark) + Licensable by such Contributor to use, reproduce, make available, + modify, display, perform, distribute, and otherwise exploit its + Contributions, either on an unmodified basis, with Modifications, or + as part of a Larger Work; and + +(b) under Patent Claims of such Contributor to make, use, sell, offer + for sale, have made, import, and otherwise transfer either its + Contributions or its Contributor Version. + +2.2. Effective Date + +The licenses granted in Section 2.1 with respect to any Contribution +become effective for each Contribution on the date the Contributor first +distributes such Contribution. + +2.3. Limitations on Grant Scope + +The licenses granted in this Section 2 are the only rights granted under +this License. No additional rights or licenses will be implied from the +distribution or licensing of Covered Software under this License. +Notwithstanding Section 2.1(b) above, no patent license is granted by a +Contributor: + +(a) for any code that a Contributor has removed from Covered Software; + or + +(b) for infringements caused by: (i) Your and any other third party's + modifications of Covered Software, or (ii) the combination of its + Contributions with other software (except as part of its Contributor + Version); or + +(c) under Patent Claims infringed by Covered Software in the absence of + its Contributions. + +This License does not grant any rights in the trademarks, service marks, +or logos of any Contributor (except as may be necessary to comply with +the notice requirements in Section 3.4). + +2.4. Subsequent Licenses + +No Contributor makes additional grants as a result of Your choice to +distribute the Covered Software under a subsequent version of this +License (see Section 10.2) or under the terms of a Secondary License (if +permitted under the terms of Section 3.3). + +2.5. Representation + +Each Contributor represents that the Contributor believes its +Contributions are its original creation(s) or it has sufficient rights +to grant the rights to its Contributions conveyed by this License. + +2.6. Fair Use + +This License is not intended to limit any rights You have under +applicable copyright doctrines of fair use, fair dealing, or other +equivalents. + +2.7. Conditions + +Sections 3.1, 3.2, 3.3, and 3.4 are conditions of the licenses granted +in Section 2.1. + +3. Responsibilities +------------------- + +3.1. Distribution of Source Form + +All distribution of Covered Software in Source Code Form, including any +Modifications that You create or to which You contribute, must be under +the terms of this License. You must inform recipients that the Source +Code Form of the Covered Software is governed by the terms of this +License, and how they can obtain a copy of this License. You may not +attempt to alter or restrict the recipients' rights in the Source Code +Form. + +3.2. Distribution of Executable Form + +If You distribute Covered Software in Executable Form then: + +(a) such Covered Software must also be made available in Source Code + Form, as described in Section 3.1, and You must inform recipients of + the Executable Form how they can obtain a copy of such Source Code + Form by reasonable means in a timely manner, at a charge no more + than the cost of distribution to the recipient; and + +(b) You may distribute such Executable Form under the terms of this + License, or sublicense it under different terms, provided that the + license for the Executable Form does not attempt to limit or alter + the recipients' rights in the Source Code Form under this License. + +3.3. Distribution of a Larger Work + +You may create and distribute a Larger Work under terms of Your choice, +provided that You also comply with the requirements of this License for +the Covered Software. If the Larger Work is a combination of Covered +Software with a work governed by one or more Secondary Licenses, and the +Covered Software is not Incompatible With Secondary Licenses, this +License permits You to additionally distribute such Covered Software +under the terms of such Secondary License(s), so that the recipient of +the Larger Work may, at their option, further distribute the Covered +Software under the terms of either this License or such Secondary +License(s). + +3.4. Notices + +You may not remove or alter the substance of any license notices +(including copyright notices, patent notices, disclaimers of warranty, +or limitations of liability) contained within the Source Code Form of +the Covered Software, except that You may alter any license notices to +the extent required to remedy known factual inaccuracies. + +3.5. Application of Additional Terms + +You may choose to offer, and to charge a fee for, warranty, support, +indemnity or liability obligations to one or more recipients of Covered +Software. However, You may do so only on Your own behalf, and not on +behalf of any Contributor. You must make it absolutely clear that any +such warranty, support, indemnity, or liability obligation is offered by +You alone, and You hereby agree to indemnify every Contributor for any +liability incurred by such Contributor as a result of warranty, support, +indemnity or liability terms You offer. You may include additional +disclaimers of warranty and limitations of liability specific to any +jurisdiction. + +4. Inability to Comply Due to Statute or Regulation +--------------------------------------------------- + +If it is impossible for You to comply with any of the terms of this +License with respect to some or all of the Covered Software due to +statute, judicial order, or regulation then You must: (a) comply with +the terms of this License to the maximum extent possible; and (b) +describe the limitations and the code they affect. Such description must +be placed in a text file included with all distributions of the Covered +Software under this License. Except to the extent prohibited by statute +or regulation, such description must be sufficiently detailed for a +recipient of ordinary skill to be able to understand it. + +5. Termination +-------------- + +5.1. The rights granted under this License will terminate automatically +if You fail to comply with any of its terms. However, if You become +compliant, then the rights granted under this License from a particular +Contributor are reinstated (a) provisionally, unless and until such +Contributor explicitly and finally terminates Your grants, and (b) on an +ongoing basis, if such Contributor fails to notify You of the +non-compliance by some reasonable means prior to 60 days after You have +come back into compliance. Moreover, Your grants from a particular +Contributor are reinstated on an ongoing basis if such Contributor +notifies You of the non-compliance by some reasonable means, this is the +first time You have received notice of non-compliance with this License +from such Contributor, and You become compliant prior to 30 days after +Your receipt of the notice. + +5.2. If You initiate litigation against any entity by asserting a patent +infringement claim (excluding declaratory judgment actions, +counter-claims, and cross-claims) alleging that a Contributor Version +directly or indirectly infringes any patent, then the rights granted to +You by any and all Contributors for the Covered Software under Section +2.1 of this License shall terminate. + +5.3. In the event of termination under Sections 5.1 or 5.2 above, all +end user license agreements (excluding distributors and resellers) which +have been validly granted by You or Your distributors under this License +prior to termination shall survive termination. + +************************************************************************ +* * +* 6. Disclaimer of Warranty * +* ------------------------- * +* * +* Covered Software is provided under this License on an "as is" * +* basis, without warranty of any kind, either expressed, implied, or * +* statutory, including, without limitation, warranties that the * +* Covered Software is free of defects, merchantable, fit for a * +* particular purpose or non-infringing. The entire risk as to the * +* quality and performance of the Covered Software is with You. * +* Should any Covered Software prove defective in any respect, You * +* (not any Contributor) assume the cost of any necessary servicing, * +* repair, or correction. This disclaimer of warranty constitutes an * +* essential part of this License. No use of any Covered Software is * +* authorized under this License except under this disclaimer. * +* * +************************************************************************ + +************************************************************************ +* * +* 7. Limitation of Liability * +* -------------------------- * +* * +* Under no circumstances and under no legal theory, whether tort * +* (including negligence), contract, or otherwise, shall any * +* Contributor, or anyone who distributes Covered Software as * +* permitted above, be liable to You for any direct, indirect, * +* special, incidental, or consequential damages of any character * +* including, without limitation, damages for lost profits, loss of * +* goodwill, work stoppage, computer failure or malfunction, or any * +* and all other commercial damages or losses, even if such party * +* shall have been informed of the possibility of such damages. This * +* limitation of liability shall not apply to liability for death or * +* personal injury resulting from such party's negligence to the * +* extent applicable law prohibits such limitation. Some * +* jurisdictions do not allow the exclusion or limitation of * +* incidental or consequential damages, so this exclusion and * +* limitation may not apply to You. * +* * +************************************************************************ + +8. Litigation +------------- + +Any litigation relating to this License may be brought only in the +courts of a jurisdiction where the defendant maintains its principal +place of business and such litigation shall be governed by laws of that +jurisdiction, without reference to its conflict-of-law provisions. +Nothing in this Section shall prevent a party's ability to bring +cross-claims or counter-claims. + +9. Miscellaneous +---------------- + +This License represents the complete agreement concerning the subject +matter hereof. If any provision of this License is held to be +unenforceable, such provision shall be reformed only to the extent +necessary to make it enforceable. Any law or regulation which provides +that the language of a contract shall be construed against the drafter +shall not be used to construe this License against a Contributor. + +10. Versions of the License +--------------------------- + +10.1. New Versions + +Mozilla Foundation is the license steward. Except as provided in Section +10.3, no one other than the license steward has the right to modify or +publish new versions of this License. Each version will be given a +distinguishing version number. + +10.2. Effect of New Versions + +You may distribute the Covered Software under the terms of the version +of the License under which You originally received the Covered Software, +or under the terms of any subsequent version published by the license +steward. + +10.3. Modified Versions + +If you create software not governed by this License, and you want to +create a new license for such software, you may create and use a +modified version of this License if you rename the license and remove +any references to the name of the license steward (except to note that +such modified license differs from this License). + +10.4. Distributing Source Code Form that is Incompatible With Secondary +Licenses + +If You choose to distribute Source Code Form that is Incompatible With +Secondary Licenses under the terms of this version of the License, the +notice described in Exhibit B of this License must be attached. + +Exhibit A - Source Code Form License Notice +------------------------------------------- + + This Source Code Form is subject to the terms of the Mozilla Public + License, v. 2.0. If a copy of the MPL was not distributed with this + file, You can obtain one at http://mozilla.org/MPL/2.0/. + +If it is not possible or desirable to put the notice in a particular +file, then You may include the notice in a location (such as a LICENSE +file in a relevant directory) where a recipient would be likely to look +for such a notice. + +You may add additional accurate notices of copyright ownership. + +Exhibit B - "Incompatible With Secondary Licenses" Notice +--------------------------------------------------------- + + This Source Code Form is "Incompatible With Secondary Licenses", as + defined by the Mozilla Public License, v. 2.0. diff --git a/README.adoc b/README.adoc new file mode 100644 index 0000000..a2dae72 --- /dev/null +++ b/README.adoc @@ -0,0 +1,141 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += arghda-core +:toc: +:toc-placement: preamble + +image:https://img.shields.io/badge/Sponsor-%E2%9D%A4-pink?logo=github[Sponsor,link=https://github.com/sponsors/hyperpolymath] +image:https://img.shields.io/badge/License-MPL_2.0-blue.svg[License,link=https://www.mozilla.org/MPL/2.0/] + +Lightweight proof-workspace manager for Agda — the language-agnostic engine +half of *arghda*. Extracted from +https://github.com/hyperpolymath/echo-types[`hyperpolymath/echo-types`] to its +own repository on 2026-05-30 (see echo-types#159 for the move record). + +arghda-core organises, lints, and reports on an Agda proof workspace; it +*never proves anything itself* — Agda does. It manages a four-state triage +workspace (inbox → working → proven → rejected) as file moves, runs a lint +pack targeting the _silent-failure_ class (cases where Agda appears to succeed +but the file is not actually in the verified suite), builds a first-class +import-graph DAG, and emits a JSON + event-stream contract a visual layer +consumes. + +== Status + +v0.1 is feature-complete against `docs/arghda-spec.adoc`: all seven v0 Agda +lint rules, the four-state workspace state machine, the import-graph `dag`, +the `check` command (Agda typecheck + lint verdict), content-hash +invalidation of `proven`, and `.arghda/config.toml` operator configuration. +The live status of record is link:.machine_readable/6a2/STATE.a2ml[`STATE.a2ml`]. + +== Lint rules + +Hard-block (forbids the `working → proven` transition): + +* `missing-safe-pragma` — file lacks `{-# OPTIONS --safe --without-K #-}`. +* `orphan-module` — `.agda` file unreachable from any CI root (roots are + auto-discovered as `All.agda`/`Smoke.agda`, or passed via `--entry`; + reachability is the _union_, so a module verified from any root is not an + orphan). +* `unjustified-postulate` — `postulate` without an adjacent `-- JUSTIFY:` + comment. + +Warn (surfaced, non-blocking): + +* `escape-hatch` — termination overrides (`TERMINATING`, `NON_TERMINATING`, + `NO_TERMINATION_CHECK`) and trust primitives (`believe_me`/`primTrustMe`). +* `tab-mix` — a tab in leading whitespace. +* `unpinned-headline` — a top-level theorem whose name matches the headline + pattern is not pinned in any `Smoke.agda` via a `using ( … )` clause (the + estate "every headline pinned in Smoke" discipline). The pattern is + operator-configurable; its default `^[a-z][A-Za-z0-9-]*$` is deliberately + broad, so operators narrow it to their own convention. Self-skips when no + `Smoke.agda` is in scope. +* `unused-import` — re-emits the findings of the external + https://github.com/msuperdock/agda-unused[`agda-unused`] tool. Opt-in behind + `scan --unused`; invoked per file in local mode with `LC_ALL=C.UTF-8`; + skipped with a note if the binary is not on `PATH`. + +== Commands + +The CLI is `arghda`. + +[cols="1,3"] +|=== +| Command | What it does + +| `init` | Create the four-state workspace layout at a path. +| `scan` | Lint every `.agda` file under a path. `--unused` adds the agda-unused pass; `--config`/`--headline-pattern` tune configuration. +| `check` | Run Agda on one file and lint it; combined verdict (degrades when `agda` is absent). +| `dag` | Emit the dependency-DAG JSON — nodes (lint status + declared `headlines`), import edges, and a blocked list. +| `claim` / `promote` / `reject` / `requeue` / `invalidate` | State-machine transitions; each is a file move logged to `.arghda/events.jsonl`. +| `events` | Replay the workspace event log. +| `stale` | List `proven` files whose content changed since promotion; `--invalidate` returns them to inbox. +| `watch` | Watch `inbox/` and `working/` and print events. +|=== + +== Configuration + +`scan` and `dag` read `.arghda/config.toml` (from `/.arghda/config.toml`, +or an explicit `--config `). Precedence is built-in default < +`config.toml` < CLI flag. + +[source,toml] +---- +[lint] +headline_pattern = "^[a-z][A-Za-z0-9-]*$" +---- + +== Build + +[source,sh] +---- +just check # fmt-check + clippy (-D warnings) + build + test — the CI gate +cargo build +cargo test +---- + +`agda` and `agda-unused` are optional: the `check` and `scan --unused` paths +degrade gracefully (with a note) when the binary is absent, so the rest of the +engine still works in an Agda-less environment. + +== Smoke against an Agda workspace + +[source,sh] +---- +cargo run -- scan path/to/your/agda/sources +---- + +Dogfooded against the echo-types corpus (193 modules): `dag` emits the +903-edge import graph; multi-root discovery (`All.agda`, `Smoke.agda`, +`Ordinal/Buchholz/Smoke.agda`, `characteristic/All.agda`, `examples/All.agda`) +narrows orphan reports from 38 to the 17 genuine orphans. + +== Ecosystem + +Part of the https://github.com/hyperpolymath[hyperpolymath ecosystem]. arghda +splits into `arghda-core` (this engine) and the planned `arghda-studio` / +`arghda-panll` visual layers, which consume the `dag` JSON + `events.jsonl` +contract. The motivating workspace was the echo-types proof pipeline, but +arghda-core has no echo-types-specific code. + +Adjacent projects: + +* https://github.com/hyperpolymath/echo-types[echo-types] — the Agda library + that motivated arghda's design (not a build dependency). +* https://github.com/hyperpolymath/absolute-zero[absolute-zero] — a sister + Agda library under the same `--safe --without-K` discipline. + +== Machine-readable + +Per the Rhodium Standard, structured project metadata lives under +link:.machine_readable/6a2/[`.machine_readable/6a2/`] — `STATE`, `META`, +`ECOSYSTEM`, `AGENTIC`, `NEUROSYM`, `PLAYBOOK` in A2ML — with +link:0-AI-MANIFEST.a2ml[`0-AI-MANIFEST.a2ml`] as the AI entry point and +link:EXPLAINME.adoc[`EXPLAINME.adoc`] as the orientation pointer. + +== Licence + +Code, configuration and scripts are `MPL-2.0` (see link:LICENSE[LICENSE]); +prose documentation is `CC-BY-SA-4.0`, per the +https://github.com/hyperpolymath/standards[hyperpolymath licence policy]. +SPDX headers are owner-managed and applied manually per file. diff --git a/README.md b/README.md deleted file mode 100644 index 60eddc6..0000000 --- a/README.md +++ /dev/null @@ -1,108 +0,0 @@ -[![Sponsor](https://img.shields.io/badge/Sponsor-%E2%9D%A4-pink?logo=github)](https://github.com/sponsors/hyperpolymath) - -# arghda-core - -Lightweight proof-workspace manager for Agda. Extracted from -[`hyperpolymath/echo-types`](https://github.com/hyperpolymath/echo-types) -to its own repository on 2026-05-30 — see echo-types#159 for the move -record. - -## v0.1 scope - -- `Workspace` struct with four-state dir layout (`inbox`, `working`, - `proven`, `rejected`) -- Filesystem watcher (`notify`-based) -- Linter rules: - - `missing-safe-pragma` — file lacks `{-# OPTIONS --safe --without-K #-}` - - `orphan-module` — `.agda` file not reachable from any CI root (roots - are auto-discovered as `All.agda`/`Smoke.agda`, or passed via `--entry`; - reachability is the *union*, so a module verified from any root is not - an orphan) - - `unjustified-postulate` — `postulate` without an adjacent `-- JUSTIFY:` comment - - `escape-hatch` (warn) — termination overrides (`TERMINATING`, - `NON_TERMINATING`, `NO_TERMINATION_CHECK`) and trust primitives - (`believe_me`/`primTrustMe`) - - `tab-mix` (warn) — a tab in leading whitespace - - `unpinned-headline` (warn) — a top-level theorem whose name matches the - headline pattern is not pinned in any `Smoke.agda` via a `using ( … )` - clause (the estate "every headline pinned in Smoke" discipline). The - pattern is operator-configurable (via `.arghda/config.toml` or - `--headline-pattern `); its default `^[a-z][A-Za-z0-9-]*$` is - deliberately broad, so operators narrow it to their own headline-naming - convention. Self-skips when no `Smoke.agda` is in scope (e.g. a - single-file `check`) - - `unused-import` (warn) — re-emits the findings of the external - [`agda-unused`](https://github.com/msuperdock/agda-unused) tool. Opt-in - behind `scan --unused` (it runs `agda-unused` per file in local mode and - re-checks each file); skipped with a note if the binary is not on `PATH`. - Invoked with `LC_ALL=C.UTF-8` so it can read UTF-8 Agda sources -- Workspace state machine — transitions are file moves, each logged to - `.arghda/events.jsonl` (`claim`, `promote`, `reject`, `requeue`, - `invalidate`) -- `dag` — emits the dependency-DAG JSON (nodes — each with its lint status - and declared `headlines` — plus import edges and a blocked list) for a - source tree: the contract a visual layer consumes -- `check` — runs Agda on a file and combines the typecheck verdict with the - lint report (degrades gracefully when `agda` is absent) -- First-class import graph (the `graph` module, lifted out of the orphan rule) -- CLI (`arghda`): `init`, `scan`, `check`, `dag`, `claim`, `promote`, - `reject`, `requeue`, `invalidate`, `events`, `watch` - -Dogfooded against the echo-types corpus (193 modules): `dag` emits the -903-edge import graph; multi-root discovery (5 roots: `All.agda`, -`Smoke.agda`, `Ordinal/Buchholz/Smoke.agda`, `characteristic/All.agda`, -`examples/All.agda`) narrows orphan reports from 38 to the 17 genuine -orphans — the `experimental/echo-additive/` tree (including -`VarianceGate.agda`, the orphan the 2026-06-16 trust audit found by hand) -plus standalone scratch files. `scan` also flags the files deliberately -outside the `--safe --without-K` kernel cone (`Fidelity.agda`, the cubical -island, the postulated shadow). - -Configuration: `scan` and `dag` read `.arghda/config.toml` (from -`/.arghda/config.toml`, or an explicit `--config `). Precedence is -built-in default < `config.toml` < CLI flag. Current schema: - -```toml -[lint] -headline_pattern = "^[a-z][A-Za-z0-9-]*$" -``` - -Not yet: the Groove service manifest. (`missing-without-k` is subsumed by -`missing-safe-pragma`, which already reports a missing `--without-K`.) - -## Build - -``` -cargo build -cargo test -``` - -## Smoke against an Agda workspace - -``` -cargo run -- scan path/to/your/agda/sources -``` - -Expected output enumerates per-file lint hits. With no `All.agda` -present, `orphan-module` is a no-op; with one present, modules -unreachable from `All.agda` get flagged. - -## Ecosystem context - -Part of the [hyperpolymath ecosystem](https://github.com/hyperpolymath). -The original design motivation was the echo-types proof pipeline -(triage folders `inbox → working → proven → rejected`), but `arghda` -operates on any `--safe --without-K` Agda workspace; it has no -echo-types-specific code. - -Adjacent projects: - -- [echo-types](https://github.com/hyperpolymath/echo-types) — the - Agda library that motivated arghda's design; arghda is not a - build-dependency. -- [absolute-zero](https://github.com/hyperpolymath/absolute-zero) — - a sister Agda library with the same `--safe --without-K` discipline. - -## License - -MPL-2.0. SPDX headers on each source file. From af5fa44ef33409de54134e97ab5f710ee286dec6 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 20 Jun 2026 05:14:30 +0000 Subject: [PATCH 2/2] chore(licence): apply + enforce MPL-2.0 / CC-BY-SA-4.0 SPDX invariant MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Owner-directed (satisfies LICENCE-POLICY.adoc A2's "manual, per-file, by the owner" gate). Makes the licence split a formal, enforced invariant. - Applied SPDX headers per file: MPL-2.0 to all code/config/scripts/state (25 src+tests .rs, Cargo.toml, .gitignore); CC-BY-SA-4.0 to prose. Fixed prose drift: CHANGELOG/CONTRIBUTING/SECURITY MPL-2.0 -> CC-BY-SA-4.0, and docs/*.adoc CC-BY-4.0 -> CC-BY-SA-4.0 (the check caught the missing -SA). - New scripts/check-spdx.sh enforces the invariant; wired into `just check` (new `license-check` recipe) and .github/workflows/rust-ci.yml. - New .machine_readable/licensing-policy.toml declares the rule + the excluded set machine-readably. Third-party protection: nothing not ours is relicensed. Cargo.lock (generated, enumerates third-party deps), LICENSE (the MPL text itself), and tests/fixtures/ (Agda test-input data) are excluded. There is no vendored third-party source in-tree; if any is added, the checker FAILS until it is listed as excluded with its original SPDX preserved — that failure is the guard against silent relicensing. `bash scripts/check-spdx.sh` OK; fmt/clippy/test green. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_019GiSiEfgZCte35dyykgBHs --- .github/workflows/rust-ci.yml | 3 ++ .gitignore | 3 ++ .machine_readable/6a2/STATE.a2ml | 10 ++--- .machine_readable/licensing-policy.toml | 36 +++++++++++++++ CHANGELOG.md | 13 ++++-- CONTRIBUTING.md | 2 +- Cargo.toml | 3 ++ Justfile | 7 ++- README.adoc | 9 +++- SECURITY.md | 2 +- docs/arghda-spec.adoc | 2 +- docs/arghda-vision.adoc | 2 +- scripts/check-spdx.sh | 58 +++++++++++++++++++++++++ src/agda.rs | 3 ++ src/config.rs | 3 ++ src/dag.rs | 3 ++ src/diagnostic.rs | 3 ++ src/event.rs | 3 ++ src/graph.rs | 3 ++ src/hash.rs | 3 ++ src/lib.rs | 3 ++ src/lint/escape_hatch.rs | 3 ++ src/lint/mod.rs | 3 ++ src/lint/orphan_module.rs | 3 ++ src/lint/postulate.rs | 3 ++ src/lint/safe_pragma.rs | 3 ++ src/lint/tab_mix.rs | 3 ++ src/lint/unpinned_headline.rs | 3 ++ src/main.rs | 3 ++ src/proven.rs | 3 ++ src/timestamp.rs | 3 ++ src/unused.rs | 3 ++ src/watcher.rs | 3 ++ src/workspace.rs | 3 ++ tests/dag.rs | 3 ++ tests/proven.rs | 3 ++ tests/smoke.rs | 3 ++ tests/transitions.rs | 3 ++ 38 files changed, 209 insertions(+), 16 deletions(-) create mode 100644 .machine_readable/licensing-policy.toml create mode 100755 scripts/check-spdx.sh diff --git a/.github/workflows/rust-ci.yml b/.github/workflows/rust-ci.yml index 5325346..648adbb 100644 --- a/.github/workflows/rust-ci.yml +++ b/.github/workflows/rust-ci.yml @@ -49,6 +49,9 @@ jobs: cargo --version rustup component add clippy rustfmt + - name: SPDX licence invariant + run: bash scripts/check-spdx.sh + - name: cargo fmt --check run: cargo fmt --all -- --check diff --git a/.gitignore b/.gitignore index 2dcc89f..b733efa 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,6 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + # Rust build artefacts target/ diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 93ad619..195925b 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -34,15 +34,13 @@ milestones = [ ] [blockers-and-issues] -# No active blockers. v0.1 lint set + DAG schema (arghda-spec.adoc) are complete. -# Known compliance gap (owner-manual only, per LICENCE-POLICY A2 — never an -# agent sweep): src/*.rs lack per-file `// SPDX-License-Identifier: MPL-2.0` -# headers. The repo is declared MPL-2.0 (Cargo.toml, LICENSE); applying the -# per-file headers is owner-driven manual work. +# No active blockers. v0.1 lint set + DAG schema (arghda-spec.adoc) are +# complete. The SPDX licence invariant is applied and enforced +# (scripts/check-spdx.sh; .machine_readable/licensing-policy.toml). [critical-next-actions] actions = [ - "Owner-manual: apply MPL-2.0 SPDX headers to src/*.rs (no agent bulk sweep — LICENCE-POLICY A2)", + "Formalise template-applicability rules (capability-gated RSR profile: carry a template module iff the repo declares the capability it serves) — estate-wide, candidate for hyperpolymath/standards", "Extend content-hash invalidation to cover transitive imports (needs include-root tracking)", "Serve /.well-known/groove for PanLL discovery (Groove protocol)", "Scaffold arghda-studio (AffineScript visual layer consuming the dag JSON)", diff --git a/.machine_readable/licensing-policy.toml b/.machine_readable/licensing-policy.toml new file mode 100644 index 0000000..ecc0e3c --- /dev/null +++ b/.machine_readable/licensing-policy.toml @@ -0,0 +1,36 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# Licence invariant for arghda-core — machine-readable declaration of the rule +# enforced by scripts/check-spdx.sh (run in `just check` + Rust CI). The split +# itself comes from hyperpolymath/standards LICENCE-POLICY.adoc Rule 1. + +[invariant] +enforced = true +checker = "scripts/check-spdx.sh" +wired-into = ["Justfile (just check / just license-check)", ".github/workflows/rust-ci.yml"] + +[licences] +# By content type, not by directory. +code = "MPL-2.0" # *.rs, *.toml, *.a2ml, *.yml, *.sh, Justfile, .gitignore, .well-known/* +prose = "CC-BY-SA-4.0" # *.adoc, *.md narrative +# Canonical texts: MPL-2.0 -> ./LICENSE ; CC-BY-SA-4.0 -> standards/LICENSES/CC-BY-SA-4.0.txt + +[excluded] +# NOT ours, generated, or test-input data. These never carry the repo's +# licence choices; the checker skips them. +paths = [ + "Cargo.lock", # generated by cargo; enumerates third-party dependencies + "LICENSE", # the MPL-2.0 licence text itself + "target/", # cargo build output (gitignored) + "tests/fixtures/", # Agda test-input data (some deliberately malformed) +] + +[third-party] +# arghda-core vendors NO third-party source in-tree: every dependency is +# fetched by cargo (declared in Cargo.toml, pinned in Cargo.lock) and is never +# relicensed. If third-party source is ever vendored in-tree, add its path to +# [excluded] above and preserve its ORIGINAL SPDX header verbatim. The checker +# fails on any unrecognised in-tree file until it is excluded — that failure is +# the intended guard against silently relicensing others' code. +vendored-in-tree = [] diff --git a/CHANGELOG.md b/CHANGELOG.md index 371ad8e..818ba11 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,4 +1,4 @@ - + # Changelog All notable changes to arghda-core are documented here. The format follows @@ -16,8 +16,15 @@ All notable changes to arghda-core are documented here. The format follows docs carry `CC-BY-SA-4.0`; code/config/state stay `MPL-2.0` (per the estate licence policy). Refreshed `.machine_readable/6a2/STATE.a2ml` + `META.a2ml` and the `0-AI-MANIFEST.a2ml` read-order; removed local `dist-newstyle/` - build cruft. (Per-file SPDX headers on `src/*.rs` remain owner-manual by - policy — never an agent bulk sweep.) + build cruft. +- Formal SPDX licence invariant (owner-directed): every tracked file carries + the correct header — `MPL-2.0` for code/config/scripts/state, `CC-BY-SA-4.0` + for prose — applied per file (incl. all `src/*.rs`) and enforced by + `scripts/check-spdx.sh`, wired into `just check` and Rust CI. Third-party, + generated (`Cargo.lock`), and test-data (`tests/fixtures/`) files are + explicitly excluded and never relicensed; `docs/*.adoc` normalised from + `CC-BY-4.0` to `CC-BY-SA-4.0`. Declared in + `.machine_readable/licensing-policy.toml`. ### Added diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 0fa2722..8ad261f 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -1,4 +1,4 @@ - + # Contributing to arghda-core arghda-core is the Rust engine for the arghda proof-workspace tool. diff --git a/Cargo.toml b/Cargo.toml index 455e3b2..0533a63 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,3 +1,6 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + [package] name = "arghda-core" version = "0.1.0" diff --git a/Justfile b/Justfile index 7a71331..150f8b0 100644 --- a/Justfile +++ b/Justfile @@ -32,8 +32,13 @@ fmt-check: lint: cargo clippy --all-targets -- -D warnings +# SPDX licence invariant: MPL-2.0 for code/config/scripts, CC-BY-SA-4.0 for +# prose; third-party / generated / test data excluded (CI gate). +license-check: + bash scripts/check-spdx.sh + # The full CI gate, exactly what .github/workflows/rust-ci.yml runs. -check: fmt-check lint build test +check: fmt-check lint license-check build test # Alias for CI. ci: check diff --git a/README.adoc b/README.adoc index a2dae72..f196154 100644 --- a/README.adoc +++ b/README.adoc @@ -137,5 +137,10 @@ link:EXPLAINME.adoc[`EXPLAINME.adoc`] as the orientation pointer. Code, configuration and scripts are `MPL-2.0` (see link:LICENSE[LICENSE]); prose documentation is `CC-BY-SA-4.0`, per the -https://github.com/hyperpolymath/standards[hyperpolymath licence policy]. -SPDX headers are owner-managed and applied manually per file. +https://github.com/hyperpolymath/standards[hyperpolymath licence policy] (Rule +1). This split is a **formal invariant**: every tracked file carries the +appropriate SPDX header, checked by `scripts/check-spdx.sh` in `just check` and +in CI. Third-party, generated, and test-data files are explicitly excluded +(link:.machine_readable/licensing-policy.toml[`licensing-policy.toml`]) and are +never relicensed — vendoring third-party source in-tree fails the check until +it is listed as excluded with its original SPDX preserved. diff --git a/SECURITY.md b/SECURITY.md index 758453f..9aa8ee8 100644 --- a/SECURITY.md +++ b/SECURITY.md @@ -1,4 +1,4 @@ - + # Security Policy ## Supported versions diff --git a/docs/arghda-spec.adoc b/docs/arghda-spec.adoc index 7062284..dc21728 100644 --- a/docs/arghda-spec.adoc +++ b/docs/arghda-spec.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: CC-BY-4.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell = ArghDA MVP Specification :toc: macro diff --git a/docs/arghda-vision.adoc b/docs/arghda-vision.adoc index 5ecdae9..6c81414 100644 --- a/docs/arghda-vision.adoc +++ b/docs/arghda-vision.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: CC-BY-4.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell = ArghDA — Vision, Architecture & Roadmap :toc: macro diff --git a/scripts/check-spdx.sh b/scripts/check-spdx.sh new file mode 100755 index 0000000..981b24e --- /dev/null +++ b/scripts/check-spdx.sh @@ -0,0 +1,58 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# Licence invariant for arghda-core (enforced by `just check` + Rust CI). +# +# code / config / scripts / state -> SPDX-License-Identifier: MPL-2.0 +# prose documentation (*.adoc, *.md) -> SPDX-License-Identifier: CC-BY-SA-4.0 +# +# Files that are NOT ours, generated, or test-input data are EXCLUDED and must +# never carry the repo's licence choices. The machine-readable declaration of +# this rule is .machine_readable/licensing-policy.toml; the split itself comes +# from hyperpolymath/standards LICENCE-POLICY.adoc Rule 1. +# +# Guard for third-party code: any tracked, non-excluded file that lacks our +# header FAILS the check. Vendoring third-party source therefore forces a +# conscious exclusion (and the file keeps its original SPDX) rather than being +# silently relicensed. +set -euo pipefail +cd "$(git rev-parse --show-toplevel)" + +MPL='SPDX-License-Identifier: MPL-2.0' +CC='SPDX-License-Identifier: CC-BY-SA-4.0' +fail=0 + +# Not ours / generated / test-input data — see [excluded] in the policy file. +excluded() { + case "$1" in + Cargo.lock | LICENSE) return 0 ;; # generated lockfile / the licence text itself + target/* | tests/fixtures/*) return 0 ;; # build output / Agda test-input data + *) return 1 ;; + esac +} + +while IFS= read -r f; do + excluded "$f" && continue + case "$f" in + *.adoc | *.md) want="$CC"; label="CC-BY-SA-4.0 (prose)" ;; + *) want="$MPL"; label="MPL-2.0 (code/config/script/state)" ;; + esac + if ! grep -qF "$want" "$f"; then + echo " MISSING $label: $f" + fail=1 + fi +done < <(git ls-files) + +if [ "$fail" -ne 0 ]; then + cat >&2 <<'MSG' +SPDX licence invariant: FAIL (see above). +Fix one of: + * add the correct SPDX header to the file, OR + * if the file is third-party / generated / test data, add it to the + excluded set in scripts/check-spdx.sh AND + .machine_readable/licensing-policy.toml — never relicense others' code. +MSG + exit 1 +fi +echo "SPDX licence invariant: OK" diff --git a/src/agda.rs b/src/agda.rs index 9894541..ee65ad2 100644 --- a/src/agda.rs +++ b/src/agda.rs @@ -1,3 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + //! Shelling out to `agda` to typecheck a file. //! //! ArghDA never proves anything itself — it asks Agda. This module runs diff --git a/src/config.rs b/src/config.rs index 372f684..59d0ef6 100644 --- a/src/config.rs +++ b/src/config.rs @@ -1,3 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + //! Operator configuration from `.arghda/config.toml`. //! //! The spec makes the `unpinned-headline` pattern operator-overridable diff --git a/src/dag.rs b/src/dag.rs index 30a7894..8c7a210 100644 --- a/src/dag.rs +++ b/src/dag.rs @@ -1,3 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + //! The DAG document — the JSON contract a visual layer consumes. //! //! Builds on the import graph (`crate::graph`) plus a lint pass over every diff --git a/src/diagnostic.rs b/src/diagnostic.rs index 6061774..9af001d 100644 --- a/src/diagnostic.rs +++ b/src/diagnostic.rs @@ -1,3 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + use serde::{Deserialize, Serialize}; use std::path::PathBuf; diff --git a/src/event.rs b/src/event.rs index 9026162..df15ce0 100644 --- a/src/event.rs +++ b/src/event.rs @@ -1,3 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + //! The triage event stream. //! //! Every state transition appends one JSON object (one line) to diff --git a/src/graph.rs b/src/graph.rs index faf837f..f912a49 100644 --- a/src/graph.rs +++ b/src/graph.rs @@ -1,3 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + //! First-class Agda import graph. //! //! The reachability primitives (`module_name_of`, `module_to_path`, diff --git a/src/hash.rs b/src/hash.rs index eaea825..8dad5e5 100644 --- a/src/hash.rs +++ b/src/hash.rs @@ -1,3 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + //! Dependency-free SHA-256 (FIPS 180-4). //! //! Used for `proven`-state content hashing — detecting when a file changes diff --git a/src/lib.rs b/src/lib.rs index 48ff1c1..7e0a8ee 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,3 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + //! arghda-core: proof-workspace manager for Agda. //! //! Public surface is intentionally small: `Workspace`, the lint traits, diff --git a/src/lint/escape_hatch.rs b/src/lint/escape_hatch.rs index 5d05c16..37edc66 100644 --- a/src/lint/escape_hatch.rs +++ b/src/lint/escape_hatch.rs @@ -1,3 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + //! `escape-hatch` (warn) — surface soundness escape hatches. //! //! Flags termination-checker overrides (`{-# TERMINATING #-}`, diff --git a/src/lint/mod.rs b/src/lint/mod.rs index 649d2b9..63f2e67 100644 --- a/src/lint/mod.rs +++ b/src/lint/mod.rs @@ -1,3 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + use crate::diagnostic::LintReport; use anyhow::Result; use std::path::{Path, PathBuf}; diff --git a/src/lint/orphan_module.rs b/src/lint/orphan_module.rs index bd33a99..2869943 100644 --- a/src/lint/orphan_module.rs +++ b/src/lint/orphan_module.rs @@ -1,3 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + use super::{LintContext, LintRule}; use crate::diagnostic::{Diagnostic, LintReport, Severity}; use crate::graph::{module_name_of, reachable_from_roots}; diff --git a/src/lint/postulate.rs b/src/lint/postulate.rs index a335494..ba3d0ec 100644 --- a/src/lint/postulate.rs +++ b/src/lint/postulate.rs @@ -1,3 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + //! `unjustified-postulate` — flag `postulate` openers that lack an //! adjacent `-- JUSTIFY:` rationale. //! diff --git a/src/lint/safe_pragma.rs b/src/lint/safe_pragma.rs index 5e330ab..2d19a4a 100644 --- a/src/lint/safe_pragma.rs +++ b/src/lint/safe_pragma.rs @@ -1,3 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + use super::{LintContext, LintRule}; use crate::diagnostic::{Diagnostic, LintReport, Severity}; use anyhow::{Context, Result}; diff --git a/src/lint/tab_mix.rs b/src/lint/tab_mix.rs index 8cfa138..e4fc784 100644 --- a/src/lint/tab_mix.rs +++ b/src/lint/tab_mix.rs @@ -1,3 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + //! `tab-mix` (warn) — flag tabs used for indentation. //! //! Agda's layout rule and the estate style use spaces; a stray tab in diff --git a/src/lint/unpinned_headline.rs b/src/lint/unpinned_headline.rs index 4a47775..c2bd87b 100644 --- a/src/lint/unpinned_headline.rs +++ b/src/lint/unpinned_headline.rs @@ -1,3 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + //! `unpinned-headline` (warn) — a module declares a top-level theorem whose //! name matches the headline pattern, but the name is not pinned in any //! `Smoke.agda` via a `using ( … )` clause. diff --git a/src/main.rs b/src/main.rs index 0df60ed..3d6f803 100644 --- a/src/main.rs +++ b/src/main.rs @@ -1,3 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + use anyhow::{Context, Result}; use arghda_core::lint::LintContext; use arghda_core::{ diff --git a/src/proven.rs b/src/proven.rs index b98cfc3..55d2b0e 100644 --- a/src/proven.rs +++ b/src/proven.rs @@ -1,3 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + //! The `proven`-state content-hash manifest (`.arghda/hashes.json`). //! //! When a file is promoted to `proven`, its content hash is recorded here. diff --git a/src/timestamp.rs b/src/timestamp.rs index c3d1cd7..e7a982e 100644 --- a/src/timestamp.rs +++ b/src/timestamp.rs @@ -1,3 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + //! Dependency-free UTC timestamps. //! //! Emits RFC 3339 / ISO-8601 strings (e.g. `2026-06-18T11:45:32Z`) without diff --git a/src/unused.rs b/src/unused.rs index a47f87b..f48250f 100644 --- a/src/unused.rs +++ b/src/unused.rs @@ -1,3 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + //! Shelling out to `agda-unused` to find unused code (the `unused-import` rule). //! //! Like [`crate::agda`], ArghDA does not analyse for unused code itself — it diff --git a/src/watcher.rs b/src/watcher.rs index 1f4e420..71a032d 100644 --- a/src/watcher.rs +++ b/src/watcher.rs @@ -1,3 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + use anyhow::Result; use notify::{RecommendedWatcher, RecursiveMode, Watcher}; use std::path::Path; diff --git a/src/workspace.rs b/src/workspace.rs index 41c02f5..3a0dcd0 100644 --- a/src/workspace.rs +++ b/src/workspace.rs @@ -1,3 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + use crate::event::{self, Event, EventKind}; use crate::proven::{self, ProvenRecord}; use anyhow::{Context, Result}; diff --git a/tests/dag.rs b/tests/dag.rs index 3936a29..e227172 100644 --- a/tests/dag.rs +++ b/tests/dag.rs @@ -1,3 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + //! `dag` document construction over the fixtures. use arghda_core::lint::unpinned_headline::DEFAULT_HEADLINE_PATTERN; diff --git a/tests/proven.rs b/tests/proven.rs index 72191f3..915d6d6 100644 --- a/tests/proven.rs +++ b/tests/proven.rs @@ -1,3 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + //! Proven-state content hashing and staleness detection. use arghda_core::{proven, State, Workspace}; diff --git a/tests/smoke.rs b/tests/smoke.rs index eab65a4..68d417d 100644 --- a/tests/smoke.rs +++ b/tests/smoke.rs @@ -1,3 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + //! End-to-end smoke tests for the v0.1 lint pack. //! //! Each test runs the default rule pack against a self-contained diff --git a/tests/transitions.rs b/tests/transitions.rs index ded4257..872118e 100644 --- a/tests/transitions.rs +++ b/tests/transitions.rs @@ -1,3 +1,6 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + //! Workspace state-machine transitions and the event log. use arghda_core::{event, EventKind, State, Workspace};