Skip to content

Commit e253289

Browse files
chore(rsr): standards compliance — adoc-first cleanup + licence invariant (#10)
## Summary Brings arghda-core to the hyperpolymath **standards / RSR** baseline, clears root cruft, and makes the **MPL-2.0 / CC-BY-SA-4.0 licence split a formal, enforced invariant**. Two commits: ### 1 — adoc-first cleanup + RSR baseline (`5b7aff4`) - `README.md` → **`README.adoc`** (adoc-first), refreshed to feature-complete v0.1. New **`EXPLAINME.adoc`**, **`LICENSE`** (full MPL-2.0), **`CODE_OF_CONDUCT.md`**. Refreshed `STATE`/`META`/`0-AI-MANIFEST`. Removed `dist-newstyle/`. No duplicate doc formats; `just validate-rsr` passes. ### 2 — licence invariant (`af5fa44`, owner-directed) - Applied SPDX headers per file: **`MPL-2.0`** to all code/config/scripts/state (25 `.rs`, `Cargo.toml`, `.gitignore`), **`CC-BY-SA-4.0`** to prose. Fixed drift: prose docs that were `MPL-2.0` or `CC-BY-4.0` → `CC-BY-SA-4.0`. - New **`scripts/check-spdx.sh`** enforces the split; wired into `just check` + Rust CI. New **`.machine_readable/licensing-policy.toml`** declares it machine-readably. - **Third-party protection:** `Cargo.lock` (generated), `LICENSE` (the licence text), and `tests/fixtures/` (Agda test data) are excluded and never relicensed. No vendored third-party source exists in-tree; if any is added, the checker fails until it's listed as excluded **with its original SPDX preserved** — the guard against silent relicensing. ## Deliberately NOT done - The maximalist rsr-template tree (`build/just`, `verification/proofs`, `container/`, hundreds of placeholder dirs) — vestigial for a small Rust CLI. A formal *capability-gated* rule for this ("carry a template module iff the repo has the capability it serves") is the proposed follow-up (recorded in `STATE.a2ml`). ## Verification `bash scripts/check-spdx.sh` ✓ · `cargo fmt --check` ✓ · `cargo clippy -D warnings` ✓ · `cargo test` ✓ (7 groups) · `just validate-rsr` ✓. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_019GiSiEfgZCte35dyykgBHs
2 parents 3f761e2 + af5fa44 commit e253289

44 files changed

Lines changed: 786 additions & 132 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

.github/workflows/rust-ci.yml

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -49,6 +49,9 @@ jobs:
4949
cargo --version
5050
rustup component add clippy rustfmt
5151
52+
- name: SPDX licence invariant
53+
run: bash scripts/check-spdx.sh
54+
5255
- name: cargo fmt --check
5356
run: cargo fmt --all -- --check
5457

.gitignore

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,6 @@
1+
# SPDX-License-Identifier: MPL-2.0
2+
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
14
# Rust build artefacts
25
target/
36

.machine_readable/6a2/META.a2ml

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
66

77
[metadata]
88
version = "0.1.0"
9-
last-updated = "2026-06-18"
9+
last-updated = "2026-06-20"
1010

1111
[project-info]
1212
type = "library" # library | binary | monorepo | service | website
@@ -20,6 +20,9 @@ author = "Jonathan D.A. Jewell (hyperpolymath)"
2020
# - { id = "ADR-002", title = "Triage transitions are file moves; ground truth is the filesystem", status = "accepted", date = "2026-05-30" }
2121
# - { id = "ADR-003", title = "Dependency-free RFC 3339 timestamps (hermetic build, no chrono)", status = "accepted", date = "2026-06-18" }
2222
# - { id = "ADR-004", title = "Orphan reachability is the union of discovered CI roots (All.agda/Smoke.agda)", status = "accepted", date = "2026-06-18" }
23+
# - { 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" }
24+
# - { 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" }
25+
# - { id = "ADR-007", title = "DAG node `headlines` reuses the unpinned-headline extractor with the configured pattern", status = "accepted", date = "2026-06-20" }
2326

2427
[development-practices]
2528
build-tool = "just"

.machine_readable/6a2/STATE.a2ml

Lines changed: 22 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -6,13 +6,13 @@
66
[metadata]
77
project = "arghda-core"
88
version = "0.1.0"
9-
last-updated = "2026-06-18"
9+
last-updated = "2026-06-20"
1010
status = "active" # active | paused | archived
1111

1212
[project-context]
1313
name = "arghda-core"
1414
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."
15-
completion-percentage = 55
15+
completion-percentage = 85
1616

1717
[position]
1818
phase = "implementation" # design | implementation | testing | maintenance | archived
@@ -21,37 +21,44 @@ maturity = "alpha" # experimental | alpha | beta | production | lts
2121
[route-to-mvp]
2222
milestones = [
2323
{ name = "Workspace scaffold + filesystem watcher", completion = 100 },
24-
{ name = "Lint pack (missing-safe-pragma, orphan-module, unjustified-postulate, escape-hatch, tab-mix)", completion = 100 },
25-
{ name = "First-class import graph + `dag` JSON command", completion = 100 },
24+
{ name = "Hard-block lint pack (missing-safe-pragma, orphan-module, unjustified-postulate)", completion = 100 },
25+
{ name = "Warn lint pack (escape-hatch, tab-mix, unpinned-headline, unused-import)", completion = 100 },
26+
{ name = "First-class import graph + `dag` JSON command (nodes incl. headlines, edges, blocked)", completion = 100 },
2627
{ name = "State machine (claim/promote/reject/requeue/invalidate) + events.jsonl", completion = 100 },
2728
{ name = "`check` command (Agda typecheck + lint verdict)", completion = 100 },
2829
{ name = "Multi-root reachability (union of discovered CI roots)", completion = 100 },
29-
{ name = "Content-hash invalidation of proven (file-level; +imports deferred)", completion = 75 },
30-
{ name = "Remaining lint rules (unpinned-headline, unused-import)", completion = 0 },
31-
{ name = "Groove service manifest (/.well-known/groove)", completion = 0 },
32-
{ name = "RSR retrofit (.machine_readable, Justfile, .well-known)", completion = 60 },
30+
{ name = "Content-hash invalidation of proven (file-level; transitive imports deferred)", completion = 75 },
31+
{ name = "Operator config (.arghda/config.toml + --headline-pattern + --config)", completion = 100 },
32+
{ name = "RSR / standards alignment (.machine_readable, README.adoc, EXPLAINME, LICENSE, .well-known)", completion = 100 },
33+
{ name = "Groove service manifest (/.well-known/groove) for PanLL discovery", completion = 0 },
3334
]
3435

3536
[blockers-and-issues]
36-
# No active blockers. `unpinned-headline` needs Smoke.agda parsing + a
37-
# configurable headline regex; `unused-import` shells out to `agda-unused`.
37+
# No active blockers. v0.1 lint set + DAG schema (arghda-spec.adoc) are
38+
# complete. The SPDX licence invariant is applied and enforced
39+
# (scripts/check-spdx.sh; .machine_readable/licensing-policy.toml).
3840

3941
[critical-next-actions]
4042
actions = [
41-
"Add unpinned-headline (needs config + headline regex) + unused-import (agda-unused) lint rules",
42-
"Extend content-hash to cover transitive imports (needs include-root tracking)",
43-
"Serve /.well-known/groove for PanLL discovery",
43+
"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",
44+
"Extend content-hash invalidation to cover transitive imports (needs include-root tracking)",
45+
"Serve /.well-known/groove for PanLL discovery (Groove protocol)",
4446
"Scaffold arghda-studio (AffineScript visual layer consuming the dag JSON)",
4547
]
4648

4749
[maintenance-status]
48-
last-run-utc = "never"
49-
last-result = "unknown" # unknown | pass | warn | fail
50+
last-run-utc = "2026-06-20"
51+
last-result = "pass" # unknown | pass | warn | fail
5052
open-warnings = 0
5153
open-failures = 0
54+
# `just check` (fmt-check + clippy -D warnings + build + test) green; ~50 lib
55+
# tests + integration suites pass. Dogfooded against echo-types + a live
56+
# agda-unused build.
5257

5358
[ecosystem]
5459
part-of = ["arghda"]
5560
depends-on = []
61+
# Build deps: anyhow, clap, notify, regex, serde, serde_json, toml, walkdir.
62+
# Optional external tools: agda, agda-unused (both degrade gracefully).
5663
# Downstream consumers: arghda-studio (planned), arghda-panll (planned).
5764
# Dogfood workspaces: echo-types, absolute-zero.
Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
# SPDX-License-Identifier: MPL-2.0
2+
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
#
4+
# Licence invariant for arghda-core — machine-readable declaration of the rule
5+
# enforced by scripts/check-spdx.sh (run in `just check` + Rust CI). The split
6+
# itself comes from hyperpolymath/standards LICENCE-POLICY.adoc Rule 1.
7+
8+
[invariant]
9+
enforced = true
10+
checker = "scripts/check-spdx.sh"
11+
wired-into = ["Justfile (just check / just license-check)", ".github/workflows/rust-ci.yml"]
12+
13+
[licences]
14+
# By content type, not by directory.
15+
code = "MPL-2.0" # *.rs, *.toml, *.a2ml, *.yml, *.sh, Justfile, .gitignore, .well-known/*
16+
prose = "CC-BY-SA-4.0" # *.adoc, *.md narrative
17+
# Canonical texts: MPL-2.0 -> ./LICENSE ; CC-BY-SA-4.0 -> standards/LICENSES/CC-BY-SA-4.0.txt
18+
19+
[excluded]
20+
# NOT ours, generated, or test-input data. These never carry the repo's
21+
# licence choices; the checker skips them.
22+
paths = [
23+
"Cargo.lock", # generated by cargo; enumerates third-party dependencies
24+
"LICENSE", # the MPL-2.0 licence text itself
25+
"target/", # cargo build output (gitignored)
26+
"tests/fixtures/", # Agda test-input data (some deliberately malformed)
27+
]
28+
29+
[third-party]
30+
# arghda-core vendors NO third-party source in-tree: every dependency is
31+
# fetched by cargo (declared in Cargo.toml, pinned in Cargo.lock) and is never
32+
# relicensed. If third-party source is ever vendored in-tree, add its path to
33+
# [excluded] above and preserve its ORIGINAL SPDX header verbatim. The checker
34+
# fails on any unrecognised in-tree file until it is excluded — that failure is
35+
# the intended guard against silently relicensing others' code.
36+
vendored-in-tree = []

0-AI-MANIFEST.a2ml

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,17 +5,18 @@
55

66
[metadata]
77
version = "0.1.0"
8-
last-updated = "2026-06-18"
8+
last-updated = "2026-06-20"
99

1010
[project]
1111
name = "arghda-core"
1212
purpose = "Language-agnostic proof-workspace engine for the arghda visual proof-wiring tool (Agda first). Emits the DAG / events.jsonl JSON contract a visual layer consumes; never proves anything itself."
1313

1414
[entry]
1515
read-order = [
16+
"EXPLAINME.adoc",
1617
".machine_readable/6a2/STATE.a2ml",
1718
".machine_readable/6a2/META.a2ml",
18-
"README.md",
19+
"README.adoc",
1920
"docs/arghda-spec.adoc",
2021
"docs/arghda-vision.adoc",
2122
]

CHANGELOG.md

Lines changed: 20 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
<!-- SPDX-License-Identifier: MPL-2.0 -->
1+
<!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->
22
# Changelog
33

44
All notable changes to arghda-core are documented here. The format follows
@@ -7,6 +7,25 @@ All notable changes to arghda-core are documented here. The format follows
77

88
## [Unreleased]
99

10+
### Changed
11+
12+
- Standards / RSR alignment and root cleanup: `README.md``README.adoc`
13+
(adoc-first; refreshed to the feature-complete v0.1 status), no duplicate
14+
doc formats. Added `EXPLAINME.adoc` (orientation pointer), `LICENSE` (full
15+
MPL-2.0 text), and `CODE_OF_CONDUCT.md` (Contributor Covenant 2.1). Prose
16+
docs carry `CC-BY-SA-4.0`; code/config/state stay `MPL-2.0` (per the estate
17+
licence policy). Refreshed `.machine_readable/6a2/STATE.a2ml` + `META.a2ml`
18+
and the `0-AI-MANIFEST.a2ml` read-order; removed local `dist-newstyle/`
19+
build cruft.
20+
- Formal SPDX licence invariant (owner-directed): every tracked file carries
21+
the correct header — `MPL-2.0` for code/config/scripts/state, `CC-BY-SA-4.0`
22+
for prose — applied per file (incl. all `src/*.rs`) and enforced by
23+
`scripts/check-spdx.sh`, wired into `just check` and Rust CI. Third-party,
24+
generated (`Cargo.lock`), and test-data (`tests/fixtures/`) files are
25+
explicitly excluded and never relicensed; `docs/*.adoc` normalised from
26+
`CC-BY-4.0` to `CC-BY-SA-4.0`. Declared in
27+
`.machine_readable/licensing-policy.toml`.
28+
1029
### Added
1130

1231
- `dag` command emitting the dependency-DAG JSON contract (nodes with

CODE_OF_CONDUCT.md

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
<!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->
2+
<!-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
3+
# Code of Conduct
4+
5+
This project follows the [Contributor Covenant 2.1](https://www.contributor-covenant.org/version/2/1/code_of_conduct/).
6+
7+
Reports go to `j.d.a.jewell@open.ac.uk`. Reports are confidential by default.

CONTRIBUTING.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
<!-- SPDX-License-Identifier: MPL-2.0 -->
1+
<!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->
22
# Contributing to arghda-core
33

44
arghda-core is the Rust engine for the arghda proof-workspace tool.

Cargo.toml

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,6 @@
1+
# SPDX-License-Identifier: MPL-2.0
2+
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
14
[package]
25
name = "arghda-core"
36
version = "0.1.0"

0 commit comments

Comments
 (0)