ArghDA M4 follow-on: Idris2 .ipkg-declared roots#41
Merged
Conversation
`discover_roots` for Idris2 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` are consulted) and resolves each `main` module against candidate source roots. ## Verified (ran, not inferred) - `cargo test` → 127 passing, 0 failed (+1 integration: ipkg `main = App` discovered + its cone wired; +2 unit: sourcedir/comment resolution, and a no-resolvable-main → empty). - clippy -D warnings, fmt, SPDX clean. - Dogfooded: `reason --backend idris2` over an ipkg fixture → crt_roots ['App'], App + Helper wired. - STATE.a2ml: M4 now 95% (remaining: totality-hole `?name` + per-def `partial` lint). 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 10:17
hyperpolymath
added a commit
that referenced
this pull request
Jul 1, 2026
) ## What The Flying-Logic reasoning graph can now source **real prover verdicts from a four-state workspace's `proven/` state** without re-running any tool, and demote a **stale-proven** node back to `unknown`. Honest by construction — a verdict only ever comes from a recorded promotion, and staleness always dominates a stale `Proven`. This is the last of the three refinement follow-ons (M4 `.ipkg` roots #41, M6 axiom audit #42, M3 workspace verdicts). ## How - **`reason::workspace_verdicts(dag, proven, stale) -> (verdicts, stale)`** — a pure mapping (no I/O, unit-testable): a node whose file basename is in the workspace's `proven/` set → `Proven`; if that same file is stale (content/closure hash changed since promotion) it is added to the returned stale set, so the existing demote-only fold lowers it to `Unknown`. Matched by file basename (documented collision caveat). Re-exported from `lib.rs`. - **`arghda reason <path> --workspace <ws>`** — reads the proven + stale-proven basename sets off the workspace (`Workspace::list(Proven)` / `Workspace::stale_proven`) and feeds them into `workspace_verdicts`. `--check` stays authoritative: a fresh typecheck overrides the workspace verdict and clears staleness for that node. - **Honest evidence strings** — `"prover: proven"` for a fresh promotion; `"prover: proven; stale: closure hash changed"` for a demoted stale one. ## Verification (actually run) - `cargo fmt --check` — clean - `cargo clippy --all-targets -- -D warnings` — clean - `cargo test` — **130 pass** (+1 reason unit: proven lights the cone, stale demotes) - `bash scripts/check-spdx.sh .` — OK **Dogfooded end-to-end** on a real workspace + Agda source tree: - Scenario A (fresh proven leaf): `Good` → `effective: proven` (`"prover: proven"`); un-proven root `All` → `unknown`. - Scenario B (proven file edited on disk → stale): `Good` demoted to `unknown` with `"prover: proven; stale: closure hash changed"`. ## Scope Additive only. `M3` base was already 100%; this refinement wires the reasoning graph to the triage workspace's ground truth. No change to the `reason/0.1` JSON contract keys. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7 --- _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
2 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.
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_rootsnow unions two conventions:.ipkgmain = <Module>— the package's executable entry, resolved to its.idrfile (honouring an optional quotedsourcedir;--comments stripped; first existing candidate base wins). The entry needn't be literallyMain.idr— e.g.main = AppfindsApp.idr.Main.idr— the bare-tree fallback (unchanged).ipkg_main_roots()parses the.ipkgkey = valuefields (onlymainandsourcedir/source-dirconsulted) and resolves eachmainmodule against candidate source roots.Verified (ran, not inferred)
cargo test→ 127 passing, 0 failed (+1 integration:main = Appdiscovered + its cone wired; +2 unit: sourcedir/comment resolution; no-resolvable-main → empty).reason --backend idris2over an.ipkgfixture →crt_roots: ['App'], App + Helper wired.Status
M4 now ~95% (remaining: totality-hole
?name+ per-defpartiallint). Next follow-ons: M6 (lake-env +#print axiomsaudit), M3 (workspace-fed verdicts + staleness).Generated by Claude Code