From 971a689f80354652b39b59bacc7bb5f8b3e4105b Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 22 Apr 2026 06:34:11 +0000 Subject: [PATCH 1/7] Add CLAUDE.md ecosystem context for session bootstrapping Documents adjacent hyperpolymath / PanLL projects so every session starts with the same mental map instead of being re-explained. Includes TODO placeholders for Burble, VQL-UT, and the Groove protocol pending operator-supplied descriptions. https://claude.ai/code/session_01DDGQFBtAT9JdRwmu25QzC2 --- CLAUDE.md | 51 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 51 insertions(+) create mode 100644 CLAUDE.md diff --git a/CLAUDE.md b/CLAUDE.md new file mode 100644 index 0000000..f085b74 --- /dev/null +++ b/CLAUDE.md @@ -0,0 +1,51 @@ +# Ecosystem context + +This repo (echo-types) is one node in the hyperpolymath / PanLL ecosystem. +Adjacent projects, in one line each, for session bootstrapping: + +- PanLL — three-pane cognitive-relief HTI; Ambient/Symbolic/Neural/World panes. + https://github.com/hyperpolymath/panll +- Gossamer — Zig + WebKitGTK webview shell used by PanLL (~5 MB binary). +- Burble — TODO: one-line description from operator. +- Echidna (hyperpolymath) — planned high-assurance interface verification. + NOT the Ethereum fuzzer of the same name. +- VeriSim / VeriSimDB — identity-state capture with filesystem fallback. +- VQL-UT — TODO: one-line description from operator. +- Groove protocol — TODO: one-line description from operator; + see GROOVE_PANLL_RESEARCH_SUMMARY.md in panll. +- ArghDA (planned) — lightweight proof-workspace manager for Agda; + triage folders (inbox → working → proven/rejected), linter, DAG view. + Split as `arghda-core` (language-agnostic engine) + `arghda-panll` + (Gossamer/ReScript presentation). See docs/buchholz-plan.adoc appendix + for the motivating proof pipeline. + +# This repo + +echo-types — constructive Agda formalization of fiber-based structured loss +("echo types"). Gated identity-claim development per roadmap-gates.adoc. + +Current workstream: **E (ordinal-notation / Buchholz collapsing layer)** +per docs/buchholz-plan.adoc. Aims to land a proof-theoretic collapsing-function +target — first credible milestone Bachmann–Howard (ψ₀(Ω_ω)), stretch +target ψ(Ω_Ω) ≈ TFBO. + +First landed proof: `C-monotone` in proofs/agda/Ordinal/Closure.agda. +Next planned: E3 CNF trichotomy, then E4 pedagogical `psi-notin-C`. + +# Build + +``` +cd /home/user/echo-types +agda -i proofs/agda proofs/agda/All.agda +for f in proofs/agda/*.agda proofs/agda/Ordinal/*.agda proofs/agda/Ordinal/Buchholz/*.agda; do + [ -f "$f" ] && agda -i proofs/agda "$f" +done +``` + +# Working rules in this repo + +- No postulates unless explicitly isolated and justified. +- `--safe --without-K` throughout. +- Every edit ends with an Agda compile command and captured output. +- Every headline theorem must be pinned in Smoke.agda via `using` clause. +- Branch for ordinal-notation work: claude/add-ordinal-notation-layer-9qhSf. From b6e0b5705dd67c73d8b755036b10521c08b84b5f Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 22 Apr 2026 06:36:06 +0000 Subject: [PATCH 2/7] Fill in Burble, VCL-UT, Groove ecosystem entries in CLAUDE.md Descriptions sourced from the panll repo and the hyperpolymath org's public project docs. The operator-supplied "VQL-UT" name has been recorded as likely VCL-UT (now VCL-total), with a reconcile-spelling note rather than a silent correction. https://claude.ai/code/session_01DDGQFBtAT9JdRwmu25QzC2 --- CLAUDE.md | 20 ++++++++++++++++---- 1 file changed, 16 insertions(+), 4 deletions(-) diff --git a/CLAUDE.md b/CLAUDE.md index f085b74..9810557 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -6,13 +6,25 @@ Adjacent projects, in one line each, for session bootstrapping: - PanLL — three-pane cognitive-relief HTI; Ambient/Symbolic/Neural/World panes. https://github.com/hyperpolymath/panll - Gossamer — Zig + WebKitGTK webview shell used by PanLL (~5 MB binary). -- Burble — TODO: one-line description from operator. +- Burble — self-hostable voice-communications platform; Zig-based SIMD + audio, IEEE 1588 PTP clock sync, sub-second room joining, browser-based + (no downloads / no accounts), configurable topology from single-server + to fully distributed mesh. In PanLL, used for team replication via + broadcast and as a switchable service alongside Gossamer. - Echidna (hyperpolymath) — planned high-assurance interface verification. NOT the Ethereum fuzzer of the same name. - VeriSim / VeriSimDB — identity-state capture with filesystem fallback. -- VQL-UT — TODO: one-line description from operator. -- Groove protocol — TODO: one-line description from operator; - see GROOVE_PANLL_RESEARCH_SUMMARY.md in panll. +- VCL-UT (now VCL-total) — next-generation interaction language for + VeriSim; designed to satisfy all 10 levels of type safety when + proposing, inspecting, and verifying operations in a consonance engine + (rather than querying a passive database). NOTE: operator wrote + "VQL-UT" — confirm whether this is the same project under a different + spelling or a distinct one. +- Groove protocol — HTTP-based service-discovery mechanism; lets + capabilities across the hyperpolymath ecosystem announce themselves + for automatic detection and integration (e.g. discipline-specific + analyzers becoming visible to PanLL without manual wiring). + See GROOVE_PANLL_RESEARCH_SUMMARY.md in panll. - ArghDA (planned) — lightweight proof-workspace manager for Agda; triage folders (inbox → working → proven/rejected), linter, DAG view. Split as `arghda-core` (language-agnostic engine) + `arghda-panll` From 63d7ee9003e68b041b6b87c23a93e75bb014c56f Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 22 Apr 2026 06:36:32 +0000 Subject: [PATCH 3/7] Drop VCL-UT spelling reconcile note (confirmed by operator) https://claude.ai/code/session_01DDGQFBtAT9JdRwmu25QzC2 --- CLAUDE.md | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/CLAUDE.md b/CLAUDE.md index 9810557..851ecd3 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -17,9 +17,7 @@ Adjacent projects, in one line each, for session bootstrapping: - VCL-UT (now VCL-total) — next-generation interaction language for VeriSim; designed to satisfy all 10 levels of type safety when proposing, inspecting, and verifying operations in a consonance engine - (rather than querying a passive database). NOTE: operator wrote - "VQL-UT" — confirm whether this is the same project under a different - spelling or a distinct one. + (rather than querying a passive database). - Groove protocol — HTTP-based service-discovery mechanism; lets capabilities across the hyperpolymath ecosystem announce themselves for automatic detection and integration (e.g. discipline-specific From 3847c6434c723b620cb117aa6651809aa8ee6c9a Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 22 Apr 2026 06:37:35 +0000 Subject: [PATCH 4/7] Record ephapax as hyperpolymath ecosystem member Linear-type WebAssembly language at hyperpolymath/ephapax. Added as a separate entry; the Echidna-vs-ephapax question (whether ephapax fills the Echidna role) remains open. https://claude.ai/code/session_01DDGQFBtAT9JdRwmu25QzC2 --- CLAUDE.md | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/CLAUDE.md b/CLAUDE.md index 851ecd3..bda3c44 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -12,7 +12,10 @@ Adjacent projects, in one line each, for session bootstrapping: to fully distributed mesh. In PanLL, used for team replication via broadcast and as a switchable service alongside Gossamer. - Echidna (hyperpolymath) — planned high-assurance interface verification. - NOT the Ethereum fuzzer of the same name. + NOT the Ethereum fuzzer of the same name. Exact repo still to confirm. +- Ephapax — programming language with a linear type system guaranteeing + memory safety for WebAssembly (compile-time "no use-after-free / no + memory leaks"). https://github.com/hyperpolymath/ephapax - VeriSim / VeriSimDB — identity-state capture with filesystem fallback. - VCL-UT (now VCL-total) — next-generation interaction language for VeriSim; designed to satisfy all 10 levels of type safety when From 093c0b53bdb1cabf4464a8e71160a2706f21b3d9 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 22 Apr 2026 06:39:10 +0000 Subject: [PATCH 5/7] Add echo-types one-liner to ecosystem list Mirrors the bullet format used for every other hyperpolymath member so future sessions see echo-types alongside its siblings rather than only in the "this repo" section further down. https://claude.ai/code/session_01DDGQFBtAT9JdRwmu25QzC2 --- CLAUDE.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/CLAUDE.md b/CLAUDE.md index bda3c44..05665d9 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -3,6 +3,11 @@ This repo (echo-types) is one node in the hyperpolymath / PanLL ecosystem. Adjacent projects, in one line each, for session bootstrapping: +- echo-types — constructive Agda formalization of fiber-based structured + loss ("echo types"); `Echo f y := Σ (x : A) , (f x ≡ y)`. Gated + identity-claim development; `--safe --without-K` throughout. Current + workstream: E (ordinal-notation / Buchholz collapsing layer). + https://github.com/hyperpolymath/echo-types - PanLL — three-pane cognitive-relief HTI; Ambient/Symbolic/Neural/World panes. https://github.com/hyperpolymath/panll - Gossamer — Zig + WebKitGTK webview shell used by PanLL (~5 MB binary). From 2a8d9e8a50fb18a2ac07221ea52e7521e3b8a6cb Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 22 Apr 2026 11:41:26 +0000 Subject: [PATCH 6/7] Add ArghDA MVP design spec Parks the proof-workspace-manager design in-tree until ArghDA gets its own repo. Covers: core/panll split, four-state triage file-move machine (inbox/working/proven/rejected), Agda-first linter rules targeting the silent-failure class, DAG JSON schema, first-sprint ordering, and acceptance criteria against echo-types itself as the seed workspace. https://claude.ai/code/session_01DDGQFBtAT9JdRwmu25QzC2 --- docs/arghda-spec.adoc | 218 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 218 insertions(+) create mode 100644 docs/arghda-spec.adoc diff --git a/docs/arghda-spec.adoc b/docs/arghda-spec.adoc new file mode 100644 index 0000000..4f94337 --- /dev/null +++ b/docs/arghda-spec.adoc @@ -0,0 +1,218 @@ += ArghDA MVP Specification +:toc: macro +:toclevels: 2 + +toc::[] + +== Purpose + +ArghDA is a lightweight proof-workspace manager. Initial target: +Agda. It exists to close a specific user-experience gap that +`agda-mode` and `agda-language-server` do not: making the +_lifecycle_ of a proof (inbox → working → proven | rejected) a +first-class, visible object, with a thin linter that catches the +silent-failure class _before_ the typechecker. + +Scope discipline: small tool, narrow job. Not a proof assistant, +not a replacement for `agda-mode`, not a tactic framework. + +== Motivation + +From echo-types sessions (see `docs/buchholz-plan.adoc`), the +operator repeatedly hit a specific failure mode: + +* a proof file exists, looks like it typechecked, but is missing + `--safe` / `--without-K`, or is not imported from `All.agda`, + or is not pinned in `Smoke.agda` +* the "did it really work?" question is answered only by running + the whole suite, which is slow and emotionally punishing +* there is no visible pipeline: no inbox, no "in-progress", no + "proven" tag; just a flat directory of `.agda` files + +The existing ecosystem (see ArghDA scout report: `coq-lsp`, +`VSCoq`, `Alectryon`, `LeanInk`, `Mathlib stats`, `Isabelle/jEdit +PIDE`, `agda-language-server`, `agda-unused`) gives excellent +per-file UX and some library-level dependency views, but nobody +treats proofs as _items flowing through pipeline stages_. That is +the novel contribution. + +== Split + +Two layers, developed and published as two packages: + +`arghda-core`:: Language-agnostic engine. Rust. No UI. Exposes a +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 +PanLL surface, probably adjacent to Pane-W. + +Rationale for the split: + +* Proof triage is useful outside PanLL (students, CI, large collabs). +* Testing `arghda-core` doesn't require booting PanLL. +* PanLL gains a polished dependency rather than an internal subsystem. +* Matches PanLL's existing pattern with `panll_beam`. + +== State machine (core) + +Four states, implemented as four directories under a workspace root: + +[source] +---- +/ + inbox/ -- new or returning proof files + working/ -- operator has picked this up + proven/ -- typecheck + lint clean + rejected/ -- typecheck failed, or lint-block, or manual reject +---- + +Transitions are _file moves_. This keeps the ground truth on disk, +makes recovery obvious (`mv` it back), and survives ArghDA crashing. + +Transition rules: + +[cols="1,2,3"] +|=== +| From | To | Trigger + +| inbox | working | operator claim (explicit) +| working | proven | typecheck clean AND lint clean +| working | rejected | typecheck failed OR lint-hard-block +| rejected | inbox | manual re-queue +| proven | inbox | upstream change invalidates (see DAG below) +|=== + +Every transition emits a JSON event to a rolling log under +`/.arghda/events.jsonl`. + +== Linter rules (Agda, v0) + +The linter targets the _silent-failure_ class — cases where Agda +appears to succeed but the file is not actually in the verified +suite. Rules, each emitting a structured diagnostic: + +* `missing-safe-pragma` — file lacks `{-# OPTIONS --safe --without-K #-}` +* `missing-without-k` — `--safe` without `--without-K` (or vice versa) +* `orphan-module` — module not imported (transitively) from `All.agda` +* `unpinned-headline` — module exports a theorem matching a + headline-naming pattern (operator-configurable regex) but the name + is not pinned in `Smoke.agda` via a `using` clause +* `unjustified-postulate` — `postulate` block without an adjacent + comment line starting with `-- JUSTIFY:` +* `unused-import` — shell out to `agda-unused` and re-emit findings +* `tab-mix` — file mixes tabs and spaces at line start + +Severity: `hard-block` (forbids `working → proven`) vs `warn` +(surfaced but non-blocking). Default: `missing-safe-pragma`, +`orphan-module`, `unjustified-postulate` are hard-block; the rest +are warn. + +Non-goals for v0: semantic linting, redundancy detection, +style-guide enforcement beyond whitespace. + +== DAG JSON schema (v0) + +Emitted by `arghda-core dag` as a single JSON document. Consumable by +the PanLL panel, a static HTML viewer, or third-party tools. + +[source,json] +---- +{ + "version": "0.1", + "workspace": "/path/to/workspace", + "generated_at": "ISO-8601", + "nodes": [ + { + "id": "Ordinal.Closure", + "file": "proofs/agda/Ordinal/Closure.agda", + "status": "proven", + "lint": { "hard_block": [], "warn": [] }, + "headlines": ["C-monotone"] + } + ], + "edges": [ + { "from": "Ordinal.Closure", "to": "Ordinal.Base", "kind": "imports" } + ], + "blocked": [ + { + "node": "Ordinal.Buchholz.Psi", + "blocked_by": ["Ordinal.Buchholz.Closure"], + "reason": "prereq not proven" + } + ] +} +---- + +Renderer is a separate concern; the panel consumes this verbatim. + +== Integration points + +* **LSP** (coq-lsp pattern) — per-file editor feedback. +* **PIDE async model** (Isabelle) — asynchronous document state + for the "checking now" sub-state within `working`. +* **`agda --only-scope-checking`** — cheap pre-pass for quick + syntactic / import validation before full typecheck. +* **`agda-unused`** — shell out; re-emit diagnostics in the + ArghDA diagnostic format. +* **Alectryon-style rendering** (future) — static HTML render of + proof states as a by-product of `proven` transition. + +== Non-goals (MVP) + +* Tactic language. +* Writing proofs for the operator. +* IDE replacement. +* Multi-prover support (Coq/Lean/Isabelle postponed to v0.2). +* Distributed execution. A single workspace, a single machine. + +== First sprint (v0.1) + +Ordered by unblock-value: + +. `arghda-core` Rust crate skeleton; `Workspace::open(path)` API. +. Filesystem watcher over `inbox/` and `working/` using `notify`. +. Two linter rules: `missing-safe-pragma`, `orphan-module`. +. `arghda-core check ` command: runs agda, captures exit code, + emits a `LintReport` JSON. +. `arghda-core promote ` / `arghda-core reject `: + the state-machine CLI. +. `arghda-core dag` emitting the schema above for the current + workspace. +. Minimal end-to-end smoke test over `echo-types` itself as the + first real workspace. + +PanLL panel (`arghda-panll`) is v0.2 and deliberately not in this +sprint. The CLI + JSON is the interface contract; the panel is a +consumer. + +== Open questions + +* Language choice for `arghda-core`: Rust (matches PanLL stack) vs + Zig (matches Gossamer / Burble). Default: Rust, pending operator + pushback. +* Should the `proven` state record a content hash so upstream + changes can invalidate it automatically? Default: yes, SHA-256 + of the file plus imports. +* Naming convention for "headlines" — regex default + `^[a-z][A-Za-z0-9-]*$` with export-only filter, operator-overridable + per-workspace in `.arghda/config.toml`. + +== Acceptance criteria for v0.1 + +* End-to-end demo: take `echo-types` at its current commit, place + all `*.agda` files into `inbox/`, run `arghda-core` against it, + observe that every file moves to `proven/` with no hard-blocks, + and that the emitted DAG matches the actual import graph. +* Introduce one synthetic bug (delete `--safe` from a file): observe + that file lands in `rejected/` with the correct diagnostic. +* Introduce one synthetic orphan (new `.agda` not imported from + `All.agda`): observe `orphan-module` hard-block. + +== References + +* ArghDA scout report (this session): existing proof-workspace + landscape across Coq/Rocq, Lean 4, Isabelle, Agda. +* `docs/buchholz-plan.adoc` — the motivating proof pipeline that + surfaced the silent-failure gap. From 9a46e6fda9c92135e97a57fb1681ef2150bb0375 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 22 Apr 2026 11:50:10 +0000 Subject: [PATCH 7/7] Scaffold arghda-core v0.1 with two linter rules Rust crate parked at echo-types/arghda-core/ until it gets its own repo. Implements the v0.1 surface from docs/arghda-spec.adoc: - Workspace struct with four-state (inbox/working/proven/rejected) filesystem-backed layout; init() and open() are idempotent - notify-based filesystem watcher helper - LintRule trait + LintContext with include_root and entry_module - missing-safe-pragma rule: scans the head of each file for both --safe and --without-K, emits hard-block if either is missing - orphan-module rule: builds the transitive import closure starting from All.agda (tolerating stdlib modules as silent absent files), hard-blocks any .agda file outside that closure - CLI (arghda): init, scan --json, watch - Smoke test asserts the echo-types Agda suite passes both rules at the current commit (19 files, 0 hard-blocks) https://claude.ai/code/session_01DDGQFBtAT9JdRwmu25QzC2 --- .gitignore | 1 + arghda-core/Cargo.lock | 814 ++++++++++++++++++++++++++ arghda-core/Cargo.toml | 22 + arghda-core/README.md | 35 ++ arghda-core/src/diagnostic.rs | 46 ++ arghda-core/src/lib.rs | 13 + arghda-core/src/lint/mod.rs | 40 ++ arghda-core/src/lint/orphan_module.rs | 178 ++++++ arghda-core/src/lint/safe_pragma.rs | 58 ++ arghda-core/src/main.rs | 143 +++++ arghda-core/src/watcher.rs | 22 + arghda-core/src/workspace.rs | 86 +++ arghda-core/tests/smoke.rs | 53 ++ 13 files changed, 1511 insertions(+) create mode 100644 arghda-core/Cargo.lock create mode 100644 arghda-core/Cargo.toml create mode 100644 arghda-core/README.md create mode 100644 arghda-core/src/diagnostic.rs create mode 100644 arghda-core/src/lib.rs create mode 100644 arghda-core/src/lint/mod.rs create mode 100644 arghda-core/src/lint/orphan_module.rs create mode 100644 arghda-core/src/lint/safe_pragma.rs create mode 100644 arghda-core/src/main.rs create mode 100644 arghda-core/src/watcher.rs create mode 100644 arghda-core/src/workspace.rs create mode 100644 arghda-core/tests/smoke.rs diff --git a/.gitignore b/.gitignore index 171a389..1f219d3 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,2 @@ *.agdai +arghda-core/target/ diff --git a/arghda-core/Cargo.lock b/arghda-core/Cargo.lock new file mode 100644 index 0000000..3957216 --- /dev/null +++ b/arghda-core/Cargo.lock @@ -0,0 +1,814 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 4 + +[[package]] +name = "anstream" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "824a212faf96e9acacdbd09febd34438f8f711fb84e09a8916013cd7815ca28d" +dependencies = [ + "anstyle", + "anstyle-parse", + "anstyle-query", + "anstyle-wincon", + "colorchoice", + "is_terminal_polyfill", + "utf8parse", +] + +[[package]] +name = "anstyle" +version = "1.0.14" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "940b3a0ca603d1eade50a4846a2afffd5ef57a9feac2c0e2ec2e14f9ead76000" + +[[package]] +name = "anstyle-parse" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "52ce7f38b242319f7cabaa6813055467063ecdc9d355bbb4ce0c68908cd8130e" +dependencies = [ + "utf8parse", +] + +[[package]] +name = "anstyle-query" +version = "1.1.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "40c48f72fd53cd289104fc64099abca73db4166ad86ea0b4341abe65af83dadc" +dependencies = [ + "windows-sys 0.61.2", +] + +[[package]] +name = "anstyle-wincon" +version = "3.0.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "291e6a250ff86cd4a820112fb8898808a366d8f9f58ce16d1f538353ad55747d" +dependencies = [ + "anstyle", + "once_cell_polyfill", + "windows-sys 0.61.2", +] + +[[package]] +name = "anyhow" +version = "1.0.102" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7f202df86484c868dbad7eaa557ef785d5c66295e41b460ef922eca0723b842c" + +[[package]] +name = "arghda-core" +version = "0.1.0" +dependencies = [ + "anyhow", + "clap", + "notify", + "serde", + "serde_json", + "tempfile", + "walkdir", +] + +[[package]] +name = "bitflags" +version = "1.3.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a" + +[[package]] +name = "bitflags" +version = "2.11.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c4512299f36f043ab09a583e57bceb5a5aab7a73db1805848e8fef3c9e8c78b3" + +[[package]] +name = "cfg-if" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9330f8b2ff13f34540b44e946ef35111825727b38d33286ef986142615121801" + +[[package]] +name = "clap" +version = "4.6.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1ddb117e43bbf7dacf0a4190fef4d345b9bad68dfc649cb349e7d17d28428e51" +dependencies = [ + "clap_builder", + "clap_derive", +] + +[[package]] +name = "clap_builder" +version = "4.6.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "714a53001bf66416adb0e2ef5ac857140e7dc3a0c48fb28b2f10762fc4b5069f" +dependencies = [ + "anstream", + "anstyle", + "clap_lex", + "strsim", +] + +[[package]] +name = "clap_derive" +version = "4.6.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f2ce8604710f6733aa641a2b3731eaa1e8b3d9973d5e3565da11800813f997a9" +dependencies = [ + "heck", + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "clap_lex" +version = "1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c8d4a3bb8b1e0c1050499d1815f5ab16d04f0959b233085fb31653fbfc9d98f9" + +[[package]] +name = "colorchoice" +version = "1.0.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1d07550c9036bf2ae0c684c4297d503f838287c83c53686d05370d0e139ae570" + +[[package]] +name = "crossbeam-channel" +version = "0.5.15" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "82b8f8f868b36967f9606790d1903570de9ceaf870a7bf9fbbd3016d636a2cb2" +dependencies = [ + "crossbeam-utils", +] + +[[package]] +name = "crossbeam-utils" +version = "0.8.21" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d0a5c400df2834b80a4c3327b3aad3a4c4cd4de0629063962b03235697506a28" + +[[package]] +name = "equivalent" +version = "1.0.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "877a4ace8713b0bcf2a4e7eec82529c029f1d0619886d18145fea96c3ffe5c0f" + +[[package]] +name = "errno" +version = "0.3.14" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "39cab71617ae0d63f51a36d69f866391735b51691dbda63cf6f96d042b63efeb" +dependencies = [ + "libc", + "windows-sys 0.61.2", +] + +[[package]] +name = "fastrand" +version = "2.4.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9f1f227452a390804cdb637b74a86990f2a7d7ba4b7d5693aac9b4dd6defd8d6" + +[[package]] +name = "filetime" +version = "0.2.27" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f98844151eee8917efc50bd9e8318cb963ae8b297431495d3f758616ea5c57db" +dependencies = [ + "cfg-if", + "libc", + "libredox", +] + +[[package]] +name = "foldhash" +version = "0.1.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d9c4f5dac5e15c24eb999c26181a6ca40b39fe946cbe4c263c7209467bc83af2" + +[[package]] +name = "fsevent-sys" +version = "4.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "76ee7a02da4d231650c7cea31349b889be2f45ddb3ef3032d2ec8185f6313fd2" +dependencies = [ + "libc", +] + +[[package]] +name = "getrandom" +version = "0.4.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0de51e6874e94e7bf76d726fc5d13ba782deca734ff60d5bb2fb2607c7406555" +dependencies = [ + "cfg-if", + "libc", + "r-efi", + "wasip2", + "wasip3", +] + +[[package]] +name = "hashbrown" +version = "0.15.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9229cfe53dfd69f0609a49f65461bd93001ea1ef889cd5529dd176593f5338a1" +dependencies = [ + "foldhash", +] + +[[package]] +name = "hashbrown" +version = "0.17.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4f467dd6dccf739c208452f8014c75c18bb8301b050ad1cfb27153803edb0f51" + +[[package]] +name = "heck" +version = "0.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2304e00983f87ffb38b55b444b5e3b60a884b5d30c0fca7d82fe33449bbe55ea" + +[[package]] +name = "id-arena" +version = "2.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3d3067d79b975e8844ca9eb072e16b31c3c1c36928edf9c6789548c524d0d954" + +[[package]] +name = "indexmap" +version = "2.14.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d466e9454f08e4a911e14806c24e16fba1b4c121d1ea474396f396069cf949d9" +dependencies = [ + "equivalent", + "hashbrown 0.17.0", + "serde", + "serde_core", +] + +[[package]] +name = "inotify" +version = "0.9.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f8069d3ec154eb856955c1c0fbffefbf5f3c40a104ec912d4797314c1801abff" +dependencies = [ + "bitflags 1.3.2", + "inotify-sys", + "libc", +] + +[[package]] +name = "inotify-sys" +version = "0.1.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e05c02b5e89bff3b946cedeca278abc628fe811e604f027c45a8aa3cf793d0eb" +dependencies = [ + "libc", +] + +[[package]] +name = "is_terminal_polyfill" +version = "1.70.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a6cb138bb79a146c1bd460005623e142ef0181e3d0219cb493e02f7d08a35695" + +[[package]] +name = "itoa" +version = "1.0.18" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8f42a60cbdf9a97f5d2305f08a87dc4e09308d1276d28c869c684d7777685682" + +[[package]] +name = "kqueue" +version = "1.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "eac30106d7dce88daf4a3fcb4879ea939476d5074a9b7ddd0fb97fa4bed5596a" +dependencies = [ + "kqueue-sys", + "libc", +] + +[[package]] +name = "kqueue-sys" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ed9625ffda8729b85e45cf04090035ac368927b8cebc34898e7c120f52e4838b" +dependencies = [ + "bitflags 1.3.2", + "libc", +] + +[[package]] +name = "leb128fmt" +version = "0.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "09edd9e8b54e49e587e4f6295a7d29c3ea94d469cb40ab8ca70b288248a81db2" + +[[package]] +name = "libc" +version = "0.2.185" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "52ff2c0fe9bc6cb6b14a0592c2ff4fa9ceb83eea9db979b0487cd054946a2b8f" + +[[package]] +name = "libredox" +version = "0.1.16" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e02f3bb43d335493c96bf3fd3a321600bf6bd07ed34bc64118e9293bdffea46c" +dependencies = [ + "bitflags 2.11.1", + "libc", + "plain", + "redox_syscall", +] + +[[package]] +name = "linux-raw-sys" +version = "0.12.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "32a66949e030da00e8c7d4434b251670a91556f4144941d37452769c25d58a53" + +[[package]] +name = "log" +version = "0.4.29" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5e5032e24019045c762d3c0f28f5b6b8bbf38563a65908389bf7978758920897" + +[[package]] +name = "memchr" +version = "2.8.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f8ca58f447f06ed17d5fc4043ce1b10dd205e060fb3ce5b979b8ed8e59ff3f79" + +[[package]] +name = "mio" +version = "0.8.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a4a650543ca06a924e8b371db273b2756685faae30f8487da1b56505a8f78b0c" +dependencies = [ + "libc", + "log", + "wasi", + "windows-sys 0.48.0", +] + +[[package]] +name = "notify" +version = "6.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6205bd8bb1e454ad2e27422015fb5e4f2bcc7e08fa8f27058670d208324a4d2d" +dependencies = [ + "bitflags 2.11.1", + "crossbeam-channel", + "filetime", + "fsevent-sys", + "inotify", + "kqueue", + "libc", + "log", + "mio", + "walkdir", + "windows-sys 0.48.0", +] + +[[package]] +name = "once_cell" +version = "1.21.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9f7c3e4beb33f85d45ae3e3a1792185706c8e16d043238c593331cc7cd313b50" + +[[package]] +name = "once_cell_polyfill" +version = "1.70.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "384b8ab6d37215f3c5301a95a4accb5d64aa607f1fcb26a11b5303878451b4fe" + +[[package]] +name = "plain" +version = "0.2.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b4596b6d070b27117e987119b4dac604f3c58cfb0b191112e24771b2faeac1a6" + +[[package]] +name = "prettyplease" +version = "0.2.37" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "479ca8adacdd7ce8f1fb39ce9ecccbfe93a3f1344b3d0d97f20bc0196208f62b" +dependencies = [ + "proc-macro2", + "syn", +] + +[[package]] +name = "proc-macro2" +version = "1.0.106" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8fd00f0bb2e90d81d1044c2b32617f68fcb9fa3bb7640c23e9c748e53fb30934" +dependencies = [ + "unicode-ident", +] + +[[package]] +name = "quote" +version = "1.0.45" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "41f2619966050689382d2b44f664f4bc593e129785a36d6ee376ddf37259b924" +dependencies = [ + "proc-macro2", +] + +[[package]] +name = "r-efi" +version = "6.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f8dcc9c7d52a811697d2151c701e0d08956f92b0e24136cf4cf27b57a6a0d9bf" + +[[package]] +name = "redox_syscall" +version = "0.7.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f450ad9c3b1da563fb6948a8e0fb0fb9269711c9c73d9ea1de5058c79c8d643a" +dependencies = [ + "bitflags 2.11.1", +] + +[[package]] +name = "rustix" +version = "1.1.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b6fe4565b9518b83ef4f91bb47ce29620ca828bd32cb7e408f0062e9930ba190" +dependencies = [ + "bitflags 2.11.1", + "errno", + "libc", + "linux-raw-sys", + "windows-sys 0.61.2", +] + +[[package]] +name = "same-file" +version = "1.0.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "93fc1dc3aaa9bfed95e02e6eadabb4baf7e3078b0bd1b4d7b6b0b68378900502" +dependencies = [ + "winapi-util", +] + +[[package]] +name = "semver" +version = "1.0.28" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8a7852d02fc848982e0c167ef163aaff9cd91dc640ba85e263cb1ce46fae51cd" + +[[package]] +name = "serde" +version = "1.0.228" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9a8e94ea7f378bd32cbbd37198a4a91436180c5bb472411e48b5ec2e2124ae9e" +dependencies = [ + "serde_core", + "serde_derive", +] + +[[package]] +name = "serde_core" +version = "1.0.228" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "41d385c7d4ca58e59fc732af25c3983b67ac852c1a25000afe1175de458b67ad" +dependencies = [ + "serde_derive", +] + +[[package]] +name = "serde_derive" +version = "1.0.228" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d540f220d3187173da220f885ab66608367b6574e925011a9353e4badda91d79" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "serde_json" +version = "1.0.149" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "83fc039473c5595ace860d8c4fafa220ff474b3fc6bfdb4293327f1a37e94d86" +dependencies = [ + "itoa", + "memchr", + "serde", + "serde_core", + "zmij", +] + +[[package]] +name = "strsim" +version = "0.11.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7da8b5736845d9f2fcb837ea5d9e2628564b3b043a70948a3f0b778838c5fb4f" + +[[package]] +name = "syn" +version = "2.0.117" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e665b8803e7b1d2a727f4023456bbbbe74da67099c585258af0ad9c5013b9b99" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + +[[package]] +name = "tempfile" +version = "3.27.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "32497e9a4c7b38532efcdebeef879707aa9f794296a4f0244f6f69e9bc8574bd" +dependencies = [ + "fastrand", + "getrandom", + "once_cell", + "rustix", + "windows-sys 0.61.2", +] + +[[package]] +name = "unicode-ident" +version = "1.0.24" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75" + +[[package]] +name = "unicode-xid" +version = "0.2.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ebc1c04c71510c7f702b52b7c350734c9ff1295c464a03335b00bb84fc54f853" + +[[package]] +name = "utf8parse" +version = "0.2.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "06abde3611657adf66d383f00b093d7faecc7fa57071cce2578660c9f1010821" + +[[package]] +name = "walkdir" +version = "2.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "29790946404f91d9c5d06f9874efddea1dc06c5efe94541a7d6863108e3a5e4b" +dependencies = [ + "same-file", + "winapi-util", +] + +[[package]] +name = "wasi" +version = "0.11.1+wasi-snapshot-preview1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ccf3ec651a847eb01de73ccad15eb7d99f80485de043efb2f370cd654f4ea44b" + +[[package]] +name = "wasip2" +version = "1.0.3+wasi-0.2.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "20064672db26d7cdc89c7798c48a0fdfac8213434a1186e5ef29fd560ae223d6" +dependencies = [ + "wit-bindgen 0.57.1", +] + +[[package]] +name = "wasip3" +version = "0.4.0+wasi-0.3.0-rc-2026-01-06" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5428f8bf88ea5ddc08faddef2ac4a67e390b88186c703ce6dbd955e1c145aca5" +dependencies = [ + "wit-bindgen 0.51.0", +] + +[[package]] +name = "wasm-encoder" +version = "0.244.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "990065f2fe63003fe337b932cfb5e3b80e0b4d0f5ff650e6985b1048f62c8319" +dependencies = [ + "leb128fmt", + "wasmparser", +] + +[[package]] +name = "wasm-metadata" +version = "0.244.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bb0e353e6a2fbdc176932bbaab493762eb1255a7900fe0fea1a2f96c296cc909" +dependencies = [ + "anyhow", + "indexmap", + "wasm-encoder", + "wasmparser", +] + +[[package]] +name = "wasmparser" +version = "0.244.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "47b807c72e1bac69382b3a6fb3dbe8ea4c0ed87ff5629b8685ae6b9a611028fe" +dependencies = [ + "bitflags 2.11.1", + "hashbrown 0.15.5", + "indexmap", + "semver", +] + +[[package]] +name = "winapi-util" +version = "0.1.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c2a7b1c03c876122aa43f3020e6c3c3ee5c05081c9a00739faf7503aeba10d22" +dependencies = [ + "windows-sys 0.61.2", +] + +[[package]] +name = "windows-link" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f0805222e57f7521d6a62e36fa9163bc891acd422f971defe97d64e70d0a4fe5" + +[[package]] +name = "windows-sys" +version = "0.48.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "677d2418bec65e3338edb076e806bc1ec15693c5d0104683f2efe857f61056a9" +dependencies = [ + "windows-targets", +] + +[[package]] +name = "windows-sys" +version = "0.61.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ae137229bcbd6cdf0f7b80a31df61766145077ddf49416a728b02cb3921ff3fc" +dependencies = [ + "windows-link", +] + +[[package]] +name = "windows-targets" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9a2fa6e2155d7247be68c096456083145c183cbbbc2764150dda45a87197940c" +dependencies = [ + "windows_aarch64_gnullvm", + "windows_aarch64_msvc", + "windows_i686_gnu", + "windows_i686_msvc", + "windows_x86_64_gnu", + "windows_x86_64_gnullvm", + "windows_x86_64_msvc", +] + +[[package]] +name = "windows_aarch64_gnullvm" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2b38e32f0abccf9987a4e3079dfb67dcd799fb61361e53e2882c3cbaf0d905d8" + +[[package]] +name = "windows_aarch64_msvc" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "dc35310971f3b2dbbf3f0690a219f40e2d9afcf64f9ab7cc1be722937c26b4bc" + +[[package]] +name = "windows_i686_gnu" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a75915e7def60c94dcef72200b9a8e58e5091744960da64ec734a6c6e9b3743e" + +[[package]] +name = "windows_i686_msvc" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8f55c233f70c4b27f66c523580f78f1004e8b5a8b659e05a4eb49d4166cca406" + +[[package]] +name = "windows_x86_64_gnu" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "53d40abd2583d23e4718fddf1ebec84dbff8381c07cae67ff7768bbf19c6718e" + +[[package]] +name = "windows_x86_64_gnullvm" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0b7b52767868a23d5bab768e390dc5f5c55825b6d30b86c844ff2dc7414044cc" + +[[package]] +name = "windows_x86_64_msvc" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ed94fce61571a4006852b7389a063ab983c02eb1bb37b47f8272ce92d06d9538" + +[[package]] +name = "wit-bindgen" +version = "0.51.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d7249219f66ced02969388cf2bb044a09756a083d0fab1e566056b04d9fbcaa5" +dependencies = [ + "wit-bindgen-rust-macro", +] + +[[package]] +name = "wit-bindgen" +version = "0.57.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1ebf944e87a7c253233ad6766e082e3cd714b5d03812acc24c318f549614536e" + +[[package]] +name = "wit-bindgen-core" +version = "0.51.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ea61de684c3ea68cb082b7a88508a8b27fcc8b797d738bfc99a82facf1d752dc" +dependencies = [ + "anyhow", + "heck", + "wit-parser", +] + +[[package]] +name = "wit-bindgen-rust" +version = "0.51.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b7c566e0f4b284dd6561c786d9cb0142da491f46a9fbed79ea69cdad5db17f21" +dependencies = [ + "anyhow", + "heck", + "indexmap", + "prettyplease", + "syn", + "wasm-metadata", + "wit-bindgen-core", + "wit-component", +] + +[[package]] +name = "wit-bindgen-rust-macro" +version = "0.51.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0c0f9bfd77e6a48eccf51359e3ae77140a7f50b1e2ebfe62422d8afdaffab17a" +dependencies = [ + "anyhow", + "prettyplease", + "proc-macro2", + "quote", + "syn", + "wit-bindgen-core", + "wit-bindgen-rust", +] + +[[package]] +name = "wit-component" +version = "0.244.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9d66ea20e9553b30172b5e831994e35fbde2d165325bec84fc43dbf6f4eb9cb2" +dependencies = [ + "anyhow", + "bitflags 2.11.1", + "indexmap", + "log", + "serde", + "serde_derive", + "serde_json", + "wasm-encoder", + "wasm-metadata", + "wasmparser", + "wit-parser", +] + +[[package]] +name = "wit-parser" +version = "0.244.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ecc8ac4bc1dc3381b7f59c34f00b67e18f910c2c0f50015669dde7def656a736" +dependencies = [ + "anyhow", + "id-arena", + "indexmap", + "log", + "semver", + "serde", + "serde_derive", + "serde_json", + "unicode-xid", + "wasmparser", +] + +[[package]] +name = "zmij" +version = "1.0.21" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b8848ee67ecc8aedbaf3e4122217aff892639231befc6a1b58d29fff4c2cabaa" diff --git a/arghda-core/Cargo.toml b/arghda-core/Cargo.toml new file mode 100644 index 0000000..873b67b --- /dev/null +++ b/arghda-core/Cargo.toml @@ -0,0 +1,22 @@ +[package] +name = "arghda-core" +version = "0.1.0" +edition = "2021" +description = "Lightweight proof-workspace manager for Agda" +license = "PMPL-1.0-or-later" +repository = "https://github.com/hyperpolymath/echo-types" + +[[bin]] +name = "arghda" +path = "src/main.rs" + +[dependencies] +anyhow = "1" +clap = { version = "4", features = ["derive"] } +notify = "6" +serde = { version = "1", features = ["derive"] } +serde_json = "1" +walkdir = "2" + +[dev-dependencies] +tempfile = "3" diff --git a/arghda-core/README.md b/arghda-core/README.md new file mode 100644 index 0000000..303c530 --- /dev/null +++ b/arghda-core/README.md @@ -0,0 +1,35 @@ +# arghda-core + +Lightweight proof-workspace manager for Agda. This crate parks inside +`echo-types` until its own repo exists; see `docs/arghda-spec.adoc` at +the echo-types root for the design. + +## v0.1 scope + +- `Workspace` struct with four-state dir layout (`inbox`, `working`, + `proven`, `rejected`) +- Filesystem watcher (`notify`-based) +- Two linter rules: + - `missing-safe-pragma` — file lacks `{-# OPTIONS --safe --without-K #-}` + - `orphan-module` — `.agda` file not imported from `All.agda` +- CLI (`arghda`) with subcommands: `init`, `scan`, `watch` + +Not yet: `promote`, `reject`, `dag` (v0.1.x). + +## Build + +``` +cd arghda-core +cargo build +cargo test +``` + +## Smoke against echo-types + +``` +cd arghda-core +cargo run -- scan ../proofs/agda +``` + +Expected: every `.agda` file passes `missing-safe-pragma`; `orphan-module` +checks against `../proofs/agda/All.agda`. diff --git a/arghda-core/src/diagnostic.rs b/arghda-core/src/diagnostic.rs new file mode 100644 index 0000000..e7aca9b --- /dev/null +++ b/arghda-core/src/diagnostic.rs @@ -0,0 +1,46 @@ +use serde::{Deserialize, Serialize}; +use std::path::PathBuf; + +#[derive(Clone, Copy, Debug, Eq, PartialEq, Serialize, Deserialize)] +#[serde(rename_all = "kebab-case")] +pub enum Severity { + HardBlock, + Warn, +} + +#[derive(Clone, Debug, Serialize, Deserialize)] +pub struct Diagnostic { + pub rule: String, + pub severity: Severity, + pub file: PathBuf, + pub message: String, + pub line: Option, +} + +#[derive(Clone, Debug, Default, Serialize, Deserialize)] +pub struct LintReport { + pub file: PathBuf, + pub diagnostics: Vec, +} + +impl LintReport { + pub fn new(file: PathBuf) -> Self { + Self { file, diagnostics: Vec::new() } + } + + pub fn push(&mut self, d: Diagnostic) { + self.diagnostics.push(d); + } + + pub fn has_hard_block(&self) -> bool { + self.diagnostics.iter().any(|d| d.severity == Severity::HardBlock) + } + + pub fn hard_blocks(&self) -> impl Iterator { + self.diagnostics.iter().filter(|d| d.severity == Severity::HardBlock) + } + + pub fn warns(&self) -> impl Iterator { + self.diagnostics.iter().filter(|d| d.severity == Severity::Warn) + } +} diff --git a/arghda-core/src/lib.rs b/arghda-core/src/lib.rs new file mode 100644 index 0000000..755a61a --- /dev/null +++ b/arghda-core/src/lib.rs @@ -0,0 +1,13 @@ +//! arghda-core: proof-workspace manager for Agda. +//! +//! Public surface is intentionally small: `Workspace`, the lint traits, +//! and the diagnostic types. The CLI in `main.rs` is a thin consumer. + +pub mod diagnostic; +pub mod lint; +pub mod watcher; +pub mod workspace; + +pub use diagnostic::{Diagnostic, LintReport, Severity}; +pub use lint::{LintRule, default_rules, run_lints}; +pub use workspace::{State, Workspace}; diff --git a/arghda-core/src/lint/mod.rs b/arghda-core/src/lint/mod.rs new file mode 100644 index 0000000..b4ec3b8 --- /dev/null +++ b/arghda-core/src/lint/mod.rs @@ -0,0 +1,40 @@ +use crate::diagnostic::LintReport; +use anyhow::Result; +use std::path::Path; + +pub mod orphan_module; +pub mod safe_pragma; + +/// Context handed to every rule. +#[derive(Clone, Debug)] +pub struct LintContext<'a> { + /// Agda include root; `.agda` files' module names are computed + /// relative to this path. + pub include_root: &'a Path, + /// Path to the `All.agda` (or equivalent) entry module. + pub entry_module: &'a Path, +} + +pub trait LintRule: Send + Sync { + fn name(&self) -> &'static str; + fn run(&self, file: &Path, ctx: &LintContext<'_>, report: &mut LintReport) -> Result<()>; +} + +pub fn default_rules() -> Vec> { + vec![ + Box::new(safe_pragma::SafePragma), + Box::new(orphan_module::OrphanModule), + ] +} + +pub fn run_lints( + file: &Path, + ctx: &LintContext<'_>, + rules: &[Box], +) -> Result { + let mut report = LintReport::new(file.to_path_buf()); + for rule in rules { + rule.run(file, ctx, &mut report)?; + } + Ok(report) +} diff --git a/arghda-core/src/lint/orphan_module.rs b/arghda-core/src/lint/orphan_module.rs new file mode 100644 index 0000000..d74cc63 --- /dev/null +++ b/arghda-core/src/lint/orphan_module.rs @@ -0,0 +1,178 @@ +use super::{LintContext, LintRule}; +use crate::diagnostic::{Diagnostic, LintReport, Severity}; +use anyhow::{Context, Result}; +use std::collections::HashSet; +use std::fs; +use std::path::{Path, PathBuf}; + +pub struct OrphanModule; + +impl LintRule for OrphanModule { + fn name(&self) -> &'static str { + "orphan-module" + } + + fn run(&self, file: &Path, ctx: &LintContext<'_>, report: &mut LintReport) -> Result<()> { + let Some(module) = module_name_of(file, ctx.include_root) else { + return Ok(()); // file sits outside include_root; nothing to say + }; + + // The entry module itself is never an orphan of itself. + if Some(module.as_str()) == module_name_of(ctx.entry_module, ctx.include_root).as_deref() { + return Ok(()); + } + + let reachable = transitive_imports(ctx.entry_module, ctx.include_root) + .with_context(|| { + format!( + "computing transitive imports from {}", + ctx.entry_module.display() + ) + })?; + + if !reachable.contains(&module) { + report.push(Diagnostic { + rule: self.name().to_string(), + severity: Severity::HardBlock, + file: file.to_path_buf(), + message: format!( + "module `{}` is not reachable via imports from `{}`", + module, + ctx.entry_module.display() + ), + line: None, + }); + } + + Ok(()) + } +} + +/// Relative module path for `file` under `include_root`. +/// Returns `None` if `file` is outside the root or not a `.agda` source. +fn module_name_of(file: &Path, include_root: &Path) -> Option { + let rel = file.strip_prefix(include_root).ok()?; + let stem = rel.with_extension(""); + let mut parts = Vec::new(); + for comp in stem.components() { + let std::path::Component::Normal(s) = comp else { + return None; + }; + parts.push(s.to_str()?.to_string()); + } + if parts.is_empty() { + return None; + } + Some(parts.join(".")) +} + +fn module_to_path(module: &str, include_root: &Path) -> PathBuf { + let mut p = include_root.to_path_buf(); + for part in module.split('.') { + p.push(part); + } + p.set_extension("agda"); + p +} + +fn transitive_imports(entry: &Path, include_root: &Path) -> Result> { + let mut reachable: HashSet = HashSet::new(); + let mut worklist: Vec = Vec::new(); + + if let Some(m) = module_name_of(entry, include_root) { + reachable.insert(m.clone()); + worklist.push(m); + } else { + // Entry is outside the include root; seed with its imports directly. + for imp in direct_imports(entry)? { + if reachable.insert(imp.clone()) { + worklist.push(imp); + } + } + } + + while let Some(module) = worklist.pop() { + let path = module_to_path(&module, include_root); + // Missing files (stdlib, external deps) are silently skipped. + if !path.is_file() { + continue; + } + for imp in direct_imports(&path)? { + if reachable.insert(imp.clone()) { + worklist.push(imp); + } + } + } + + Ok(reachable) +} + +/// Extract module names appearing in `import ...` / `open import ...` +/// top-level forms of `file`. Tolerant: stops at the first token after +/// `import`; ignores `hiding`, `using`, `as`, `public` modifiers. +fn direct_imports(file: &Path) -> Result> { + let contents = fs::read_to_string(file) + .with_context(|| format!("reading {}", file.display()))?; + let mut out = Vec::new(); + for line in contents.lines() { + let trimmed = line.trim_start(); + if trimmed.starts_with("--") { + continue; + } + // Accept `import X`, `open import X`, `open import X as Y`, etc. + let tokens: Vec<&str> = trimmed.split_whitespace().collect(); + let idx = tokens.iter().position(|&t| t == "import"); + let Some(i) = idx else { continue }; + // Reject lines where `import` is inside a string literal or embedded + // in a larger identifier; a cheap heuristic is to require that the + // token before `import` is empty, `open`, or absent. + if i > 0 { + let prev = tokens[i - 1]; + if prev != "open" { + continue; + } + } + let Some(module) = tokens.get(i + 1) else { continue }; + // Strip trailing punctuation Agda never allows in module paths. + let cleaned = module.trim_end_matches(|c: char| !c.is_alphanumeric() && c != '.' && c != '_'); + if cleaned.is_empty() { + continue; + } + out.push(cleaned.to_string()); + } + Ok(out) +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn module_name_roundtrip() { + let root = Path::new("/r"); + let file = Path::new("/r/Ordinal/Closure.agda"); + let name = module_name_of(file, root).unwrap(); + assert_eq!(name, "Ordinal.Closure"); + let back = module_to_path(&name, root); + assert_eq!(back, PathBuf::from("/r/Ordinal/Closure.agda")); + } + + #[test] + fn parses_open_import_with_modifiers() { + let tmp = tempfile::NamedTempFile::new().unwrap(); + std::fs::write( + tmp.path(), + "module M where\n\ + open import Data.Nat using (ℕ)\n\ + open import Foo.Bar\n\ + import Baz as B\n\ + -- open import IgnoredComment\n", + ) + .unwrap(); + let imports = direct_imports(tmp.path()).unwrap(); + assert!(imports.contains(&"Data.Nat".to_string())); + assert!(imports.contains(&"Foo.Bar".to_string())); + assert!(imports.contains(&"Baz".to_string())); + assert!(!imports.iter().any(|i| i.contains("Ignored"))); + } +} diff --git a/arghda-core/src/lint/safe_pragma.rs b/arghda-core/src/lint/safe_pragma.rs new file mode 100644 index 0000000..4d7039e --- /dev/null +++ b/arghda-core/src/lint/safe_pragma.rs @@ -0,0 +1,58 @@ +use super::{LintContext, LintRule}; +use crate::diagnostic::{Diagnostic, LintReport, Severity}; +use anyhow::{Context, Result}; +use std::fs; +use std::path::Path; + +pub struct SafePragma; + +const HEAD_LINES_SCANNED: usize = 30; + +impl LintRule for SafePragma { + fn name(&self) -> &'static str { + "missing-safe-pragma" + } + + fn run(&self, file: &Path, _ctx: &LintContext<'_>, report: &mut LintReport) -> Result<()> { + let contents = fs::read_to_string(file) + .with_context(|| format!("reading {}", file.display()))?; + + let mut safe_seen = false; + let mut without_k_seen = false; + + for line in contents.lines().take(HEAD_LINES_SCANNED) { + if !line.trim_start().starts_with("{-#") { + continue; + } + if line.contains("OPTIONS") { + if line.contains("--safe") { + safe_seen = true; + } + if line.contains("--without-K") { + without_k_seen = true; + } + } + } + + if !safe_seen || !without_k_seen { + let missing = match (safe_seen, without_k_seen) { + (false, false) => "--safe and --without-K", + (false, true) => "--safe", + (true, false) => "--without-K", + _ => unreachable!(), + }; + report.push(Diagnostic { + rule: self.name().to_string(), + severity: Severity::HardBlock, + file: file.to_path_buf(), + message: format!( + "missing {} pragma in first {} lines", + missing, HEAD_LINES_SCANNED + ), + line: None, + }); + } + + Ok(()) + } +} diff --git a/arghda-core/src/main.rs b/arghda-core/src/main.rs new file mode 100644 index 0000000..65098c4 --- /dev/null +++ b/arghda-core/src/main.rs @@ -0,0 +1,143 @@ +use anyhow::{Context, Result}; +use arghda_core::{default_rules, run_lints, watcher, Workspace}; +use arghda_core::lint::LintContext; +use clap::{Parser, Subcommand}; +use std::path::{Path, PathBuf}; +use std::time::Duration; +use walkdir::WalkDir; + +#[derive(Parser)] +#[command(name = "arghda", version, about = "Proof-workspace manager (Agda, v0.1)")] +struct Cli { + #[command(subcommand)] + cmd: Cmd, +} + +#[derive(Subcommand)] +enum Cmd { + /// Create the four-state workspace layout at PATH. + Init { + path: PathBuf, + }, + /// Lint every `.agda` file under PATH without moving anything. + Scan { + /// Directory containing `.agda` files; treated as the include root. + path: PathBuf, + /// Entry module used for orphan detection. Defaults to + /// `/All.agda`. + #[arg(long)] + entry: Option, + /// Emit the report as JSON instead of human-readable text. + #[arg(long)] + json: bool, + }, + /// Watch `inbox/` and `working/` in a workspace; print events. + Watch { + workspace: PathBuf, + }, +} + +fn main() -> Result<()> { + let cli = Cli::parse(); + match cli.cmd { + Cmd::Init { path } => { + let ws = Workspace::init(&path)?; + println!("initialised workspace at {}", ws.root().display()); + } + Cmd::Scan { path, entry, json } => scan(&path, entry.as_deref(), json)?, + Cmd::Watch { workspace } => watch(&workspace)?, + } + Ok(()) +} + +fn scan(include_root: &Path, entry: Option<&Path>, json: bool) -> Result<()> { + let entry_buf; + let entry = match entry { + Some(e) => e, + None => { + entry_buf = include_root.join("All.agda"); + &entry_buf + } + }; + if !entry.is_file() { + anyhow::bail!("entry module not found: {}", entry.display()); + } + + let rules = default_rules(); + let ctx = LintContext { include_root, entry_module: entry }; + + let mut reports = Vec::new(); + let mut hard_blocks = 0usize; + let mut warns = 0usize; + + for entry in WalkDir::new(include_root).into_iter().filter_map(|e| e.ok()) { + let path = entry.path(); + if path.extension().and_then(|s| s.to_str()) != Some("agda") { + continue; + } + let report = run_lints(path, &ctx, &rules) + .with_context(|| format!("linting {}", path.display()))?; + hard_blocks += report.hard_blocks().count(); + warns += report.warns().count(); + reports.push(report); + } + + if json { + let payload = serde_json::json!({ + "version": "0.1", + "include_root": include_root, + "entry_module": entry, + "files_scanned": reports.len(), + "hard_blocks": hard_blocks, + "warns": warns, + "reports": reports, + }); + println!("{}", serde_json::to_string_pretty(&payload)?); + } else { + for report in &reports { + if report.diagnostics.is_empty() { + continue; + } + println!("{}", report.file.display()); + for d in &report.diagnostics { + let tag = match d.severity { + arghda_core::Severity::HardBlock => "BLOCK", + arghda_core::Severity::Warn => "warn", + }; + println!(" [{}] {}: {}", tag, d.rule, d.message); + } + } + println!( + "\nscanned {} files; {} hard-block(s), {} warn(s)", + reports.len(), + hard_blocks, + warns + ); + } + Ok(()) +} + +fn watch(workspace_path: &Path) -> Result<()> { + let ws = Workspace::open(workspace_path)?; + let inbox = ws.state_dir(arghda_core::State::Inbox); + let working = ws.state_dir(arghda_core::State::Working); + + let (_w_inbox, rx_inbox) = watcher::watch(&inbox, false)?; + let (_w_working, rx_working) = watcher::watch(&working, false)?; + + println!("watching {} and {}", inbox.display(), working.display()); + println!("press ctrl-c to stop"); + + loop { + if let Ok(ev) = rx_inbox.recv_timeout(Duration::from_millis(200)) { + if let Ok(ev) = ev { + println!("inbox: {:?} {:?}", ev.kind, ev.paths); + } + } + if let Ok(ev) = rx_working.recv_timeout(Duration::from_millis(200)) { + if let Ok(ev) = ev { + println!("working: {:?} {:?}", ev.kind, ev.paths); + } + } + } +} diff --git a/arghda-core/src/watcher.rs b/arghda-core/src/watcher.rs new file mode 100644 index 0000000..80ad887 --- /dev/null +++ b/arghda-core/src/watcher.rs @@ -0,0 +1,22 @@ +use anyhow::Result; +use notify::{RecommendedWatcher, RecursiveMode, Watcher}; +use std::path::Path; +use std::sync::mpsc; + +/// Minimal blocking watcher over a single directory. +/// Returns a receiver the caller can drain. Callers are responsible +/// for deciding what a given event means for triage state. +pub fn watch( + path: impl AsRef, + recursive: bool, +) -> Result<(RecommendedWatcher, mpsc::Receiver>)> { + let (tx, rx) = mpsc::channel(); + let mut watcher = notify::recommended_watcher(tx)?; + let mode = if recursive { + RecursiveMode::Recursive + } else { + RecursiveMode::NonRecursive + }; + watcher.watch(path.as_ref(), mode)?; + Ok((watcher, rx)) +} diff --git a/arghda-core/src/workspace.rs b/arghda-core/src/workspace.rs new file mode 100644 index 0000000..908ea65 --- /dev/null +++ b/arghda-core/src/workspace.rs @@ -0,0 +1,86 @@ +use anyhow::{Context, Result}; +use serde::{Deserialize, Serialize}; +use std::fs; +use std::path::{Path, PathBuf}; + +const STATE_DIRS: &[&str] = &["inbox", "working", "proven", "rejected"]; + +#[derive(Clone, Copy, Debug, Eq, PartialEq, Serialize, Deserialize)] +#[serde(rename_all = "kebab-case")] +pub enum State { + Inbox, + Working, + Proven, + Rejected, +} + +impl State { + pub fn dir_name(self) -> &'static str { + match self { + State::Inbox => "inbox", + State::Working => "working", + State::Proven => "proven", + State::Rejected => "rejected", + } + } +} + +/// A workspace is a directory with the four state subdirs. +/// Its source of truth is the filesystem: transitions are file moves. +#[derive(Clone, Debug)] +pub struct Workspace { + root: PathBuf, +} + +impl Workspace { + /// Create the workspace layout at `root`, idempotently. + pub fn init(root: impl AsRef) -> Result { + let root = root.as_ref().to_path_buf(); + fs::create_dir_all(&root) + .with_context(|| format!("creating workspace root {}", root.display()))?; + for dir in STATE_DIRS { + let p = root.join(dir); + fs::create_dir_all(&p) + .with_context(|| format!("creating state dir {}", p.display()))?; + } + let meta = root.join(".arghda"); + fs::create_dir_all(&meta) + .with_context(|| format!("creating meta dir {}", meta.display()))?; + Ok(Self { root }) + } + + /// Open an existing workspace; fails if any state dir is missing. + pub fn open(root: impl AsRef) -> Result { + let root = root.as_ref().to_path_buf(); + for dir in STATE_DIRS { + let p = root.join(dir); + if !p.is_dir() { + anyhow::bail!("workspace missing state dir: {}", p.display()); + } + } + Ok(Self { root }) + } + + pub fn root(&self) -> &Path { + &self.root + } + + pub fn state_dir(&self, state: State) -> PathBuf { + self.root.join(state.dir_name()) + } + + /// List files currently in `state`. + pub fn list(&self, state: State) -> Result> { + let dir = self.state_dir(state); + let mut out = Vec::new(); + for entry in fs::read_dir(&dir) + .with_context(|| format!("reading state dir {}", dir.display()))? + { + let entry = entry?; + if entry.file_type()?.is_file() { + out.push(entry.path()); + } + } + Ok(out) + } +} diff --git a/arghda-core/tests/smoke.rs b/arghda-core/tests/smoke.rs new file mode 100644 index 0000000..41b671c --- /dev/null +++ b/arghda-core/tests/smoke.rs @@ -0,0 +1,53 @@ +//! End-to-end smoke test: run lints over the echo-types Agda suite and +//! verify v0.1 expectations. +//! +//! Expectation: every `.agda` file in `proofs/agda` passes +//! `missing-safe-pragma` and `orphan-module` relative to `All.agda`. + +use arghda_core::lint::{default_rules, LintContext}; +use arghda_core::{run_lints, Severity}; +use std::path::PathBuf; +use walkdir::WalkDir; + +fn echo_types_root() -> PathBuf { + // arghda-core sits at echo-types/arghda-core/. + let mut p = PathBuf::from(env!("CARGO_MANIFEST_DIR")); + p.pop(); + p +} + +#[test] +fn echo_types_passes_default_rules() { + let root = echo_types_root(); + let include_root = root.join("proofs").join("agda"); + let entry = include_root.join("All.agda"); + + assert!(entry.is_file(), "All.agda not found at {}", entry.display()); + + let rules = default_rules(); + let ctx = LintContext { + include_root: &include_root, + entry_module: &entry, + }; + + let mut hard_blocks = Vec::new(); + + for entry in WalkDir::new(&include_root).into_iter().filter_map(|e| e.ok()) { + let path = entry.path(); + if path.extension().and_then(|s| s.to_str()) != Some("agda") { + continue; + } + let report = run_lints(path, &ctx, &rules).expect("lint run failed"); + for d in report.diagnostics { + if d.severity == Severity::HardBlock { + hard_blocks.push(format!("{}: {} — {}", path.display(), d.rule, d.message)); + } + } + } + + assert!( + hard_blocks.is_empty(), + "expected no hard-blocks, got:\n{}", + hard_blocks.join("\n") + ); +}