ArghDA M4 follow-on: Idris2 .ipkg-declared roots

.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 = <Module>` 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

src/prover/idris2.rs

@@ -126,23 +126,26 @@ impl Backend for Idris2 {
     }
 
     fn discover_roots(&self, include_root: &Path) -> Vec<PathBuf> {
-        // 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 = <Module>` — 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 = <Module>` 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<PathBuf> {
+    let Ok(contents) = fs::read_to_string(ipkg) else {
+        return Vec::new();
+    };
+    let mut mains: Vec<String> = Vec::new();
+    let mut sourcedir: Option<String> = 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<PathBuf> = 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());
+    }
 }

tests/fixtures/idris2-pkg/App.idr

@@ -0,0 +1,6 @@
+module App
+
+import Helper
+
+main : IO ()
+main = putStrLn message

tests/fixtures/idris2-pkg/Helper.idr

@@ -0,0 +1,5 @@
+module Helper
+
+export
+message : String
+message = "hi"

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

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<Box<dyn LintRule>> {
     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<String> = 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"
+    );
+}