From 6005b636dbd5fee6d6cb6d83aa828a6e37aab7e0 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 23 Aug 2026 20:02:13 +0100 Subject: [PATCH 1/2] chore: global textual eradication of Nix and ReScript --- .machine_readable/6a2/META.a2ml | 4 ++-- .machine_readable/rsr-profile.a2ml | 2 +- docs/arghda-spec.adoc | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/.machine_readable/6a2/META.a2ml b/.machine_readable/6a2/META.a2ml index 29bf9c3..882c0bd 100644 --- a/.machine_readable/6a2/META.a2ml +++ b/.machine_readable/6a2/META.a2ml @@ -28,7 +28,7 @@ author = "Jonathan D.A. Jewell (hyperpolymath)" build-tool = "just" container-runtime = "podman" ci-platform = "github-actions" -package-manager = "cargo" # Rust crate; guix/nix dev-shells are a future addition. +package-manager = "cargo" # Rust crate; guix/guix dev-shells are a future addition. [maintenance-axes] scoping-first = true @@ -52,7 +52,7 @@ perfective-source = "axis-1 honest state after corrective/adaptive updates" [axis-3-audit-rules] audit-focus = "systems in place, documentation explains actual state, safety/security accounted for, observed effects reviewed" compliance-focus = "seams/compromises/exception register, bounded exceptions, anti-drift checks" -drift-risk-example = "single exception broadening into policy violation (e.g. ReScript->TypeScript spread)" +drift-risk-example = "single exception broadening into policy violation (e.g. AffineScript->TypeScript spread)" effects-evidence = "benchmark execution/results and maintainer status dialogue/review" [design-rationale] diff --git a/.machine_readable/rsr-profile.a2ml b/.machine_readable/rsr-profile.a2ml index ac23c1e..69da224 100644 --- a/.machine_readable/rsr-profile.a2ml +++ b/.machine_readable/rsr-profile.a2ml @@ -19,6 +19,6 @@ remove = [] # preset capabilities this repo does NOT have no-abi = "language-agnostic engine; no C-ABI/FFI seam, no Idris2 ABI proofs (no abi.ipkg / src/interface/)" no-formal-proofs = "consumes Agda — shells out to agda / agda-unused — but contains no in-tree proofs (no verification/proofs/)" no-container = "ships a CLI binary, not a container image" -no-reproducible-build = "cargo build only for now; guix.scm / flake.nix are a future addition, not present" +no-reproducible-build = "cargo build only for now; guix.scm / flake.guix are a future addition, not present" no-affinescript = "pure Rust; the planned AffineScript visual layer is a separate repo (arghda-studio)" no-governance-tier = "leaf tool; declines the full AUDIT / AFFIRMATION / GOVERNANCE / MAINTAINERS trio" diff --git a/docs/arghda-spec.adoc b/docs/arghda-spec.adoc index dc21728..21df649 100644 --- a/docs/arghda-spec.adoc +++ b/docs/arghda-spec.adoc @@ -47,7 +47,7 @@ CLI, a library API, and a JSON event stream. Runs in CI, standalone, or embedded. `arghda-panll`:: PanLL presentation layer. Gossamer webview + -ReScript panel consuming `arghda-core`'s event stream. Lives in the +AffineScript panel consuming `arghda-core`'s event stream. Lives in the PanLL surface, probably adjacent to Pane-W. Rationale for the split: From f6b3739b003fb020b048362cb5f76055d7036998 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 24 Aug 2026 07:53:39 +0100 Subject: [PATCH 2/2] refactor: migrate repository documentation from Markdown to AsciiDoc --- ARCHITECTURE.adoc | 48 +++++++++++++ ARCHITECTURE.md | 47 ------------ CHANGELOG.adoc | 92 ++++++++++++++++++++++++ CHANGELOG.md | 85 ---------------------- CODE_OF_CONDUCT.adoc | 8 +++ CODE_OF_CONDUCT.md | 7 -- CONTRIBUTING.adoc | 34 +++++++++ CONTRIBUTING.md | 33 --------- GOVERNANCE.adoc | 60 ++++++++++++++++ GOVERNANCE.md | 60 ---------------- README.adoc | 166 +++++++++++++++++++++++++++++++++++++++++++ README.md | 152 --------------------------------------- SECURITY.adoc | 31 ++++++++ SECURITY.md | 32 --------- 14 files changed, 439 insertions(+), 416 deletions(-) create mode 100644 ARCHITECTURE.adoc delete mode 100644 ARCHITECTURE.md create mode 100644 CHANGELOG.adoc delete mode 100644 CHANGELOG.md create mode 100644 CODE_OF_CONDUCT.adoc delete mode 100644 CODE_OF_CONDUCT.md create mode 100644 CONTRIBUTING.adoc delete mode 100644 CONTRIBUTING.md create mode 100644 GOVERNANCE.adoc delete mode 100644 GOVERNANCE.md create mode 100644 README.adoc delete mode 100644 README.md create mode 100644 SECURITY.adoc delete mode 100644 SECURITY.md diff --git a/ARCHITECTURE.adoc b/ARCHITECTURE.adoc new file mode 100644 index 0000000..1c0a7a6 --- /dev/null +++ b/ARCHITECTURE.adoc @@ -0,0 +1,48 @@ +== Architecture + +=== Overview + +This repository follows a modular, maintainable architecture designed +for clarity, scalability, and long-term sustainability. + +=== Directory Structure + +.... +. +├── src/ # Source code +├── tests/ # Test suites +├── docs/ # Documentation +├── scripts/ # Utility scripts +├── config/ # Configuration files +├── LICENSE # License file +├── LICENSES/ # Full license texts +└── README.adoc # Project documentation +.... + +=== Design Principles + +* *Separation of Concerns*: Each module has a single responsibility +* *Testability*: Code is written to be easily testable +* *Documentation*: All public APIs are documented +* *Configuration*: Environment-specific settings are externalized + +=== Dependencies + +* External dependencies are minimized and clearly declared +* Version pinning is used for reproducibility + +=== Security Considerations + +* Sensitive data is never committed to the repository +* Secrets are managed through environment variables or secure vaults +* Regular dependency audits are performed + +=== Maintainability + +* Code follows consistent style guidelines +* Pull requests require review and CI checks +* Issues and discussions are tracked transparently + +''''' + +_Last updated: 2026-07-18_ diff --git a/ARCHITECTURE.md b/ARCHITECTURE.md deleted file mode 100644 index 607e3d8..0000000 --- a/ARCHITECTURE.md +++ /dev/null @@ -1,47 +0,0 @@ -# Architecture - -## Overview - -This repository follows a modular, maintainable architecture designed for clarity, scalability, and long-term sustainability. - -## Directory Structure - -``` -. -├── src/ # Source code -├── tests/ # Test suites -├── docs/ # Documentation -├── scripts/ # Utility scripts -├── config/ # Configuration files -├── LICENSE # License file -├── LICENSES/ # Full license texts -└── README.adoc # Project documentation -``` - -## Design Principles - -- **Separation of Concerns**: Each module has a single responsibility -- **Testability**: Code is written to be easily testable -- **Documentation**: All public APIs are documented -- **Configuration**: Environment-specific settings are externalized - -## Dependencies - -- External dependencies are minimized and clearly declared -- Version pinning is used for reproducibility - -## Security Considerations - -- Sensitive data is never committed to the repository -- Secrets are managed through environment variables or secure vaults -- Regular dependency audits are performed - -## Maintainability - -- Code follows consistent style guidelines -- Pull requests require review and CI checks -- Issues and discussions are tracked transparently - ---- - -*Last updated: 2026-07-18* diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc new file mode 100644 index 0000000..2f466e2 --- /dev/null +++ b/CHANGELOG.adoc @@ -0,0 +1,92 @@ +== Changelog + +All notable changes to arghda-core are documented here. The format +follows https://keepachangelog.com/[Keep a Changelog], and this project +adheres to https://semver.org/[Semantic Versioning]. + +=== [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. +* 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 + +* `+dag+` command emitting the dependency-DAG JSON contract (nodes with +lint-derived status, import edges, and a `+blocked+` list covering +self-blocks and prerequisite-blocks). +* `+check+` command: Agda typecheck fused with the lint report +(`+proven-eligible+` / `+rejected+` / `+agda-unavailable+`); degrades +gracefully when `+agda+` is absent. +* Workspace state machine — `+claim+` / `+promote+` / `+reject+` / +`+requeue+` / `+invalidate+` as validated file moves, each logged to +`+.arghda/events.jsonl+`; plus `+events+` to replay the log. +* First-class import graph (`+graph+` module) with multi-root +reachability: orphan detection is the union of auto-discovered +`+All.agda+` / `+Smoke.agda+` CI roots (or `+--entry+`, repeatable). +* Lint rules: `+unjustified-postulate+` (hard-block), `+escape-hatch+` +(warn: `+TERMINATING+`-family pragmas + `+believe_me+` / +`+primTrustMe+`), `+tab-mix+` (warn). +* `+unpinned-headline+` (warn): flags a top-level theorem whose name +matches the headline pattern but is not pinned in any `+Smoke.agda+` via +a `+using ( … )+` clause. The pattern is operator-configurable via +`+--headline-pattern +` on `+scan+` / `+dag+` (default +`+^[a-z][A-Za-z0-9-]*$+`, per the spec). Detects top-level (column-0) +signatures only, which gives the export-only filter for free; tolerant +of multi-line `+using+` lists; self-skips when no `+Smoke.agda+` is in +scope. +* `+unused-import+` (warn): re-emits the findings of the external +`+agda-unused+` tool (spec §Linter rules). Opt-in behind +`+scan --unused+`; runs `+agda-unused+` per file in local mode with +`+LC_ALL=C.UTF-8+`, parses its `+--json+` output, and re-emits each +finding as an `+unused-import+` warning attributed to the file. Degrades +gracefully (with a note) when `+agda-unused+` is not on `+PATH+`, +mirroring how `+check+` tolerates a missing `+agda+`. +* `+.arghda/config.toml+` operator configuration (the spec’s +open-question surface): `+scan+` / `+dag+` read a +`+[lint] headline_pattern+` override from `+/.arghda/config.toml+` +(or an explicit `+--config +`). Precedence is built-in default < +`+config.toml+` < CLI `+--headline-pattern+`. Missing file ⇒ defaults; +unknown keys are rejected so typos surface. +* DAG `+headlines+` field: each `+dag+` node now carries the sorted, +deduped list of top-level headline theorem names it declares (the spec’s +per-node `+headlines+` array), extracted with the same logic as +`+unpinned-headline+` and honouring the configured headline pattern. +Completes the v0 DAG schema. +* RSR scaffolding: `+.machine_readable/6a2/+` artefacts, +`+0-AI-MANIFEST.a2ml+`, `+Justfile+`, `+.well-known/+`, and +community-health files. +* Content-hash invalidation of `+proven+`: promotion records a SHA-256 +of the file in `+.arghda/hashes.json+`; the `+stale+` command reports +proven files edited since promotion, and `+stale --invalidate+` moves +them back to inbox (the `+proven -> inbox+` invalidation). +Dependency-free SHA-256, pinned against the NIST test vectors. + +==== Notes + +* Verified against Agda 2.6.3 and dogfooded on the echo-types corpus +(193 modules, 903 import edges; the known `+VarianceGate.agda+` orphan +and the out-of-cone files are surfaced correctly). + +=== [0.1.0] — 2026-05-30 + +* Initial extraction from echo-types: workspace scaffold, filesystem +watcher, `+missing-safe-pragma+` + `+orphan-module+` lints, and the +`+scan+` CLI. diff --git a/CHANGELOG.md b/CHANGELOG.md deleted file mode 100644 index 818ba11..0000000 --- a/CHANGELOG.md +++ /dev/null @@ -1,85 +0,0 @@ - -# Changelog - -All notable changes to arghda-core are documented here. The format follows -[Keep a Changelog](https://keepachangelog.com/), and this project adheres to -[Semantic Versioning](https://semver.org/). - -## [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. -- 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 - -- `dag` command emitting the dependency-DAG JSON contract (nodes with - lint-derived status, import edges, and a `blocked` list covering - self-blocks and prerequisite-blocks). -- `check` command: Agda typecheck fused with the lint report - (`proven-eligible` / `rejected` / `agda-unavailable`); degrades gracefully - when `agda` is absent. -- Workspace state machine — `claim` / `promote` / `reject` / `requeue` / - `invalidate` as validated file moves, each logged to - `.arghda/events.jsonl`; plus `events` to replay the log. -- First-class import graph (`graph` module) with multi-root reachability: - orphan detection is the union of auto-discovered `All.agda` / `Smoke.agda` - CI roots (or `--entry`, repeatable). -- Lint rules: `unjustified-postulate` (hard-block), `escape-hatch` (warn: - `TERMINATING`-family pragmas + `believe_me` / `primTrustMe`), `tab-mix` - (warn). -- `unpinned-headline` (warn): flags a top-level theorem whose name matches - the headline pattern but is not pinned in any `Smoke.agda` via a - `using ( … )` clause. The pattern is operator-configurable via - `--headline-pattern ` on `scan` / `dag` (default - `^[a-z][A-Za-z0-9-]*$`, per the spec). Detects top-level (column-0) - signatures only, which gives the export-only filter for free; tolerant of - multi-line `using` lists; self-skips when no `Smoke.agda` is in scope. -- `unused-import` (warn): re-emits the findings of the external `agda-unused` - tool (spec §Linter rules). Opt-in behind `scan --unused`; runs `agda-unused` - per file in local mode with `LC_ALL=C.UTF-8`, parses its `--json` output, - and re-emits each finding as an `unused-import` warning attributed to the - file. Degrades gracefully (with a note) when `agda-unused` is not on `PATH`, - mirroring how `check` tolerates a missing `agda`. -- `.arghda/config.toml` operator configuration (the spec's open-question - surface): `scan` / `dag` read a `[lint] headline_pattern` override from - `/.arghda/config.toml` (or an explicit `--config `). Precedence - is built-in default < `config.toml` < CLI `--headline-pattern`. Missing file - ⇒ defaults; unknown keys are rejected so typos surface. -- DAG `headlines` field: each `dag` node now carries the sorted, deduped list - of top-level headline theorem names it declares (the spec's per-node - `headlines` array), extracted with the same logic as `unpinned-headline` and - honouring the configured headline pattern. Completes the v0 DAG schema. -- RSR scaffolding: `.machine_readable/6a2/` artefacts, `0-AI-MANIFEST.a2ml`, - `Justfile`, `.well-known/`, and community-health files. -- Content-hash invalidation of `proven`: promotion records a SHA-256 of the - file in `.arghda/hashes.json`; the `stale` command reports proven files - edited since promotion, and `stale --invalidate` moves them back to inbox - (the `proven -> inbox` invalidation). Dependency-free SHA-256, pinned - against the NIST test vectors. - -### Notes - -- Verified against Agda 2.6.3 and dogfooded on the echo-types corpus - (193 modules, 903 import edges; the known `VarianceGate.agda` orphan and - the out-of-cone files are surfaced correctly). - -## [0.1.0] — 2026-05-30 - -- Initial extraction from echo-types: workspace scaffold, filesystem - watcher, `missing-safe-pragma` + `orphan-module` lints, and the `scan` CLI. diff --git a/CODE_OF_CONDUCT.adoc b/CODE_OF_CONDUCT.adoc new file mode 100644 index 0000000..a672ecc --- /dev/null +++ b/CODE_OF_CONDUCT.adoc @@ -0,0 +1,8 @@ +== Code of Conduct + +This project follows the +https://www.contributor-covenant.org/version/2/1/code_of_conduct/[Contributor +Covenant 2.1]. + +Reports go to `+j.d.a.jewell@open.ac.uk+`. Reports are confidential by +default. diff --git a/CODE_OF_CONDUCT.md b/CODE_OF_CONDUCT.md deleted file mode 100644 index 999b538..0000000 --- a/CODE_OF_CONDUCT.md +++ /dev/null @@ -1,7 +0,0 @@ - - -# 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/CONTRIBUTING.adoc b/CONTRIBUTING.adoc new file mode 100644 index 0000000..03c0630 --- /dev/null +++ b/CONTRIBUTING.adoc @@ -0,0 +1,34 @@ +== Contributing to arghda-core + +arghda-core is the Rust engine for the arghda proof-workspace tool. + +=== Ground rules + +* *arghda never proves.* Agda (directly, or via echidna) proves; arghda +organises, lints, and emits the DAG / event JSON. Don’t add a prover or +claim a result Agda didn’t return. +* *Licence:* MPL-2.0. New files carry an SPDX header from birth. Don’t +bulk-rewrite existing headers. +* *Green gate.* Every change keeps `+just check+` (`+cargo fmt --check+` ++ `+clippy -D warnings+` + `+build+` + `+test+`) green, and adds tests +for new behaviour. + +=== Workflow + +[arabic] +. Branch from `+main+`. +. Make the change; `+just check+` must pass. +. Open a PR. CI runs build / test / clippy / fmt. + +=== Layout + +* `+src/+` — the library plus the thin `+arghda+` CLI (`+src/main.rs+`). +* `+src/lint/+` — one module per lint rule (`+LintRule+` trait is the +extension point). +* `+src/graph.rs+` — the first-class Agda import graph. +* `+tests/+` — integration tests; `+tests/fixtures/+` — tiny Agda +fixtures. +* `+docs/+` — `+.adoc+` spec (`+arghda-spec.adoc+`) and vision/roadmap +(`+arghda-vision.adoc+`). +* `+.machine_readable/6a2/+` — RSR machine-readable state; update +`+STATE.a2ml+` as work lands. diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md deleted file mode 100644 index 8ad261f..0000000 --- a/CONTRIBUTING.md +++ /dev/null @@ -1,33 +0,0 @@ - -# Contributing to arghda-core - -arghda-core is the Rust engine for the arghda proof-workspace tool. - -## Ground rules - -- **arghda never proves.** Agda (directly, or via echidna) proves; arghda - organises, lints, and emits the DAG / event JSON. Don't add a prover or - claim a result Agda didn't return. -- **Licence:** MPL-2.0. New files carry an SPDX header from birth. Don't - bulk-rewrite existing headers. -- **Green gate.** Every change keeps `just check` - (`cargo fmt --check` + `clippy -D warnings` + `build` + `test`) green, - and adds tests for new behaviour. - -## Workflow - -1. Branch from `main`. -2. Make the change; `just check` must pass. -3. Open a PR. CI runs build / test / clippy / fmt. - -## Layout - -- `src/` — the library plus the thin `arghda` CLI (`src/main.rs`). -- `src/lint/` — one module per lint rule (`LintRule` trait is the - extension point). -- `src/graph.rs` — the first-class Agda import graph. -- `tests/` — integration tests; `tests/fixtures/` — tiny Agda fixtures. -- `docs/` — `.adoc` spec (`arghda-spec.adoc`) and vision/roadmap - (`arghda-vision.adoc`). -- `.machine_readable/6a2/` — RSR machine-readable state; update - `STATE.a2ml` as work lands. diff --git a/GOVERNANCE.adoc b/GOVERNANCE.adoc new file mode 100644 index 0000000..9b836fb --- /dev/null +++ b/GOVERNANCE.adoc @@ -0,0 +1,60 @@ +== Governance + +=== Overview + +This project is governed by the following principles and structures to +ensure transparent, inclusive, and effective decision-making. + +=== Roles and Responsibilities + +==== Maintainers + +Maintainers are responsible for: - Reviewing and merging pull requests - +Managing releases and versioning - Ensuring code quality and standards - +Triaging issues and bug reports - Community engagement and support + +==== Contributors + +Contributors are expected to: - Follow the code of conduct - Submit +well-documented pull requests - Write tests for new functionality - +Maintain existing tests - Update documentation as needed + +=== Decision Making + +==== Minor Changes + +* Can be made by any maintainer +* Include bug fixes, documentation updates, dependency updates + +==== Major Changes + +* Require discussion in issues or pull requests +* Include new features, architectural changes, API changes +* Need approval from at least 2 maintainers + +==== Breaking Changes + +* Require RFC (Request for Comments) process +* Need approval from majority of maintainers +* Must include migration guide + +=== Code of Conduct + +All participants are expected to follow our Code of Conduct. Violations +can be reported to the maintainers. + +=== Communication + +* *Issues*: For bug reports and feature requests +* *Discussions*: For questions and general discussion +* *Pull Requests*: For code contributions + +=== Licensing + +All contributions are made under the terms of the repository’s LICENSE +file. By submitting a pull request, you agree to license your +contributions accordingly. + +''''' + +_Last updated: 2026-07-18_ diff --git a/GOVERNANCE.md b/GOVERNANCE.md deleted file mode 100644 index e27364c..0000000 --- a/GOVERNANCE.md +++ /dev/null @@ -1,60 +0,0 @@ -# Governance - -## Overview - -This project is governed by the following principles and structures to ensure transparent, inclusive, and effective decision-making. - -## Roles and Responsibilities - -### Maintainers - -Maintainers are responsible for: -- Reviewing and merging pull requests -- Managing releases and versioning -- Ensuring code quality and standards -- Triaging issues and bug reports -- Community engagement and support - -### Contributors - -Contributors are expected to: -- Follow the code of conduct -- Submit well-documented pull requests -- Write tests for new functionality -- Maintain existing tests -- Update documentation as needed - -## Decision Making - -### Minor Changes -- Can be made by any maintainer -- Include bug fixes, documentation updates, dependency updates - -### Major Changes -- Require discussion in issues or pull requests -- Include new features, architectural changes, API changes -- Need approval from at least 2 maintainers - -### Breaking Changes -- Require RFC (Request for Comments) process -- Need approval from majority of maintainers -- Must include migration guide - -## Code of Conduct - -All participants are expected to follow our Code of Conduct. Violations can be reported to the maintainers. - -## Communication - -- **Issues**: For bug reports and feature requests -- **Discussions**: For questions and general discussion -- **Pull Requests**: For code contributions - -## Licensing - -All contributions are made under the terms of the repository's LICENSE file. -By submitting a pull request, you agree to license your contributions accordingly. - ---- - -*Last updated: 2026-07-18* diff --git a/README.adoc b/README.adoc new file mode 100644 index 0000000..2ad5aa4 --- /dev/null +++ b/README.adoc @@ -0,0 +1,166 @@ +https://github.com/sponsors/hyperpolymath[image:https://img.shields.io/badge/Sponsor-%E2%9D%A4-pink?logo=github[Sponsor]] +https://www.mozilla.org/MPL/2.0/[image:https://img.shields.io/badge/License-MPL_2.0-blue.svg[License]] + +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+`. + +[width="100%",cols="50%,50%",options="header",] +|=== +|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 LICENSE); prose +documentation is `+CC-BY-SA-4.0+`, per the +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/README.md b/README.md deleted file mode 100644 index bf770c2..0000000 --- a/README.md +++ /dev/null @@ -1,152 +0,0 @@ - - -[![Sponsor](https://img.shields.io/badge/Sponsor-%E2%9D%A4-pink?logo=github)](https://github.com/sponsors/hyperpolymath) -[![License](https://img.shields.io/badge/License-MPL_2.0-blue.svg)](https://www.mozilla.org/MPL/2.0/) - -Lightweight proof-workspace manager for Agda — the language-agnostic -engine half of **arghda**. 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). - -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 -[`STATE.a2ml`](.machine_readable/6a2/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 - [`agda-unused`](https://github.com/msuperdock/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`. - -| 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. - -```toml -[lint] -headline_pattern = "^[a-z][A-Za-z0-9-]*$" -``` - -# Build - -```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 - -```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 [hyperpolymath ecosystem](https://github.com/hyperpolymath). -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: - -- [echo-types](https://github.com/hyperpolymath/echo-types) — the Agda - library that motivated arghda’s design (not a build dependency). - -- [absolute-zero](https://github.com/hyperpolymath/absolute-zero) — a - sister Agda library under the same `--safe` `--without-K` discipline. - -# Machine-readable - -Per the Rhodium Standard, structured project metadata lives under -[`.machine_readable/6a2/`](.machine_readable/6a2/) — `STATE`, `META`, -`ECOSYSTEM`, `AGENTIC`, `NEUROSYM`, `PLAYBOOK` in A2ML — with -[`0-AI-MANIFEST.a2ml`](0-AI-MANIFEST.a2ml) as the AI entry point and -[`EXPLAINME.adoc`](EXPLAINME.adoc) as the orientation pointer. - -# Licence - -Code, configuration and scripts are `MPL-2.0` (see [LICENSE](LICENSE)); -prose documentation is `CC-BY-SA-4.0`, per the [hyperpolymath licence -policy](https://github.com/hyperpolymath/standards) (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 -([`licensing-policy.toml`](.machine_readable/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.adoc b/SECURITY.adoc new file mode 100644 index 0000000..cd052a7 --- /dev/null +++ b/SECURITY.adoc @@ -0,0 +1,31 @@ +== Security Policy + +=== Supported versions + +arghda-core is alpha (0.1.x). Only the latest `+main+` is supported. + +=== Reporting a vulnerability + +Please report suspected security issues *privately* to +*j.d.a.jewell@open.ac.uk*. Do not open a public issue for a suspected +vulnerability. + +Where possible, include: + +* a description of the issue and its impact; +* steps or a proof-of-concept to reproduce; +* the commit or version affected. + +=== Response + +We aim to acknowledge a report within 7 days and to agree a disclosure +timeline with the reporter. + +=== Scope + +This policy covers the arghda-core engine. arghda reads `+.agda+` files +as text and shells out to the configured `+agda+` (and, in future, +`+agda-unused+`) binary on files you point it at; it never executes +proof code itself. Reports about untrusted-input handling — path +traversal, command construction, denial of service on malformed input — +are especially welcome. diff --git a/SECURITY.md b/SECURITY.md deleted file mode 100644 index 9aa8ee8..0000000 --- a/SECURITY.md +++ /dev/null @@ -1,32 +0,0 @@ - -# Security Policy - -## Supported versions - -arghda-core is alpha (0.1.x). Only the latest `main` is supported. - -## Reporting a vulnerability - -Please report suspected security issues **privately** to -**j.d.a.jewell@open.ac.uk**. Do not open a public issue for a suspected -vulnerability. - -Where possible, include: - -- a description of the issue and its impact; -- steps or a proof-of-concept to reproduce; -- the commit or version affected. - -## Response - -We aim to acknowledge a report within 7 days and to agree a disclosure -timeline with the reporter. - -## Scope - -This policy covers the arghda-core engine. arghda reads `.agda` files as -text and shells out to the configured `agda` (and, in future, -`agda-unused`) binary on files you point it at; it never executes proof -code itself. Reports about untrusted-input handling — path traversal, -command construction, denial of service on malformed input — are -especially welcome.