build(just): add just gate — one-command local green-check

[hyperpolymath]

What

Deliverable #1 from the "continue in-site" discussion: a one-command, billing-independent local green-check. While GitHub-hosted CI is blocked, just gate runs the same checks locally and gives a single authoritative answer.

just gate

Runs every locally-faithful CI stage in sequence, continues past failures, and prints a per-stage PASS/FAIL/SKIP summary (non-zero exit on any FAIL):

stage	source of truth
rustfmt	cargo fmt --all -- --check
clippy	cargo clippy --workspace -- -D warnings
test	cargo test --workspace
grammar-check	Pest consistency (existing target)
verify-harvard	Harvard invariant (existing target)
e2e	tests/e2e.sh (parse + typecheck + run all examples)
idris2-proofs	idris2 --check of all 12 Idris proofs

Stages needing an absent toolchain (idris2) or an external GitHub action (A2ML/K9 validators, security scans) self-skip with a notice rather than failing, so it runs anywhere. The rocq canonical-proof-suite (needs Rocq 9) and the external manifest/security scans stay CI/nightly-only — there's no local validator for them in-repo.

Named gate to sit alongside the existing ci (build/test/lint/verify simulation) and check (fast fmt/lint/test pre-commit) without redefining either.

Verified

Ran end-to-end on main — GREEN ✓ (exit 0):

✓ PASS rustfmt   ✓ PASS clippy        ✓ PASS test
✓ PASS grammar-check  ✓ PASS verify-harvard  ✓ PASS e2e
✓ PASS idris2-proofs  ⊘ SKIP a2ml (no local validator)  ⊘ SKIP assail (panic-attack absent)
RESULT: GREEN ✓

(e2e internal tally: 49 pass / 0 fail / 17 intentional-skip.)

Scope

One file (Justfile) + CHANGELOG + session-log. No code/compiler changes.

Context: 007 is a private repo, so hosted CI draws the owner's GitHub Pro included minutes; the current block is a billing-settings state (owner-side). This gate makes "is it green?" answerable without waiting on that.

https://claude.ai/code/session_018CaSgNjNURC7ocsyjYh9We

---

Generated by Claude Code