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

[hyperpolymath]

What

The second heavy-tail backend. arghda is now an eight-backend prover-parametric workspace (agda, agda-cubical, idris2, lean4, coq, isabelle as Assistants; z3, cvc5 as Solvers).

Foundation-first again: provisioned Isabelle2025 (1.08 GB tarball, HOL heap ships prebuilt), ground-truthed the invocation against the real tool, then built and dogfooded the adapter.

How

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 — honest, never fabricated: 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.
• 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.
• 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 — clean
• cargo clippy --all-targets -- -D warnings — clean
• cargo test — 159 pass (+6 isabelle unit, +4 isabelle lint unit, +3 isabelle integration; the graph tests are hermetic — text/ROOT only, run tool-less)
• bash scripts/check-spdx.sh . — OK

Dogfooded against real Isabelle2025:

fixture	arghda check --backend isabelle
Good.thy (by simp)	proven
Admits.thy (sorry)	admitted
Postulate.thy (axiomatization)	postulated
Broken.thy (false lemma)	error

• reason --check --backend isabelle reproduces those verdicts
• imports All → Base / All → Util / Util → Base parsed; ROOT theories = All → crt_root All; Base+Util wired; Orphan unwired
• arghda doctor → [OK] isabelle assistant Isabelle2025

Scope

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

🤖 Generated with Claude Code

https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7

---

Generated by Claude Code