ArghDA M9 follow-on: Isabelle session-qualified imports (M9 → 98%)

.machine_readable/6a2/STATE.a2ml

@@ -49,7 +49,7 @@ milestones = [
   { name = "M6: Lean4 adapter (lake build + #print axioms audit)", completion = 100 },
   { name = "M7: Echidna dispatch seam (optional route to orchestrator :8090, same Outcome)", completion = 70 },
   { name = "M8: Coq/Rocq adapter (--heavy provisioning; Section-aware postulate classifier)", completion = 97 },
-  { name = "M9: Isabelle adapter (--heavy; dogfood tropical-resource-typing .thy)", completion = 90 },
+  { name = "M9: Isabelle adapter (--heavy; dogfood tropical-resource-typing .thy)", completion = 98 },
   { name = "M10: Mizar adapter (detect-only first; highest uncertainty)", completion = 95 },
   { name = "M11: studio JSON freeze (reason/0.1) + Groove manifest", completion = 100 },
 ]
@@ -114,6 +114,25 @@ milestones = [
 # --backend idris2` over an ipkg fixture → crt_roots ['App'], App+Helper wired.
 # M4 now 95% (remaining: totality-hole `?name` + per-def `partial` lint).
 #
+# M9 FOLLOW-ON landed 2026-07-01 (M9 90% → 98%): Isabelle session-qualified
+# imports. GROUND-TRUTHED FIRST (the important step): FLAT sibling imports were
+# ALREADY working — the adapter copies every sibling .thy into the generated
+# session, so `imports Main Foo` (Foo a sibling) already resolved (dogfooded:
+# Bar imports Foo → proven). The genuine gap was SESSION-QUALIFIED imports like
+# `imports "HOL-Library.FuncSet"` (a theory from another SESSION): the generated
+# ROOT said `= HOL +` with no way to reach HOL-Library → "Cannot load theory"
+# error. Fix: `session_prefixes` scans all staged theories' imports clauses for
+# qualified `"Session.Theory"` forms (session = segment before the first `.`;
+# Isabelle session names are dot-free) and emits a `sessions "<S>" …` clause in
+# the ROOT, so `isabelle build` pulls those sessions' heaps. Ground-truthed the
+# HOL-Library heap ships prebuilt (dry-run clean), so the build is ~15 s.
+# 176 tests (+1 session_prefixes unit). DOGFOODED vs real Isabelle2025: Q.thy
+# `imports "HOL-Library.FuncSet"` using Pi-notation → proven (was error pre-fix);
+# flat-sibling regression (Bar imports Foo) → still proven. Residual 2%: a
+# project with its OWN multi-session ROOT (a locally-defined session importing
+# another local session's theories) — niche; single-theory + flat-sibling +
+# distribution-session-qualified all work.
+#
 # M10 FOLLOW-ON landed 2026-07-01 (M10 85% → 95%): Mizar local-article cross-
 # references. Was: `theorems X;` on a sibling article errored (X not in the
 # library). GROUND-TRUTHED the export pipeline vs real Mizar 8.1.15: to Require
@@ -473,7 +492,7 @@ actions = [
   "M9 (Isabelle): DONE (90%) — Isabelle2025 provisioned + adapter built + dogfooded (proven/admitted/postulated/error) via session-build; ROOT-based roots, imports-clause edges. Remaining: session-qualified imports + dependency-ordered multi-session builds.",
   "M10 (Mizar): DONE (85%) — turned out to be a REAL verify, not detect-only: static i386 verifier runs on x86_64; provisioned + adapter (accom+verifier+.err) + dogfooded (proven/error). HEAVY TAIL M8-M10 COMPLETE. Remaining: local-article prel export.",
   "M7 client INVESTIGATED 2026-07-01 → BLOCKED (stub stays): no confirmed Echidna HTTP contract exists (dispatch.rs says API unconfirmed; ECOSYSTEM.a2ml gives no endpoints/schema; the echidna repo is out of this session's access scope). Building a client would mean inventing an unverifiable contract — forbidden. Unblock: a published Echidna API + a reachable instance to dogfood; then wire Dispatch::run behind a cargo feature. ROADMAP TERMINUS — all tractable items done; M7's client is the sole residual, externally blocked.",
-  "HEAVY-TAIL COMPLETION CUTS (owner asked 2026-07-01, foundation-first, one PR each, real-tool dogfood): [DONE] Coq dependency-ordered compilation (M8 90→97%); [DONE] Mizar local-article cross-refs via accom/verifier/exporter/transfer export pipeline (M10 85→95%, theorems path dogfooded); [NEXT/LAST] Isabelle session-qualified imports + multi-session builds (M9 90→~100%). Residual after: Coq _CoqProject custom -Q/-R prefixes (3%); Mizar definitions/notations cross-refs not separately dogfooded (5%); arghda-studio visual layer (separate repo, out of this session's scope; AffineScript).",
+  "HEAVY-TAIL COMPLETION CUTS COMPLETE (owner asked 2026-07-01, foundation-first, one PR each, real-tool dogfood): [DONE] Coq dependency-ordered compilation (M8 90→97%); [DONE] Mizar local-article cross-refs via export pipeline (M10 85→95%); [DONE] Isabelle session-qualified imports (M9 90→98%). All three heavy provers now handle multi-file/cross-session projects, dogfooded against their real tools. Small residuals (owner's call, none blocking): Coq _CoqProject custom -Q/-R prefixes (3%); Mizar definitions/notations cross-refs not separately dogfooded (5%); Isabelle own-multi-session-ROOT projects (2%). Out of this session's scope: arghda-studio visual layer (separate repo, AffineScript).",
 ]
 
 [maintenance-status]
@@ -482,7 +501,9 @@ 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-M10-crossref: 132 lib + 43 integration = 175 tests pass. M10 Mizar
+# post-M9-sessionqual: 133 lib + 43 integration = 176 tests pass. M9 Isabelle
+# session-qualified imports dogfooded vs real Isabelle2025 (imports
+# "HOL-Library.FuncSet" → proven; flat sibling still proven). M10 Mizar
 # local-article cross-refs dogfooded vs real Mizar 8.1.15 (y requires local x →
 # proven; broken dep → dependent error). M8 dependency-ordered Coq compilation
 # dogfooded vs real coqc 8.18.0 (A←B←C chain → all proven; transitive admit

src/prover/isabelle.rs

@@ -23,11 +23,14 @@
 //! Theory names map to files like every other assistant (`Foo` ↔ `Foo.thy`),
 //! so [`crate::graph::module_name_of`] is reused (a flat tree's dotted name is
 //! just the theory stem). Import edges come from the header `imports` clause
-//! (`theory Foo imports Bar Baz begin`). Roots are the theories a `ROOT` file
-//! lists under a `theories` section — the genuine Isabelle entry-point
-//! convention (analogue of Agda's `All.agda`). Session-qualified / relative-
-//! path imports and dependency-ordered multi-session builds are documented
-//! follow-ons.
+//! (`theory Foo imports Bar Baz begin`). Flat in-tree imports resolve because
+//! every sibling `.thy` is staged into the session; **session-qualified**
+//! imports (`imports "HOL-Library.FuncSet"`) resolve too — [`session_prefixes`]
+//! collects each qualified import's session (`HOL-Library`) across the staged
+//! theories and emits a `sessions` clause in the generated ROOT, so
+//! `isabelle build` pulls those sessions' heaps. Roots are the theories a
+//! `ROOT` file lists under a `theories` section — the genuine Isabelle
+//! entry-point convention (analogue of Agda's `All.agda`).
 
 use super::{probe_tool_arg, Backend, BackendKind, Outcome, Probe, Verdict};
 use crate::graph;
@@ -94,8 +97,11 @@ impl Backend for Isabelle {
             return Ok(Outcome::unavailable(BackendKind::Assistant));
         }
 
-        // Copy every sibling `.thy` (basename) so in-tree imports resolve,
-        // then ensure the target is present (it may sit outside include_root).
+        // Copy every sibling `.thy` (basename) so flat in-tree imports resolve,
+        // and collect any session-qualified import prefixes (`"HOL-Library.X"`
+        // → session `HOL-Library`) across all staged theories so they can be
+        // declared in the ROOT's `sessions` clause.
+        let mut sessions: std::collections::BTreeSet<String> = std::collections::BTreeSet::new();
         for entry in WalkDir::new(include_root)
             .into_iter()
             .filter_map(|e| e.ok())
@@ -105,11 +111,26 @@ impl Backend for Isabelle {
                 if let Some(name) = p.file_name() {
                     let _ = fs::copy(p, session_dir.join(name));
                 }
+                if let Ok(s) = fs::read_to_string(p) {
+                    sessions.extend(session_prefixes(&s));
+                }
             }
         }
         let _ = fs::copy(file, session_dir.join(format!("{stem}.thy")));
-
-        let root = format!("session \"ArghdaCheck\" = \"HOL\" +\n  theories\n    {stem}\n");
+        let src_for_sessions = fs::read_to_string(file).unwrap_or_default();
+        sessions.extend(session_prefixes(&src_for_sessions));
+
+        // Generate the ROOT: base HOL, a `sessions` clause for every qualified
+        // import prefix (so `isabelle build` can pull those sessions), then the
+        // target theory.
+        let mut root = String::from("session \"ArghdaCheck\" = \"HOL\" +\n");
+        if !sessions.is_empty() {
+            root.push_str("  sessions\n");
+            for s in &sessions {
+                root.push_str(&format!("    \"{s}\"\n"));
+            }
+        }
+        root.push_str(&format!("  theories\n    {stem}\n"));
         if fs::write(session_dir.join("ROOT"), root).is_err() {
             let _ = fs::remove_dir_all(&session_dir);
             return Ok(Outcome::unavailable(BackendKind::Assistant));
@@ -241,6 +262,26 @@ fn parse_imports(contents: &str) -> Vec<String> {
     out
 }
 
+/// The session qualifiers of a theory's `imports` clause: for each
+/// session-qualified import `"Session.Theory"` (a dotted name — Isabelle
+/// session names are themselves dot-free, so the session is the segment before
+/// the first `.`), yield `Session`. Bare theory names (`Main`, a flat sibling)
+/// have no dot and contribute nothing. These become the ROOT's `sessions`
+/// clause so `isabelle build` can pull the imported session's heap.
+fn session_prefixes(contents: &str) -> Vec<String> {
+    parse_imports(contents)
+        .into_iter()
+        .filter_map(|imp| {
+            let (pre, rest) = imp.split_once('.')?;
+            if pre.is_empty() || rest.is_empty() {
+                None
+            } else {
+                Some(pre.to_string())
+            }
+        })
+        .collect()
+}
+
 /// Normalise an `imports`/`ROOT` theory token to a bare theory name: strip
 /// quotes, then take the final path segment (`"../Other/Baz"` → `Baz`).
 fn theory_token(tok: &str) -> String {
@@ -353,6 +394,21 @@ mod tests {
         assert!(!imports.iter().any(|i| i == "x"));
     }
 
+    #[test]
+    fn session_prefixes_only_from_qualified_imports() {
+        // A session-qualified import contributes its session; bare theory names
+        // (Main, a flat sibling) do not.
+        let thy = "theory Q\n  imports Main Foo \"HOL-Library.FuncSet\" \"HOL-Analysis.Derivative\"\nbegin\nend\n";
+        let mut ps = session_prefixes(thy);
+        ps.sort();
+        assert_eq!(
+            ps,
+            vec!["HOL-Analysis".to_string(), "HOL-Library".to_string()]
+        );
+        // No qualified imports ⇒ no sessions.
+        assert!(session_prefixes("theory T imports Main Bar begin end\n").is_empty());
+    }
+
     #[test]
     fn verdict_is_honest_about_sorry_axiom_and_clean() {
         assert_eq!(