From 44332e58555423833169b56445703569fb153642 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 17 Jul 2026 04:47:02 +0000 Subject: [PATCH] =?UTF-8?q?ArghDA=20M9=20follow-on:=20Isabelle=20session-q?= =?UTF-8?q?ualified=20imports=20(M9=20=E2=86=92=2098%)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A theory that imports from another session — `imports "HOL-Library.FuncSet"` — is now checkable. (Flat sibling imports already worked: the adapter stages every sibling `.thy` into the session, so `imports Main Foo` on a sibling `Foo` already resolved — verified before touching anything.) The gap was session-qualified imports: the generated ROOT said `= HOL +` with no route to `HOL-Library`, so the build errored "Cannot load theory". Fix: `session_prefixes` scans all staged theories' `imports` clauses for qualified `"Session.Theory"` forms (session = the segment before the first `.`; Isabelle session names are dot-free) and emits a `sessions "" …` clause in the generated ROOT, so `isabelle build` pulls those sessions' heaps. The distribution session heaps ship prebuilt, so the build stays fast (~15 s). Verification (actually run): cargo fmt --check, clippy -D warnings, cargo test (176 pass, +1 `session_prefixes` unit), check-spdx.sh — all green. Dogfooded vs real Isabelle2025: `Q.thy` importing `"HOL-Library.FuncSet"` and using its Pi-notation → proven (was an error pre-fix); flat-sibling regression (`Bar` imports sibling `Foo`) → still proven. Residual: a project with its OWN multi-session ROOT (a locally-defined session importing another local session's theories) — niche; single-theory, flat-sibling and distribution-session-qualified imports all work. This completes the heavy-tail completion cuts (Coq dep-ordering, Mizar cross-refs, Isabelle session-qualified imports). Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7 --- .machine_readable/6a2/STATE.a2ml | 27 ++++++++++-- src/prover/isabelle.rs | 74 ++++++++++++++++++++++++++++---- 2 files changed, 89 insertions(+), 12 deletions(-) diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 258e69c..378ac37 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.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 "" …` 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 diff --git a/src/prover/isabelle.rs b/src/prover/isabelle.rs index 145da98..9cd55e1 100644 --- a/src/prover/isabelle.rs +++ b/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 = 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 { 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 { + 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!(