diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index c9cd696..6001e0c 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -44,7 +44,7 @@ milestones = [ { name = "M1: Backend trait (Assistant|Solver kinds; Outcome/Verdict); agda.rs -> prover/agda.rs; graph/dag take &dyn Backend (pure refactor, 50 tests stay green)", completion = 100 }, { name = "M2: Cubical-Agda variant (Agda::cubical(), --cubical --safe island)", completion = 100 }, { name = "M3: Flying-Logic reasoning graph (src/reason: And|Or juncts, demote-only cycle-safe Verdict propagation, additive studio JSON)", completion = 100 }, - { name = "M4: Idris2 adapter (core/ABI language: .ipkg/--check/totality; escape-hatches)", completion = 90 }, + { name = "M4: Idris2 adapter (core/ABI language: .ipkg/--check/totality; escape-hatches)", completion = 95 }, { name = "M5: SMT solver backends (Z3, CVC5): SMT-LIB2 -> sat/unsat/unknown -> Verdict", completion = 100 }, { name = "M6: Lean4 adapter (lake build + #print axioms audit)", completion = 85 }, { name = "M7: Echidna dispatch seam (optional route to orchestrator :8090, same Outcome)", completion = 70 }, @@ -60,6 +60,30 @@ milestones = [ # Remaining M0: `arghda doctor` Rust subcommand (interim: `just doctor` shells # the script's --verify-only table). # +# Follow-on round (refinement, 2026-07-01, after the engine spine): +# +# CI FIX (arghda-core#40 was auto-merge-blocked on "Waiting for Code Scanning +# results. Code Scanning may not be configured for the target branch"): arghda- +# core was EXTRACTED from echo-types, not instantiated from rsr-template-repo, +# so it never inherited the template's codeql.yml — yet main's branch protection +# requires code-scanning. Earlier PRs merged only because the owner merged +# manually; auto-merge enforces strictly. FIX (at source): restored the +# canonical estate .github/workflows/codeql.yml verbatim (language: actions, +# build-mode none, SHA-pinned; same file rsr-template-repo + cicd-squabbler run +# green). Triggers on pull_request (PR gets a run) + push:[main] (establishes the +# baseline). Landed via #40; the advanced-security bot confirmed "Code Scanning +# has recently been set up". Permanent — future PRs satisfy the gate +# automatically. NB the template is fine; only extraction-origin repos drift. +# +# M4 FOLLOW-ON landed 2026-07-01: Idris2 `.ipkg`-declared roots. discover_roots +# now unions (a) `.ipkg` `main = ` resolved to its .idr (honouring an +# optional quoted `sourcedir`; `--` comments stripped; first existing candidate +# base wins) with (b) the Main.idr fallback. So an executable entry named other +# than Main.idr (e.g. `main = App`) is found. 127 tests (+1 integration ipkg-main +# +2 unit ipkg-parser incl. sourcedir + no-resolvable-main). Dogfooded: `reason +# --backend idris2` over an ipkg fixture → crt_roots ['App'], App+Helper wired. +# M4 now 95% (remaining: totality-hole `?name` + per-def `partial` lint). +# # M7 landed 2026-07-01 (70%): the Echidna dispatch seam — completes the # engine-spine deliverable (M0-M7 + M11). src/dispatch.rs: `Dispatch { Local, # Echidna { base_url } }` + `run(backend, file, include_root) -> Outcome` @@ -219,7 +243,7 @@ actions = [ "ENGINE-SPINE DELIVERABLE COMPLETE: M0-M7 + M11 all landed. v0.1 spec closed. Six backends (agda, agda-cubical, idris2, lean4 Assistant; z3, cvc5 Solver) + reasoning graph + doctor + groove + dispatch seam. Remaining work is refinement + the heavy tail:", "M7 follow-on: the real Echidna orchestrator HTTP client (feature-gated), once Echidna's API is confirmed — only Dispatch::run changes.", "M6 follow-on: lake-env/LEAN_PATH multi-file resolution; per-decl #print axioms audit to promote Unknown→Proven.", - "M4 follow-on: .ipkg-declared roots; totality-hole (?name) + per-def `partial` lint.", + "M4 follow-on: .ipkg-declared roots DONE; remaining = totality-hole (?name) + per-def `partial` lint.", "M3 follow-on: feed real verdicts into `reason` from a workspace `proven/` state + wire staleness from the content-hash closure (proven.rs).", "M8-M10 heavy tail (Coq/Rocq, Isabelle, Mizar) — gated on --heavy provisioning (Coq via opam ~1hr; Isabelle ~4GB; Mizar niche).", ] @@ -230,7 +254,8 @@ last-result = "pass" # unknown | pass | warn | fail open-warnings = 0 open-failures = 0 # `just check` (fmt-check + clippy -D warnings + build + test + SPDX) green -# post-M7: 91 lib + 33 integration = 124 tests pass. doctor/groove/dispatch +# post-M4-followon: 93 lib + 34 integration = 127 tests pass. codeql.yml added +# (code-scanning gate fix). doctor/groove/dispatch # dogfooded: 6/6 backends runnable; groove writes /.well-known/groove; --dispatch # local real, echidna honest-stub. All six backends dogfooded via real CLI: agda # + agda-cubical + idris2 + lean4 (Assistant), z3 + cvc5 (Solver). Dogfooded diff --git a/src/prover/idris2.rs b/src/prover/idris2.rs index 4cfe480..dbe75b3 100644 --- a/src/prover/idris2.rs +++ b/src/prover/idris2.rs @@ -126,23 +126,26 @@ impl Backend for Idris2 { } fn discover_roots(&self, include_root: &Path) -> Vec { - // Idris2 has no `All.agda`-style convention; the executable entry is - // `Main.idr`. (`.ipkg`-declared `main`/`modules` roots are a - // documented follow-on.) + // Two conventions, unioned: + // 1. `.ipkg`-declared `main = ` — the package's executable + // entry, resolved to its `.idr` file (needn't be `Main.idr`). + // 2. Any `Main.idr` — the bare-tree fallback. let mut roots = Vec::new(); for entry in WalkDir::new(include_root) .into_iter() .filter_map(|e| e.ok()) { let path = entry.path(); - if path.extension().and_then(|s| s.to_str()) != Some("idr") { - continue; - } - if path.file_name().and_then(|s| s.to_str()) == Some("Main.idr") { - roots.push(path.to_path_buf()); + match path.extension().and_then(|s| s.to_str()) { + Some("ipkg") => roots.extend(ipkg_main_roots(path, include_root)), + Some("idr") if path.file_name().and_then(|s| s.to_str()) == Some("Main.idr") => { + roots.push(path.to_path_buf()); + } + _ => {} } } roots.sort(); + roots.dedup(); roots } @@ -161,6 +164,56 @@ fn tail(s: &str, n: usize) -> String { lines[start..].join("\n") } +/// Resolve an Idris2 `.ipkg`'s `main = ` declaration(s) to the +/// module's `.idr` file, honouring an optional `sourcedir`. Returns the +/// resolved files that exist (first matching candidate base per `main`). +/// Non-`main` fields are ignored; `--` comments are stripped. +fn ipkg_main_roots(ipkg: &Path, include_root: &Path) -> Vec { + let Ok(contents) = fs::read_to_string(ipkg) else { + return Vec::new(); + }; + let mut mains: Vec = Vec::new(); + let mut sourcedir: Option = None; + for line in contents.lines() { + let code = line.split("--").next().unwrap_or(line); + if let Some((key, value)) = code.split_once('=') { + match key.trim() { + "main" => mains.push(value.trim().to_string()), + "sourcedir" | "source-dir" => { + sourcedir = Some(value.trim().trim_matches('"').trim().to_string()); + } + _ => {} + } + } + } + + let ipkg_dir = ipkg.parent().unwrap_or(include_root); + // Candidate source roots to resolve the main module against, in order. + let mut bases: Vec = Vec::new(); + if let Some(sd) = &sourcedir { + bases.push(ipkg_dir.join(sd)); + bases.push(include_root.join(sd)); + } + bases.push(ipkg_dir.to_path_buf()); + bases.push(include_root.to_path_buf()); + + let mut out = Vec::new(); + for m in &mains { + for base in &bases { + let mut p = base.clone(); + for part in m.split('.') { + p.push(part); + } + p.set_extension("idr"); + if p.is_file() { + out.push(p); + break; // first existing candidate wins + } + } + } + out +} + #[cfg(test)] mod tests { use super::*; @@ -217,4 +270,33 @@ mod tests { assert!(out.exit_code.is_none()); } } + + #[test] + fn ipkg_main_resolves_via_sourcedir_and_strips_comments() { + // main declared with a dotted module under a quoted sourcedir, plus a + // `--` comment and a distractor field — only the real main resolves. + let tmp = tempfile::tempdir().unwrap(); + let root = tmp.path(); + std::fs::create_dir_all(root.join("src/Cli")).unwrap(); + std::fs::write(root.join("src/Cli/App.idr"), "module Cli.App\n").unwrap(); + std::fs::write( + root.join("thing.ipkg"), + "package thing\n\ + -- main = NotThis (this line is a comment)\n\ + sourcedir = \"src\"\n\ + main = Cli.App\n\ + executable = thing\n", + ) + .unwrap(); + let roots = ipkg_main_roots(&root.join("thing.ipkg"), root); + assert_eq!(roots, vec![root.join("src/Cli/App.idr")]); + } + + #[test] + fn ipkg_with_no_resolvable_main_yields_nothing() { + let tmp = tempfile::tempdir().unwrap(); + let root = tmp.path(); + std::fs::write(root.join("x.ipkg"), "package x\nmain = Nope\n").unwrap(); + assert!(ipkg_main_roots(&root.join("x.ipkg"), root).is_empty()); + } } diff --git a/tests/fixtures/idris2-pkg/App.idr b/tests/fixtures/idris2-pkg/App.idr new file mode 100644 index 0000000..5fffbae --- /dev/null +++ b/tests/fixtures/idris2-pkg/App.idr @@ -0,0 +1,6 @@ +module App + +import Helper + +main : IO () +main = putStrLn message diff --git a/tests/fixtures/idris2-pkg/Helper.idr b/tests/fixtures/idris2-pkg/Helper.idr new file mode 100644 index 0000000..04ee403 --- /dev/null +++ b/tests/fixtures/idris2-pkg/Helper.idr @@ -0,0 +1,5 @@ +module Helper + +export +message : String +message = "hi" diff --git a/tests/fixtures/idris2-pkg/foo.ipkg b/tests/fixtures/idris2-pkg/foo.ipkg new file mode 100644 index 0000000..a4514e9 --- /dev/null +++ b/tests/fixtures/idris2-pkg/foo.ipkg @@ -0,0 +1,5 @@ +package foo +-- the executable entry module is App, not Main +main = App +executable = foo +depends = base diff --git a/tests/idris2.rs b/tests/idris2.rs index 85e725a..cd994ea 100644 --- a/tests/idris2.rs +++ b/tests/idris2.rs @@ -20,6 +20,14 @@ fn idris2_fixture() -> PathBuf { p } +fn idris2_pkg_fixture() -> PathBuf { + let mut p = PathBuf::from(env!("CARGO_MANIFEST_DIR")); + p.push("tests"); + p.push("fixtures"); + p.push("idris2-pkg"); + p +} + /// The graph path needs no lint rules; a typed empty pack. fn no_rules() -> Vec> { Vec::new() @@ -89,3 +97,37 @@ fn idris2_reason_graph_wires_the_main_cone() { assert!(wired("Data.Helper")); assert!(!wired("Orphan"), "Orphan must be unwired"); } + +#[test] +fn idris2_ipkg_main_is_discovered_as_a_root() { + // The `.ipkg` follow-on: `main = App` (NOT Main.idr) is resolved to + // App.idr as the CI root, and the App cone wires from it. + let root = idris2_pkg_fixture(); + let roots = Idris2.discover_roots(&root); + let names: Vec = roots + .iter() + .map(|p| p.file_name().unwrap().to_str().unwrap().to_string()) + .collect(); + assert_eq!( + names, + vec!["App.idr".to_string()], + "ipkg `main = App` must be discovered (there is no Main.idr)" + ); + + let dag = build_dag( + &root, + &roots, + &no_rules(), + DEFAULT_HEADLINE_PATTERN, + &Idris2, + ) + .unwrap(); + let doc = build_reason(dag, &Idris2, &BTreeMap::new(), &BTreeSet::new()); + assert_eq!(doc.crt_roots, vec!["App".to_string()]); + let wired = |id: &str| doc.nodes.iter().find(|n| n.id == id).unwrap().wired; + assert!(wired("App")); + assert!( + wired("Helper"), + "Helper is imported by the ipkg-declared main" + ); +}