ArghDA M9: Isabelle/HOL adapter — second heavy-tail backend (foundation-first)

Provisioned Isabelle2025 (1.08 GB tarball, HOL heap prebuilt) BEFORE the
adapter, ground-truthed the invocation, then built and dogfooded against the
real tool. arghda is now an eight-backend prover-parametric workspace.

Adapter (src/prover/isabelle.rs, `Isabelle`):
- Assistant kind, extensions [thy], command `isabelle`.
- Isabelle is session-based (no single-file --check), so check_file generates a
  throwaway session: copies the target .thy + sibling .thy files into a temp
  dir, writes a ROOT (`session ArghdaCheck = HOL + theories <T>`), and runs
  `isabelle build -o quick_and_dirty -d <dir> ArghdaCheck`. Heaps land in
  ~/.isabelle, so the source tree stays clean (~6 s/theory).
- Verdict, ground-truthed vs Isabelle2025: exit≠0 → Error; exit 0 + sorry/oops
  → Admitted (sorry compiles under quick_and_dirty, so it is caught at the
  source, not hidden by the exit code); exit 0 + axiomatization → Postulated;
  exit 0 clean → Proven. Never fabricated.
- Imports: the header `imports … begin` clause (bare names + quoted-path final
  segment; stdlib Main dropped as external). Roots: a ROOT file's `theories`
  section — the genuine Isabelle entry-point convention (analogue of All.agda),
  parsed tolerantly (option groups skipped).
- probe() overridden to `isabelle version` (not `--version`, which errors
  "Unknown Isabelle tool" — `doctor` caught this); added a pub(crate)
  probe_tool_arg helper for the custom version query.

Lint (src/lint/isabelle.rs, `IsabelleEscapeHatch`): warn under the shared
`escape-hatch` name (amber cap); flags sorry/oops/axiomatization.

Provisioning fix at source: the script's Isabelle URL was stale
(`/dist/Isabelle2024…` 404s once a newer release is current) — switched to the
archived `/website-<VER>/dist/` path and bumped to Isabelle2025.

Wired: backend_for "isabelle", KNOWN_BACKENDS, all four `--backend` help
strings, the CLI about line.

Verification (actually run): cargo fmt --check, clippy -D warnings, cargo test
(159 pass: +6 isabelle unit, +4 isabelle lint unit, +3 isabelle integration;
graph tests hermetic — text/ROOT only, run tool-less), check-spdx.sh — all
green. Dogfooded vs real Isabelle2025: `check` → Good=proven / Admits=admitted
/ Postulate=postulated / Broken=error; `reason --check --backend isabelle`
reproduces those; imports All→Base / All→Util / Util→Base parsed; ROOT
theories=All → crt_root All, Base+Util wired, Orphan unwired; `doctor` →
[OK] isabelle assistant Isabelle2025.

Remaining (M9 at 90%): session-qualified / relative-path imports +
dependency-ordered multi-session builds.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7

Author: claude

.machine_readable/6a2/STATE.a2ml

@@ -11,7 +11,7 @@ status = "active"  # active | paused | archived
 
 [project-context]
 name = "arghda-core"
-purpose = "Multi-backend proof-workspace manager — the 'Flying Logic for provers/solvers' engine. A four-state triage workspace (inbox/working/proven/rejected) as file moves, per-backend lint packs targeting the silent-failure class, a backend-parametric import-graph DAG, a demote-only status-propagating reasoning graph, and a JSON + event-stream contract a visual layer (arghda-studio) consumes. Seven backends across both interaction models (Agda, Cubical-Agda, Idris2, Lean4, Coq/Rocq assistants; Z3, CVC5 solvers). It never proves anything itself; the tools do."
+purpose = "Multi-backend proof-workspace manager — the 'Flying Logic for provers/solvers' engine. A four-state triage workspace (inbox/working/proven/rejected) as file moves, per-backend lint packs targeting the silent-failure class, a backend-parametric import-graph DAG, a demote-only status-propagating reasoning graph, and a JSON + event-stream contract a visual layer (arghda-studio) consumes. Eight backends across both interaction models (Agda, Cubical-Agda, Idris2, Lean4, Coq/Rocq, Isabelle/HOL assistants; Z3, CVC5 solvers). It never proves anything itself; the tools do."
 completion-percentage = 92
 
 [position]
@@ -49,7 +49,7 @@ milestones = [
   { name = "M6: Lean4 adapter (lake build + #print axioms audit)", completion = 92 },
   { 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 = 90 },
-  { name = "M9: Isabelle adapter (--heavy; dogfood tropical-resource-typing .thy)", completion = 0 },
+  { name = "M9: Isabelle adapter (--heavy; dogfood tropical-resource-typing .thy)", completion = 90 },
   { name = "M10: Mizar adapter (detect-only first; highest uncertainty)", completion = 0 },
   { name = "M11: studio JSON freeze (reason/0.1) + Groove manifest", completion = 100 },
 ]
@@ -58,8 +58,13 @@ milestones = [
 # real --version. idris2 v0.7.0 builds via chez bootstrap. COQ NOW INSTALLED
 # (2026-07-01, heavy-tail foundation): opam 2.1.5 via apt → `opam install
 # coq.8.18.0` → coqc reports real --version; symlinked to /usr/local/bin/coqc
-# so `arghda doctor` probes it ([OK] coq assistant). Isabelle/Mizar remain
-# scripted (behind --heavy/--mizar) but not installed this session.
+# so `arghda doctor` probes it ([OK] coq assistant). ISABELLE NOW INSTALLED
+# (2026-07-01): Isabelle2025 tarball (1.08 GB, HOL heap prebuilt) unpacked to
+# /opt, symlinked to /usr/local/bin/isabelle; `isabelle version` → Isabelle2025;
+# doctor [OK] isabelle. NB the provision script's Isabelle URL was stale
+# (/dist/Isabelle2024… 404s once a newer release is current) — FIXED at source
+# to the archived /website-<VER>/dist/ path + bumped to Isabelle2025. Mizar
+# remains scripted (behind --mizar) but not installed (distribution manual).
 # Remaining M0: `arghda doctor` Rust subcommand (interim: `just doctor` shells
 # the script's --verify-only table).
 #
@@ -149,6 +154,36 @@ milestones = [
 # Error when an uncompiled dependency is Required — documented limitation, same
 # class as Lean's lake-env gap).
 #
+# M9 landed 2026-07-01 (90%, second heavy-tail backend): the Isabelle/HOL
+# adapter. Foundation-first again — provisioned Isabelle2025 (1.08 GB tarball,
+# HOL heap prebuilt) BEFORE the adapter; ground-truthed the invocation, then
+# built + dogfooded vs the REAL tool. Isabelle is session-based (no single-file
+# --check), so src/prover/isabelle.rs (`Isabelle`) check_file generates a
+# throwaway session: copies the target .thy + sibling .thy files into a temp
+# dir, writes `ROOT` (session ArghdaCheck = HOL + theories <T>), runs
+# `isabelle build -o quick_and_dirty -d <dir> ArghdaCheck` (heaps land in
+# ~/.isabelle, tree stays clean; ~6 s/theory). Verdict, ground-truthed vs
+# Isabelle2025: exit≠0 → Error; exit 0 + sorry/oops → Admitted (sorry compiles
+# under quick_and_dirty, so caught at source); exit 0 + axiomatization →
+# Postulated; exit 0 clean → Proven. Imports: the header `imports … begin`
+# clause (bare names + quoted-path final segment; stdlib Main dropped as
+# external). Roots: a `ROOT` file's `theories` section (the genuine Isabelle
+# entry-point convention — analogue of All.agda; parsed tolerantly, option
+# groups skipped). Lint: src/lint/isabelle.rs `IsabelleEscapeHatch` (warn,
+# shared name escape-hatch) flags sorry/oops/axiomatization. probe() overridden
+# to `isabelle version` (NOT --version, which errors "Unknown Isabelle tool" —
+# doctor caught this; added pub(crate) probe_tool_arg for the custom query).
+# Wired: backend_for "isabelle" + KNOWN_BACKENDS + all four --backend help
+# strings + about line. Also fixed the provision script's stale Isabelle URL at
+# source (/website-<VER>/dist/ + Isabelle2025). 159 tests (+6 isabelle unit +4
+# isabelle lint unit +3 isabelle integration; graph tests hermetic — text/ROOT
+# only, run tool-less). DOGFOODED vs real Isabelle2025: check → Good=proven /
+# Admits=admitted / Postulate=postulated / Broken=error; `reason --check
+# --backend isabelle` reproduces those; imports All→Base/All→Util/Util→Base
+# parsed, ROOT theories=All → crt_root All, Base+Util wired, Orphan unwired;
+# doctor → [OK] isabelle assistant Isabelle2025. Remaining 10%: session-
+# qualified / relative-path imports + dependency-ordered multi-session builds.
+#
 # 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`
@@ -311,7 +346,8 @@ actions = [
   "M4 follow-on: .ipkg-declared roots DONE; remaining = totality-hole (?name) + per-def `partial` lint.",
   "M3 follow-on: DONE — `reason --workspace <ws>` sources real verdicts from a `proven/` state (workspace_verdicts) + demotes stale-proven via the content-hash closure. Refinement follow-ons bucket now complete.",
   "M8 (Coq/Rocq): DONE (90%) — coqc 8.18.0 provisioned + adapter built + dogfooded (proven/admitted/postulated/error) with Section-aware postulate classifier. Remaining: _CoqProject logical paths + dependency-ordered compilation.",
-  "M9-M10 heavy tail (Isabelle, Mizar) — next, foundation-first: Isabelle ~4GB tarball then adapter; Mizar niche/detect-only. Then climb to M6 lake-env, M4 totality lint, M7 Echidna client.",
+  "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): next, foundation-first — detect-only first (distribution is manual/niche via mizar.org; provision honestly, check_file → Unavailable until a real toolchain confirms invocation). Then climb to M6 lake-env, M4 totality lint, M7 Echidna client.",
 ]
 
 [maintenance-status]
@@ -320,13 +356,14 @@ 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-M8: 108 lib + 38 integration = 146 tests pass. codeql.yml added
-# (code-scanning gate fix). M8 Coq adapter dogfooded vs real coqc 8.18.0
-# (proven/admitted/postulated/error; reason --check; import edges; roots; wired;
-# doctor [OK] coq). reason --workspace verdicts+staleness dogfooded. Lean
-# #print axioms audit dogfooded. doctor/groove/dispatch dogfooded. SEVEN
-# backends now: agda + agda-cubical + idris2 + lean4 + coq (Assistant), z3 +
-# cvc5 (Solver). Dogfooded historically vs echo-types + agda-unused.
+# post-M9: 118 lib + 41 integration = 159 tests pass. codeql.yml added
+# (code-scanning gate fix). M9 Isabelle adapter dogfooded vs real Isabelle2025
+# (proven/admitted/postulated/error; reason --check; imports edges; ROOT roots;
+# wired; doctor [OK] isabelle). M8 Coq adapter dogfooded vs real coqc 8.18.0.
+# reason --workspace verdicts+staleness dogfooded. Lean #print axioms audit
+# dogfooded. doctor/groove/dispatch dogfooded. EIGHT backends now: agda +
+# agda-cubical + idris2 + lean4 + coq + isabelle (Assistant), z3 + cvc5
+# (Solver). Dogfooded historically vs echo-types + agda-unused.
 
 [ecosystem]
 part-of = ["arghda"]

scripts/provision-provers.sh

@@ -35,7 +35,7 @@ IDRIS2_TAG="v0.7.0"                       # standards/a2ml CI pin
 LEAN_VER="v4.13.0"                        # tropical-resource-typing lean-toolchain
 CVC5_VER="1.2.0"                          # cvc5 static-binary release
 COQ_VER="8.18.0"                          # opam (with --heavy)
-ISABELLE_VER="Isabelle2024"               # TUM tarball (with --heavy)
+ISABELLE_VER="Isabelle2025"               # TUM tarball (with --heavy)
 
 STDLIB_DIR=/opt/agda-stdlib
 CUBICAL_DIR=/opt/agda-cubical
@@ -203,8 +203,11 @@ install_coq() {
 
 install_isabelle() {
   have isabelle && { log "isabelle present"; return; }
-  log "installing ${ISABELLE_VER} (heavy, ~4 GB)…"
-  local url="https://isabelle.in.tum.de/dist/${ISABELLE_VER}_linux.tar.gz"
+  log "installing ${ISABELLE_VER} (heavy, ~1.1 GB download, HOL heap ships prebuilt)…"
+  # Only the *current* release lives under /dist/; older ones move to the
+  # archived /website-<VER>/dist/ path (the /dist/ form 404s). The archived
+  # path is stable and works for the current release too, so use it uniformly.
+  local url="https://isabelle.in.tum.de/website-${ISABELLE_VER}/dist/${ISABELLE_VER}_linux.tar.gz"
   if curl -fsSL "$url" -o /tmp/isabelle.tar.gz 2>/dev/null && [ -s /tmp/isabelle.tar.gz ]; then
     tar -xzf /tmp/isabelle.tar.gz -C /opt \
       && ln -sf "/opt/${ISABELLE_VER}/bin/isabelle" /usr/local/bin/isabelle \

src/lib.rs

@@ -35,8 +35,8 @@ pub use graph::{build as build_graph, ImportGraph};
 pub use groove::{manifest as groove_manifest, GrooveManifest};
 pub use lint::{default_rules, rules_with_config, run_lints, LintRule, RuleConfig};
 pub use prover::{
-    default_backend, Agda, AgdaCubical, Backend, BackendKind, Coq, Idris2, Lean, Outcome, Probe,
-    Smt, Verdict,
+    default_backend, Agda, AgdaCubical, Backend, BackendKind, Coq, Idris2, Isabelle, Lean, Outcome,
+    Probe, Smt, Verdict,
 };
 pub use reason::{
     build as build_reason, workspace_verdicts, Junct, ReasonDocument, ReasonEdge, ReasonNode,

src/lint/isabelle.rs

@@ -0,0 +1,146 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
+//! Isabelle/HOL `escape-hatch` (warn) — surface soundness escape hatches.
+//!
+//! The Isabelle analogue of the Agda/Idris2/Lean/Coq escape-hatch rules;
+//! shares the rule *name* `escape-hatch` so the reasoning graph caps any hit
+//! at amber.
+//!
+//! Flags `sorry` (admits a proposition without proof), `oops` (abandons a
+//! proof mid-attempt) and `axiomatization` (introduces unverified axioms).
+//! `isabelle build -o quick_and_dirty` compiles a theory containing `sorry`
+//! with exit 0, so without this warn — and without the backend's source-level
+//! classification — such gaps ride along invisibly. Block comments `(* … *)`
+//! are stripped so a "no sorry here" comment does not match; prose blocks
+//! (`text ‹…›`) are a documented minor false-positive risk.
+
+use super::{LintContext, LintRule};
+use crate::diagnostic::{Diagnostic, LintReport, Severity};
+use anyhow::{Context, Result};
+use std::fs;
+use std::path::Path;
+
+pub struct IsabelleEscapeHatch;
+
+const ESCAPE_TOKENS: &[&str] = &["sorry", "oops", "axiomatization"];
+
+impl LintRule for IsabelleEscapeHatch {
+    fn name(&self) -> &'static str {
+        "escape-hatch"
+    }
+
+    fn run(&self, file: &Path, _ctx: &LintContext<'_>, report: &mut LintReport) -> Result<()> {
+        let contents =
+            fs::read_to_string(file).with_context(|| format!("reading {}", file.display()))?;
+        for (i, raw) in contents.lines().enumerate() {
+            let trimmed = raw.trim_start();
+            if trimmed.starts_with("(*") {
+                continue; // whole-line comment (common case)
+            }
+            let code = strip_line_comments(raw);
+            for tok in ESCAPE_TOKENS {
+                if has_token(&code, tok) {
+                    report.push(warn(
+                        self.name(),
+                        file,
+                        i + 1,
+                        format!("escape primitive `{tok}`"),
+                    ));
+                }
+            }
+        }
+        Ok(())
+    }
+}
+
+fn warn(rule: &str, file: &Path, line: usize, message: String) -> Diagnostic {
+    Diagnostic {
+        rule: rule.to_string(),
+        severity: Severity::Warn,
+        file: file.to_path_buf(),
+        message,
+        line: Some(line),
+    }
+}
+
+/// Remove balanced `(* … *)` spans; an unmatched `(*` truncates the rest of
+/// the line.
+fn strip_line_comments(line: &str) -> String {
+    let mut out = String::with_capacity(line.len());
+    let bytes = line.as_bytes();
+    let mut i = 0;
+    let mut depth = 0u32;
+    while i < bytes.len() {
+        if i + 1 < bytes.len() && bytes[i] == b'(' && bytes[i + 1] == b'*' {
+            depth += 1;
+            i += 2;
+            continue;
+        }
+        if depth > 0 && i + 1 < bytes.len() && bytes[i] == b'*' && bytes[i + 1] == b')' {
+            depth -= 1;
+            i += 2;
+            continue;
+        }
+        if depth == 0 {
+            out.push(bytes[i] as char);
+        }
+        i += 1;
+    }
+    out
+}
+
+/// `tok` appears in `s` as a delimited token (so `sorryish` does not match).
+fn has_token(s: &str, tok: &str) -> bool {
+    s.split(|c: char| c.is_whitespace() || "(){}[];,.".contains(c))
+        .any(|w| w == tok)
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::lint::run_lints;
+    use std::path::PathBuf;
+
+    fn lint_str(body: &str) -> LintReport {
+        let tmp = tempfile::NamedTempFile::new().unwrap();
+        std::fs::write(tmp.path(), body).unwrap();
+        let roots: [PathBuf; 0] = [];
+        let ctx = LintContext {
+            include_root: tmp.path().parent().unwrap(),
+            entry_modules: &roots,
+        };
+        let rules: Vec<Box<dyn LintRule>> = vec![Box::new(IsabelleEscapeHatch)];
+        run_lints(tmp.path(), &ctx, &rules).unwrap()
+    }
+
+    #[test]
+    fn sorry_is_warned() {
+        let r = lint_str("theory T imports Main begin\nlemma l: \"True\" sorry\nend\n");
+        assert_eq!(r.warns().count(), 1);
+        assert_eq!(r.diagnostics[0].rule, "escape-hatch");
+        assert!(r.diagnostics[0].message.contains("sorry"));
+    }
+
+    #[test]
+    fn oops_and_axiomatization_are_warned() {
+        let r = lint_str(
+            "theory T imports Main begin\naxiomatization where foo: \"P\"\nlemma l: \"Q\" oops\nend\n",
+        );
+        assert_eq!(r.warns().count(), 2);
+    }
+
+    #[test]
+    fn escape_token_in_comment_is_ignored() {
+        let r = lint_str(
+            "theory T imports Main begin\ndefinition x where \"x = 0\" (* no sorry *)\nend\n",
+        );
+        assert!(r.diagnostics.is_empty());
+    }
+
+    #[test]
+    fn clean_theory_is_silent() {
+        let r = lint_str("theory T imports Main begin\nlemma l: \"True\" by simp\nend\n");
+        assert!(r.diagnostics.is_empty());
+    }
+}

src/lint/mod.rs

@@ -8,6 +8,7 @@ use std::path::{Path, PathBuf};
 pub mod coq;
 pub mod escape_hatch;
 pub mod idris2;
+pub mod isabelle;
 pub mod lean;
 pub mod orphan_module;
 pub mod postulate;

src/main.rs

@@ -5,8 +5,8 @@ use anyhow::{Context, Result};
 use arghda_core::lint::LintContext;
 use arghda_core::{
     build_dag, build_reason, event, groove_manifest, run_lints, unused, watcher, Agda, AgdaCubical,
-    Backend, BackendKind, Coq, Dispatch, Idris2, Lean, LintRule, Probe, RuleConfig, Smt, State,
-    Verdict, Workspace,
+    Backend, BackendKind, Coq, Dispatch, Idris2, Isabelle, Lean, LintRule, Probe, RuleConfig, Smt,
+    State, Verdict, Workspace,
 };
 use clap::{Parser, Subcommand};
 use std::path::{Path, PathBuf};
@@ -23,6 +23,7 @@ const KNOWN_BACKENDS: &[&str] = &[
     "idris2",
     "lean4",
     "coq",
+    "isabelle",
     "z3",
     "cvc5",
 ];
@@ -36,10 +37,11 @@ fn backend_for(name: &str) -> Result<Box<dyn Backend>> {
         "idris2" => Ok(Box::new(Idris2)),
         "lean4" => Ok(Box::new(Lean)),
         "coq" => Ok(Box::new(Coq)),
+        "isabelle" => Ok(Box::new(Isabelle)),
         "z3" => Ok(Box::new(Smt::z3())),
         "cvc5" => Ok(Box::new(Smt::cvc5())),
         other => anyhow::bail!(
-            "unknown backend `{other}` (known: agda, agda-cubical, idris2, lean4, coq, z3, cvc5)"
+            "unknown backend `{other}` (known: agda, agda-cubical, idris2, lean4, coq, isabelle, z3, cvc5)"
         ),
     }
 }
@@ -48,7 +50,7 @@ fn backend_for(name: &str) -> Result<Box<dyn Backend>> {
 #[command(
     name = "arghda",
     version,
-    about = "Proof-workspace manager for provers/solvers (Agda, Cubical, Idris2, Lean4, Coq, Z3, CVC5)"
+    about = "Proof-workspace manager for provers/solvers (Agda, Cubical, Idris2, Lean4, Coq, Isabelle, Z3, CVC5)"
 )]
 struct Cli {
     #[command(subcommand)]
@@ -76,7 +78,7 @@ enum Cmd {
         #[arg(long)]
         config: Option<PathBuf>,
         /// Backend: `agda` (default), `agda-cubical`, `idris2`, `lean4`,
-        /// `coq`, `z3`, `cvc5`.
+        /// `coq`, `isabelle`, `z3`, `cvc5`.
         #[arg(long, default_value = "agda")]
         backend: String,
         /// Also run the external `agda-unused` analyser and re-emit its
@@ -96,7 +98,7 @@ enum Cmd {
         #[arg(long)]
         include_root: Option<PathBuf>,
         /// Backend: `agda` (default), `agda-cubical`, `idris2`, `lean4`,
-        /// `coq`, `z3`, `cvc5`.
+        /// `coq`, `isabelle`, `z3`, `cvc5`.
         #[arg(long, default_value = "agda")]
         backend: String,
         /// Where the check runs: `local` (default) or `echidna[=<url>]`
@@ -124,7 +126,7 @@ enum Cmd {
         #[arg(long)]
         config: Option<PathBuf>,
         /// Backend: `agda` (default), `agda-cubical`, `idris2`, `lean4`,
-        /// `coq`, `z3`, `cvc5`.
+        /// `coq`, `isabelle`, `z3`, `cvc5`.
         #[arg(long, default_value = "agda")]
         backend: String,
     },
@@ -148,7 +150,7 @@ enum Cmd {
         #[arg(long)]
         config: Option<PathBuf>,
         /// Backend: `agda` (default), `agda-cubical`, `idris2`, `lean4`,
-        /// `coq`, `z3`, `cvc5`.
+        /// `coq`, `isabelle`, `z3`, `cvc5`.
         #[arg(long, default_value = "agda")]
         backend: String,
         /// Run the backend on every node to populate REAL prover verdicts