From 87103473355cdeda9eee22c030c1d45e3435af82 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 18 Jun 2026 01:42:28 +0000 Subject: [PATCH] =?UTF-8?q?build(just):=20add=20`just=20gate`=20=E2=80=94?= =?UTF-8?q?=20one-command=20local=20green-check?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A billing-independent way to answer "is it green?" without GitHub Actions — useful while the hosted-runner billing is blocked (007 is a private repo, so CI draws the owner's GitHub Pro included minutes; the gate runs the same checks locally regardless). `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): rustfmt · clippy · cargo test · grammar-check · verify-harvard · e2e · idris2 --check (all 12 Idris proofs) Stages that need an absent toolchain (idris2) or an external GitHub action (A2ML/K9 validators, security scans) self-SKIP with a notice instead of failing, so it runs anywhere. The rocq canonical-proof-suite (needs Rocq 9) and external manifest/security scans stay CI/nightly-only. Named `gate` to sit alongside the existing `ci` (build/test/lint/verify simulation) and `check` (fast fmt/lint/test pre-commit) without redefining them. Verified GREEN on main (7 PASS, 2 SKIP, 0 FAIL). https://claude.ai/code/session_018CaSgNjNURC7ocsyjYh9We --- .machine_readable/session-log.txt | 2 ++ CHANGELOG.md | 1 + Justfile | 55 +++++++++++++++++++++++++++++++ 3 files changed, 58 insertions(+) diff --git a/.machine_readable/session-log.txt b/.machine_readable/session-log.txt index 4049485..57f8965 100644 --- a/.machine_readable/session-log.txt +++ b/.machine_readable/session-log.txt @@ -33,3 +33,5 @@ [2026-06-15 17:39:22] Session continued: Layer-10 PHASE 3 RUNG 3a landed (named residues within a body) on branch claude/echo-residue-phase3-named off main. User chose syntax `reversible as undo {…}` / `reverse undo` (the `as`-binder, agent-ergonomic) and scope "static core first" (within-body, fully static; cross-handler 3b deferred). (a) Grammar: grammar.pest + spec/grammar.ebnf — reversible_block gains optional ("as" ~ ident); new reverse_named = "reverse" ~ ident; Harvard-safe (control rules ref the shared ident token; Harvard guard PASS). (b) AST: ADDITIVE variants ReversibleAs{binding,body} + ReverseNamed{target} — existing Reversible/Irreversible/Reverse untouched, so the 9 exhaustive ControlStmt matches were compiler-enumerated + mirrored (codegen_cranelift/elixir/native, dual_ast, eval, formatter, metainterpreter, semantic_analyser/control_flow, typechecker check_stmt) + oracle check.rs + the two combined typechecker passes (effects, collect_linear_lets). (c) Typechecker: per-body named_residues: HashMap — the static mirror of ResidueCell; bind_named_residue (reversible as → Holding(Linear>)); take_named_residue (reverse → Holding→Spent, else Err); per-function + per-handler mem::take isolation (no cross-body leak). Affine/linear: double reverse rejected (Spent), un-reversed bound name NOT an error, reverse of unknown/spent name = L10_REVERSE_WITHOUT_RESIDUE. (d) Parser: build_reversible_block detects optional ident → ReversibleAs vs Reversible; build_reverse_named. (e) Tests: 2 parser (reversible_as_binds_named_residue, reverse_named_parses) + 5 typechecker (named-reverse-ok, reverse-unknown-errs, double-reverse-errs, unreversed-ok-affine, no-cross-function-leak) → 890 oo7-core lib tests pass; full workspace cargo test 0 failures; cargo fmt --check clean; cargo clippy --offline -D warnings exit 0 (CI-equivalent). (f) Docs in lockstep: TYPE-SYSTEM-SPEC §11b.5 (new), docs/echo-residue-integration.adoc (phase-3 section + rung-3b still-open), CHANGELOG, 6a2 STATE. NO new Idris needed — ResidueCell/reverseLinear already model rung 3a. STILL OPEN rung 3b: cross-handler residues via agent state — irreducibly partly RUNTIME (no static knowledge whether the earlier handler fired; Idris takeForReverse returns Maybe), so it adds a residue cell in agent state + evaluator Holding/Spent + bridge lemma. Pushed to claude/echo-residue-phase3-named → draft PR. Billing may still gate CI (account-owner action); verified locally. [2026-06-15 18:13:25] Session continued (in-site, billing still blocked): HARDEN + GATE on branch claude/gate-l10-proofs off main (post-#42-merge). User asked whether the CI billing block could be solved via the hyperpolymath/bag-of-actions repo; investigated (search_repositories + WebFetch of its public README): bag-of-actions is an early-stage Elixir/Zig/WASM distributed-continuation runtime ("mobile continuations / Batons"), NOT a GitHub Actions runner — no Actions integration, no webhook/job scheduling, no arbitrary-task CLI. Cannot run 007's CI; also can't add it to MCP scope (no add_repo this session). Reported; user directed "continue in site." Chose (via AskUserQuestion) "Harden + gate what landed". Delivered: (1) Gated the L10 proofs in audits/canonical-proof-suite/MANIFEST.a2ml — new 'language' domain, L1=EchoResidue.idr (headline reverseAfterIrreversibleIllTyped), L2=EchoResidueLinear.idr (headline reverseLinear); 37 entries total, paren-balanced (490/490), runner awk parses both with correct prover/path/symbol. CRITICAL fix: scan_banned uses grep -qF (substring, whole file) so the two files' own "ZERO believe_me / assert_total / sorry" disclaimer comments would have false-flagged them as stub — reworded all 4 comment lines to "no escape hatches" phrasing (meaning preserved, banned tokens gone). Verified runner-style (the runner cd's into dirname + checks basename, so module EchoResidue matches EchoResidue.idr — my first repo-root test wrongly failed on module-name-vs-path): both exit 0, banned-scan 0 hits, verify_idris2_symbol sig+clause PASS for both headlines. Did NOT regenerate REPORT.a2ml locally (coqc 8.18 can't parse From Stdlib → would falsely downgrade the ~30 rocq entries that need Rocq 9; nightly CI regenerates with full toolchain). (2) New e2e example examples/named_reversibility.007 (agent NamedReversal, on receive, reversible as undo { } + reverse undo in one handler) — built oo7 and ran all three e2e sections: parse PASS, check PASS ("type check passed"), run PASS. CHANGELOG + 6a2 STATE updated; A2ML 6a2 validate clean. Pushing to claude/gate-l10-proofs → draft PR. CI remains billing-blocked (maintainer admin-merges, as with #40/#41/#42); everything verified locally. + +[2026-06-18 01:42:28] Added `just gate` — one-command billing-independent local green-check (branch claude/just-gate-local-ci off main). Context: 007 is a PRIVATE repo (confirmed via GitHub API: visibility=private, "Private while dual-use safety/proof/release boundaries mature"), so its GitHub-hosted Actions runs on the owner's GitHub Pro INCLUDED minutes (3,000/mo) — that IS the right mechanism; the instant-reject-404 block is a billing-settings state (exhausted included minutes and/or $0 spending limit / payment), fixable owner-side in Settings → Billing (raise spending limit to allow paid overage, or wait for monthly reset). Self-hosted runners are the free fallback (exempt from the hosted-minute spending cap) but need an always-on host the user controls — overkill if the included minutes are simply topped up. bag-of-actions re-investigated from the actual repo (raw README + file tree, not the earlier small-model summary): it's a Zig/Elixir continuation runtime whose only entrypoints are `bag_of_actions init`/`run` of its own demo; its ci-checks.exs are the checks it runs on ITSELF; no runner/executor/task-submission interface for other repos — confirmed it cannot run 007's CI. Deliverable: new Justfile `gate` recipe (named `gate` to avoid the existing `ci`=build/test/lint/verify and `check`=fmt/lint/test). Runs rustfmt + clippy + cargo test + grammar-check + verify-harvard + e2e + idris2 --check(all 12 proofs); self-skips a2ml (validate-a2ml.sh not on PATH locally) and assail (panic-attack absent); per-stage PASS/FAIL/SKIP summary + nonzero exit on FAIL. Ran end-to-end: GREEN (7 PASS, 2 SKIP, 0 FAIL; e2e internal 49 pass/0 fail/17 intentional-skip). CHANGELOG updated. CI still billing-blocked (maintainer admin-merges #34/#41/#42/#43); local gate is the authoritative substitute. Pushing → draft PR. diff --git a/CHANGELOG.md b/CHANGELOG.md index 2096d7c..2dd6e9e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -10,6 +10,7 @@ All notable changes to this project will be documented in this file. - **Layer 10 phase 2 — the residue is a linear undo-capability.** The checker's residue stack now carries `Linear>` (was a bare `Echo`), making the consumed-once discipline explicit in the type. Discipline: *affine capability, linear consumption* — a given reversal log is consumed at most once (a double `reverse` of one residue is rejected) yet a `reversible` block need not be paired with a `reverse` (an un-reversed residue is **not** an error; reversibility is a capability, usually unused). Mechanised in `proofs/idris2/EchoResidueLinear.idr` (`reverseLinear` consumes `(1 e : Echo f y)`; `ResidueCell` Holding/Spent = the residue as agent state; `holdingReverses`/`spentDoesNotReverse`; `%default total`, zero `believe_me`, `idris2 --check` clean). 3 new typechecker tests (883 `oo7-core` lib tests passing). Remaining rung: cross-handler *named* residues (residue-binding grammar syntax, Harvard-guarded — kept separate). Spec/docs updated in lockstep. - **Layer 10 phase 3 (rung 3a) — named residues within a body.** New surface syntax `reversible as { … }` binds the echo residue to a name; `reverse ` replays it (anonymous `reversible {…}`/`reverse {…}` unchanged). The named residue is tracked per body as a `Holding(Linear>)` cell that `reverse` transitions to `Spent` — the static mirror of `ResidueCell` (Holding/Spent) in `EchoResidueLinear.idr`. Same affine/linear discipline: double `reverse ` is rejected (cell already `Spent`); a never-replayed binding is **not** an error; named residues are scoped per body (no cross-body leak). Additive AST variants `ReversibleAs`/`ReverseNamed` (existing variants untouched); grammar (`grammar.pest` + `spec/grammar.ebnf`), parser, typechecker (`named_residues` map + per-function/handler isolation), and the eval/codegen/formatter/dual-ast/metainterpreter/CFG/oracle pipeline all threaded. 2 parser + 5 typechecker tests (890 `oo7-core` lib tests passing; fmt clean, clippy `-D warnings` exit 0). Remaining rung 3b: cross-handler residues through agent state (irreducibly partly runtime — `takeForReverse : Maybe`). Spec: TYPE-SYSTEM-SPEC §11b.5; docs `docs/echo-residue-integration.adoc`. - **Layer 10 proofs gated in the canonical proof suite.** The L10 echo-types proofs are now first-class suite entries (`audits/canonical-proof-suite/MANIFEST.a2ml`), gated nightly like the M/S/E classics: new `language` domain `L1` (`proofs/idris2/EchoResidue.idr`, headline `reverseAfterIrreversibleIllTyped`) and `L2` (`proofs/idris2/EchoResidueLinear.idr`, headline `reverseLinear`) — 37 entries total. Each gets the runner's banned-construct scan + `idris2 --check` + symbol-defined check; both verified locally (exit 0, zero banned constructs). The two files' "zero believe_me/assert_total/sorry" disclaimer comments were reworded so the substring banned-scan doesn't false-positive on the very tokens they disclaim. New end-to-end example `examples/named_reversibility.007` exercises `reversible as`/`reverse ` through the full pipeline (parse + typecheck + run all pass). +- **`just gate` — one-command, billing-independent local green-check.** Runs every locally-faithful CI stage in sequence (rustfmt, clippy, `cargo test`, grammar-check, verify-harvard, e2e, `idris2 --check` of all 12 Idris proofs), continues past failures, and prints a per-stage PASS/FAIL/SKIP summary with a non-zero exit on any FAIL. 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 external manifest/security scans stay CI/nightly-only. Verified GREEN on `main`. Distinct from `just ci` (build/test/lint/verify simulation) and `just check` (fast fmt/lint/test pre-commit). - **752 tests** (up from 207 at 0.5.0). CRG-C achieved 2026-04-04 for `oo7-core`. - **31 multi-language backends** via `mk2_bridge::create_backend_registry()`. Real dispatch to `elixir`, `idris2`, `gleam`, `rescript`, `nickel`, `guile`, `psql`, etc. Tier-5 coprocessor backends (CUDA/Vulkan/Metal/OpenCL/FPGA/TPU/DSP) do phase-1 device discovery with documented "kernel launch is future work" status. - **Metainterpreter** (`metainterpreter.rs`, ~3,075 LOC): reify/reflect/step/replay, four modes, 40 inline tests, 18 benches. diff --git a/Justfile b/Justfile index 327d43c..7f52ad9 100644 --- a/Justfile +++ b/Justfile @@ -159,6 +159,61 @@ fmt-check: check: fmt-check lint test @echo "All checks passed." +# Full local gate — the billing-independent "is it green?" in one command. +# Runs every locally-faithful CI check in sequence, CONTINUES past failures, +# and prints a per-stage PASS/FAIL/SKIP summary (non-zero exit if any FAIL). +# Stages that need a specific toolchain (idris2) or an external GitHub action +# (A2ML validator, etc.) self-SKIP with a notice rather than failing, so this +# runs anywhere. Rocq canonical-proof-suite (needs Rocq 9) and the external +# manifest/security scans (K9 / Groove / openssf / Hypatia / eclexiaiser) +# remain CI/nightly-only — there is no local validator for them in-repo. +# Distinct from `ci` (build/test/lint/verify) and `check` (fast fmt/lint/test). +# One command; the full local green-check with a per-stage PASS/FAIL summary. +gate: + #!/usr/bin/env bash + set -uo pipefail + fail=0 + declare -a results + run() { + local name="$1"; shift + echo; echo "──▶ ${name}" + if "$@"; then results+=(" ✓ PASS ${name}") + else results+=(" ✗ FAIL ${name}"); fail=1; fi + } + skip() { echo; echo "──▶ $1 — SKIP ($2)"; results+=(" ⊘ SKIP $1 ($2)"); } + + run "rustfmt" cargo fmt --all -- --check + run "clippy" cargo clippy --workspace -- -D warnings + run "test" cargo test --workspace + run "grammar-check" just grammar-check + run "verify-harvard" just verify-harvard + run "e2e" bash tests/e2e.sh + + if command -v idris2 >/dev/null 2>&1; then + run "idris2-proofs" bash -c 'for f in proofs/idris2/*.idr; do ( cd "$(dirname "$f")" && idris2 --check "$(basename "$f")" ) || { echo " failed: $f"; exit 1; }; done' + else + skip "idris2-proofs" "idris2 not on PATH" + fi + + if command -v validate-a2ml.sh >/dev/null 2>&1; then + run "a2ml" bash -c 'INPUT_PATH=.machine_readable/6a2 INPUT_STRICT=false validate-a2ml.sh' + else + skip "a2ml" "validate-a2ml.sh not on PATH (CI uses hyperpolymath/a2ml-validate-action)" + fi + + if command -v panic-attack >/dev/null 2>&1; then + run "assail" panic-attack assail . + else + skip "assail" "panic-attack not installed" + fi + + echo; echo "═══════════════ local CI summary ═══════════════" + printf '%s\n' "${results[@]}" + echo "─────────────────────────────────────────────────" + echo "CI/nightly-only (not run here): rocq canonical-proof-suite (needs" + echo "Rocq 9); external manifest/security scans (no local validator)." + if [ "${fail}" -eq 0 ]; then echo "RESULT: GREEN ✓"; else echo "RESULT: RED ✗ (see FAIL above)"; exit 1; fi + # Run panic-attacker pre-commit scan (RSR mandatory before commit) assail: #!/usr/bin/env bash