Skip to content

Commit 9a46e6f

Browse files
committed
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
1 parent 2a8d9e8 commit 9a46e6f

13 files changed

Lines changed: 1511 additions & 0 deletions

File tree

.gitignore

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1 +1,2 @@
11
*.agdai
2+
arghda-core/target/

0 commit comments

Comments
 (0)