ArghDA M7: Echidna dispatch seam — completes the engine-spine deliverable#40
Merged
Merged
Conversation
…able
The last piece of the engine-spine deliverable (M0-M7 + M11). A thin
indirection so a backend's check can route locally or (in future) to the
Echidna multi-prover orchestrator, returning the SAME Outcome contract.
- `src/dispatch.rs` — `Dispatch { Local, Echidna { base_url } }` +
`run(backend, file, include_root) -> Outcome`. Local = fully real
(delegates to `backend.check_file`). `Dispatch::parse` accepts
`local` / `echidna` / `echidna=<url>`.
- `src/main.rs` — `--dispatch local|echidna[=<url>]` wired on `check` and
`reason --check`.
## Honest-stub discipline
Echidna's orchestrator API is unconfirmed (it may not exist yet) and this
seam explicitly does not block on it. Rather than invent an unverifiable
HTTP contract and risk fabricating a verdict, the Echidna route returns
`available: false` / `Unavailable` with a clear reason — never a made-up
result (the same discipline as cicd-squabbler's "exits EX_UNAVAILABLE
rather than fake OK"). The value delivered now is the *seam*: one
indirection point with the Outcome contract preserved, so wiring the real
(feature-gated) client later touches only `Dispatch::run` — no backend or
caller changes.
## Verified (ran, not inferred)
- `cargo test` → 124 passing, 0 failed (+3 dispatch unit: parse;
echidna-never-fabricates; local-delegates).
- clippy -D warnings, fmt, SPDX clean.
- Dogfooded: `--dispatch local` z3 unsat → proven-eligible; `--dispatch
echidna` → backend-unavailable (honest); `--dispatch bogus` → clean error.
- STATE.a2ml: M7 = 70% (real orchestrator client is the follow-on);
completion 92%, maturity beta. The engine-spine deliverable is complete.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7
hyperpolymath
marked this pull request as ready for review
July 1, 2026 09:54
hyperpolymath
enabled auto-merge (squash)
July 1, 2026 09:54
… gate)
arghda-core's `main` branch protection requires Code Scanning results, but
the repo shipped no CodeQL workflow — so auto-merge waits forever
("Waiting for Code Scanning results. Code Scanning may not be configured
for the target branch"). Earlier PRs only merged because the owner merged
them manually; auto-merge enforces the gate strictly.
Root cause: arghda-core was EXTRACTED from echo-types rather than
instantiated from rsr-template-repo, so it never inherited the template's
`codeql.yml`. This restores the canonical estate workflow verbatim
(identical to rsr-template-repo + cicd-squabbler, which is green):
- `language: actions`, `build-mode: none` — the estate default; scans the
workflow files every repo has, avoiding the "no source files" failures
that `rust`/`javascript-typescript` extractors produce (CodeQL's Rust
support is limited). Per hypatia `codeql_language_matrix_mismatch`.
- Triggers on `push: [main]` (establishes the code-scanning BASELINE on the
target branch — the missing piece the error names) AND `pull_request`
(produces results on every PR). SHA-pinned actions.
Permanent fix: once this lands on `main`, the push-trigger run establishes
the baseline and every future PR's code-scanning gate is satisfied
automatically — no more manual-merge workaround.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7
|
You are seeing this message because GitHub Code Scanning has recently been set up for this repository, or this pull request contains the workflow file for the Code Scanning tool. What Enabling Code Scanning Means:
For more information about GitHub Code Scanning, check out the documentation. |
hyperpolymath
added a commit
that referenced
this pull request
Jul 1, 2026
First of the refinement follow-ons. Also the **live confirmation** that the code-scanning fix (`codeql.yml`, merged in #40) works — this PR should pass the Code Scanning gate and be auto-mergeable without a manual bootstrap. ## What Idris2 `discover_roots` now unions two conventions: 1. **`.ipkg` `main = <Module>`** — the package's executable entry, resolved to its `.idr` file (honouring an optional quoted `sourcedir`; `--` comments stripped; first existing candidate base wins). The entry needn't be literally `Main.idr` — e.g. `main = App` finds `App.idr`. 2. **Any `Main.idr`** — the bare-tree fallback (unchanged). `ipkg_main_roots()` parses the `.ipkg` `key = value` fields (only `main` and `sourcedir`/`source-dir` consulted) and resolves each `main` module against candidate source roots. ## Verified (ran, not inferred) - `cargo test` → **127 passing, 0 failed** (+1 integration: `main = App` discovered + its cone wired; +2 unit: sourcedir/comment resolution; no-resolvable-main → empty). - clippy -D warnings, fmt, SPDX clean. - **Dogfooded:** `reason --backend idris2` over an `.ipkg` fixture → `crt_roots: ['App']`, App + Helper wired. ## Status M4 now ~95% (remaining: totality-hole `?name` + per-def `partial` lint). Next follow-ons: M6 (lake-env + `#print axioms` audit), M3 (workspace-fed verdicts + staleness). --- _Generated by [Claude Code](https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7)_ Co-authored-by: Claude <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
CI fix included (unblocks the code-scanning merge gate)
Auto-merge on this PR was stuck on "Waiting for Code Scanning results. Code Scanning may not be configured for the target branch." Root cause: arghda-core was extracted from echo-types rather than instantiated from
rsr-template-repo, so it never inherited the template'scodeql.yml— yetmain's branch protection requires Code Scanning results. Earlier PRs merged only because the owner merged them manually; auto-merge enforces the gate strictly.This PR now also adds the canonical estate CodeQL workflow (
.github/workflows/codeql.yml, verbatim fromrsr-template-repo/ cicd-squabbler —language: actions,build-mode: none, SHA-pinned). It triggers onpull_request(so this PR gets a code-scanning run — visible asanalyze (actions, none)) andpush: [main](so once merged, the baseline the error names is established). Permanent fix: every future PR's code-scanning gate is then satisfied automatically — no more manual-merge workaround.What & why
The last piece of the engine-spine deliverable (M0–M7 + M11). A thin indirection so a backend's check can route locally (default, real) or — in future — to the Echidna multi-prover orchestrator (Zig-API, port 8090), returning the same
Outcomecontract either way.src/dispatch.rs—Dispatch { Local, Echidna { base_url } }+run(backend, file, include_root) -> Outcome.Localdelegates tobackend.check_file.Dispatch::parseacceptslocal/echidna/echidna=<url>.src/main.rs—--dispatch local|echidna[=<url>]wired oncheckandreason --check.Honest-stub discipline
Echidna's orchestrator API is unconfirmed (it may not exist yet) and this seam explicitly does not block on it. Rather than invent an unverifiable HTTP contract and risk fabricating a verdict, the Echidna route returns
available: false/Unavailablewith a clear reason — never a made-up result. The value delivered now is the seam: one indirection point with theOutcomecontract preserved, so wiring the real (feature-gated) client later touches onlyDispatch::run.Verified (ran, not inferred)
cargo test→ 124 passing, 0 failed (+3 dispatch unit). clippy -D warnings, fmt, SPDX clean.--dispatch localz3 unsat →proven-eligible;--dispatch echidna→backend-unavailable(honest);--dispatch bogus→ clean error.Milestone status — engine spine complete
M0–M7 + M11 all landed; the v0.1 spec is closed. Six backends across both interaction models, the honest reasoning graph, doctor, Groove discovery, and the dispatch seam. STATE bumped to 92% / beta. Remaining is refinement (M3/M4/M6/M7 follow-ons) and the heavy-prover tail (M8–M10,
--heavy).Generated by Claude Code