diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index d0cd8a8..ed50439 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.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-/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 ), runs +# `isabelle build -o quick_and_dirty -d 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-/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 ` 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"] diff --git a/scripts/provision-provers.sh b/scripts/provision-provers.sh index eb0818d..dafe202 100644 --- a/scripts/provision-provers.sh +++ b/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-/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 \ diff --git a/src/lib.rs b/src/lib.rs index 22158f8..ccffe22 100644 --- a/src/lib.rs +++ b/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, diff --git a/src/lint/isabelle.rs b/src/lint/isabelle.rs new file mode 100644 index 0000000..fb9e892 --- /dev/null +++ b/src/lint/isabelle.rs @@ -0,0 +1,146 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + +//! 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> = 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()); + } +} diff --git a/src/lint/mod.rs b/src/lint/mod.rs index df6346b..d700436 100644 --- a/src/lint/mod.rs +++ b/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; diff --git a/src/main.rs b/src/main.rs index 71c3c92..431dda0 100644 --- a/src/main.rs +++ b/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> { "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> { #[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, /// 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, /// 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[=]` @@ -124,7 +126,7 @@ enum Cmd { #[arg(long)] config: Option, /// 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, /// 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 diff --git a/src/prover/isabelle.rs b/src/prover/isabelle.rs new file mode 100644 index 0000000..145da98 --- /dev/null +++ b/src/prover/isabelle.rs @@ -0,0 +1,422 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + +//! The Isabelle/HOL backend. +//! +//! Assistant model. Isabelle is session-based — there is no single-file +//! `--check`; a theory is checked by building a session that lists it. So +//! [`Backend::check_file`] generates a throwaway session: it copies the target +//! `.thy` (and its sibling `.thy` files, so in-tree imports resolve) into a +//! temp directory, writes a `ROOT` declaring `session ArghdaCheck = HOL + +//! theories `, and runs `isabelle build -o quick_and_dirty -d +//! ArghdaCheck`. Heap images land in `~/.isabelle`, so the source tree stays +//! clean. Ground-truthed against Isabelle2025 (HOL heap ships prebuilt, so a +//! per-theory build is ~6 s): +//! * exit non-zero → [`Verdict::Error`] (the theory failed to build — a real +//! error, or an import the throwaway session could not resolve). +//! * exit 0, source contains `sorry`/`oops` → [`Verdict::Admitted`] (`sorry` +//! compiles under `quick_and_dirty`, so it must be caught at the source). +//! * exit 0, source contains `axiomatization` → [`Verdict::Postulated`]. +//! * exit 0, otherwise → [`Verdict::Proven`]. +//! * binary absent → [`Verdict::Unavailable`]. +//! +//! 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. + +use super::{probe_tool_arg, Backend, BackendKind, Outcome, Probe, Verdict}; +use crate::graph; +use crate::lint::{isabelle::IsabelleEscapeHatch, LintRule, RuleConfig}; +use anyhow::{Context, Result}; +use std::fs; +use std::path::{Path, PathBuf}; +use std::process::Command; +use std::time::{SystemTime, UNIX_EPOCH}; +use walkdir::WalkDir; + +const TAIL_LINES: usize = 40; + +/// `ROOT` section keywords that terminate a `theories` block. +const ROOT_SECTIONS: &[&str] = &[ + "session", + "options", + "sessions", + "directories", + "theories", + "document_theories", + "document_files", + "export_files", + "export_classpath", +]; + +/// The Isabelle/HOL proof assistant. +#[derive(Clone, Copy, Debug, Default)] +pub struct Isabelle; + +impl Backend for Isabelle { + fn name(&self) -> &'static str { + "isabelle" + } + + fn kind(&self) -> BackendKind { + BackendKind::Assistant + } + + fn extensions(&self) -> &'static [&'static str] { + &["thy"] + } + + fn safe_mode(&self) -> Option<&'static str> { + // No global safe flag; soundness is the absence of sorry/oops and of + // axiomatization. + None + } + + fn check_file(&self, file: &Path, include_root: &Path) -> Result { + let stem = file + .file_stem() + .and_then(|s| s.to_str()) + .unwrap_or("Check") + .to_string(); + + let nanos = SystemTime::now() + .duration_since(UNIX_EPOCH) + .map(|d| d.as_nanos()) + .unwrap_or(0); + let session_dir = + std::env::temp_dir().join(format!("arghda-isa-{}-{}", std::process::id(), nanos)); + if fs::create_dir_all(&session_dir).is_err() { + 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). + for entry in WalkDir::new(include_root) + .into_iter() + .filter_map(|e| e.ok()) + { + let p = entry.path(); + if p.extension().and_then(|s| s.to_str()) == Some("thy") { + if let Some(name) = p.file_name() { + let _ = fs::copy(p, session_dir.join(name)); + } + } + } + let _ = fs::copy(file, session_dir.join(format!("{stem}.thy"))); + + let root = format!("session \"ArghdaCheck\" = \"HOL\" +\n 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)); + } + + let output = Command::new("isabelle") + .arg("build") + .arg("-o") + .arg("quick_and_dirty") // let `sorry` compile so we classify it + .arg("-d") + .arg(&session_dir) + .arg("ArghdaCheck") + .output(); + + let _ = fs::remove_dir_all(&session_dir); + + match output { + Ok(out) => { + let mut combined = String::from_utf8_lossy(&out.stdout).into_owned(); + combined.push_str(&String::from_utf8_lossy(&out.stderr)); + let src = fs::read_to_string(file).unwrap_or_default(); + let verdict = isabelle_verdict(&src, out.status.success()); + Ok(Outcome { + available: true, + exit_code: out.status.code(), + ok: verdict == Verdict::Proven, + output_tail: tail(&combined, TAIL_LINES), + kind: BackendKind::Assistant, + verdict, + }) + } + Err(e) if e.kind() == std::io::ErrorKind::NotFound => { + Ok(Outcome::unavailable(BackendKind::Assistant)) + } + Err(e) => Err(e.into()), + } + } + + fn module_name_of(&self, file: &Path, include_root: &Path) -> Option { + graph::module_name_of(file, include_root) + } + + fn module_to_path(&self, module: &str, include_root: &Path) -> PathBuf { + let mut p = include_root.to_path_buf(); + for part in module.split('.') { + p.push(part); + } + p.set_extension("thy"); + p + } + + fn direct_imports(&self, file: &Path) -> Result> { + let contents = + fs::read_to_string(file).with_context(|| format!("reading {}", file.display()))?; + Ok(parse_imports(&contents)) + } + + fn discover_roots(&self, include_root: &Path) -> Vec { + // The genuine Isabelle convention: a `ROOT` file's `theories` section + // lists the session's entry theories. Resolve each to its `.thy`. + 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.file_name().and_then(|s| s.to_str()) == Some("ROOT") { + roots.extend(root_theory_files(path)); + } + } + roots.sort(); + roots.dedup(); + roots + } + + fn lint_rules(&self, _cfg: &RuleConfig) -> Result>> { + Ok(vec![Box::new(IsabelleEscapeHatch)]) + } + + fn command(&self) -> &'static str { + "isabelle" + } + + fn probe(&self) -> Probe { + // Isabelle's version query is the `version` subcommand, not + // `--version` (which errors with "Unknown Isabelle tool"). + probe_tool_arg(self.name(), self.kind(), self.command(), "version") + } +} + +/// Map Isabelle source + build status to a [`Verdict`], honestly: a green +/// build is `Proven` unless the source carries an escape hatch — +/// `sorry`/`oops` ⇒ `Admitted` (they compile under `quick_and_dirty`, so the +/// exit code alone would hide them), `axiomatization` ⇒ `Postulated`. A +/// non-zero build ⇒ `Error`. Admitted dominates a postulate. +fn isabelle_verdict(src: &str, exit_ok: bool) -> Verdict { + if !exit_ok { + return Verdict::Error; + } + if has_token(src, "sorry") || has_token(src, "oops") { + return Verdict::Admitted; + } + if has_token(src, "axiomatization") { + return Verdict::Postulated; + } + Verdict::Proven +} + +/// Extract the theories named in a theory header's `imports` clause: +/// `theory Foo imports Bar Baz "…/Qux" begin`. Bare names pass through; +/// quoted path imports contribute their final path segment. Everything from +/// `imports` up to `begin` (or a `keywords`/`abbrevs` header section) is +/// scanned, tolerating a multi-line header. +fn parse_imports(contents: &str) -> Vec { + let tokens: Vec<&str> = contents.split_whitespace().collect(); + let Some(start) = tokens.iter().position(|t| *t == "imports") else { + return Vec::new(); + }; + let mut out = Vec::new(); + for tok in &tokens[start + 1..] { + if *tok == "begin" || *tok == "keywords" || *tok == "abbrevs" { + break; + } + let name = theory_token(tok); + if !name.is_empty() { + out.push(name); + } + } + out +} + +/// 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 { + let t = tok.trim_matches('"'); + let seg = t.rsplit('/').next().unwrap_or(t); + seg.trim_matches(|c: char| !c.is_alphanumeric() && c != '_') + .to_string() +} + +/// Parse a `ROOT` file's `theories` sections and resolve each listed theory +/// to a `/.thy` file that exists. Tolerant: option groups +/// `(…)` and other sections are skipped. +fn root_theory_files(root_file: &Path) -> Vec { + let Ok(contents) = fs::read_to_string(root_file) else { + return Vec::new(); + }; + let dir = root_file.parent().unwrap_or(Path::new(".")); + let tokens: Vec<&str> = contents.split_whitespace().collect(); + let mut out = Vec::new(); + let mut collecting = false; + let mut skip_group = false; + for tok in tokens { + // Skip an inline `(options …)` group inside a theories section. + if skip_group { + if tok.ends_with(')') { + skip_group = false; + } + continue; + } + if tok == "theories" { + collecting = true; + continue; + } + if ROOT_SECTIONS.contains(&tok) { + collecting = false; + continue; + } + if !collecting { + continue; + } + if tok.starts_with('(') { + if !tok.ends_with(')') { + skip_group = true; + } + continue; + } + if tok == "+" || tok == "=" { + continue; + } + let name = theory_token(tok); + if name.is_empty() { + continue; + } + let candidate = dir.join(format!("{name}.thy")); + if candidate.is_file() { + out.push(candidate); + } + } + out +} + +fn tail(s: &str, n: usize) -> String { + let lines: Vec<&str> = s.lines().collect(); + let start = lines.len().saturating_sub(n); + lines[start..].join("\n") +} + +/// `tok` appears in `s` as a delimited token. +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::*; + + #[test] + fn isabelle_backend_identity() { + assert_eq!(Isabelle.name(), "isabelle"); + assert_eq!(Isabelle.kind(), BackendKind::Assistant); + assert_eq!(Isabelle.extensions(), &["thy"]); + assert_eq!(Isabelle.command(), "isabelle"); + } + + #[test] + fn module_to_path_uses_thy_extension() { + assert_eq!( + Isabelle.module_to_path("Foo", Path::new("/r")), + PathBuf::from("/r/Foo.thy") + ); + } + + #[test] + fn imports_clause_parsed_multiline_and_quoted() { + let tmp = tempfile::NamedTempFile::new().unwrap(); + std::fs::write( + tmp.path(), + "theory Foo\n imports Main Bar \"../Other/Baz\"\n keywords \"x\"\nbegin\nend\n", + ) + .unwrap(); + let imports = Isabelle.direct_imports(tmp.path()).unwrap(); + assert!(imports.contains(&"Main".to_string())); + assert!(imports.contains(&"Bar".to_string())); + assert!( + imports.contains(&"Baz".to_string()), + "quoted path → final seg" + ); + // `keywords` terminates the imports clause. + assert!(!imports.iter().any(|i| i == "x")); + } + + #[test] + fn verdict_is_honest_about_sorry_axiom_and_clean() { + assert_eq!( + isabelle_verdict("lemma l: \"True\" by simp", false), + Verdict::Error + ); + assert_eq!( + isabelle_verdict("lemma l: \"P\" sorry", true), + Verdict::Admitted + ); + assert_eq!( + isabelle_verdict("lemma l: \"P\" oops", true), + Verdict::Admitted + ); + assert_eq!( + isabelle_verdict("axiomatization where ax: \"P\"", true), + Verdict::Postulated + ); + assert_eq!( + isabelle_verdict("lemma l: \"True\" by simp", true), + Verdict::Proven + ); + } + + #[test] + fn root_theories_are_discovered_as_roots() { + let tmp = tempfile::tempdir().unwrap(); + let r = tmp.path(); + std::fs::write(r.join("All.thy"), "theory All imports Main begin end\n").unwrap(); + std::fs::write(r.join("Extra.thy"), "theory Extra imports Main begin end\n").unwrap(); + std::fs::write( + r.join("ROOT"), + "session \"Demo\" = \"HOL\" +\n options [document = false]\n theories\n All\n Extra\n document_files\n \"root.tex\"\n", + ) + .unwrap(); + let roots = Isabelle.discover_roots(r); + let names: Vec = roots + .iter() + .map(|p| p.file_name().unwrap().to_str().unwrap().to_string()) + .collect(); + assert!(names.contains(&"All.thy".to_string())); + assert!(names.contains(&"Extra.thy".to_string())); + assert_eq!(roots.len(), 2, "only theories-section entries: {names:?}"); + } + + #[test] + fn check_file_is_honest_about_availability() { + let tmp = tempfile::tempdir().unwrap(); + let f = tmp.path().join("T.thy"); + std::fs::write( + &f, + "theory T imports Main begin\nlemma l: \"True\" by simp\nend\n", + ) + .unwrap(); + let out = Isabelle.check_file(&f, tmp.path()).unwrap(); + if out.available { + assert!(matches!( + out.verdict, + Verdict::Proven | Verdict::Admitted | Verdict::Postulated | Verdict::Error + )); + assert_eq!(out.ok, out.verdict == Verdict::Proven); + } else { + assert_eq!(out.verdict, Verdict::Unavailable); + assert!(!out.ok); + } + } +} diff --git a/src/prover/mod.rs b/src/prover/mod.rs index 7d2c4cf..e41d236 100644 --- a/src/prover/mod.rs +++ b/src/prover/mod.rs @@ -29,12 +29,14 @@ use std::process::Command; pub mod agda; pub mod idris2; +pub mod isabelle; pub mod lean; pub mod rocq; pub mod smt; pub use agda::{Agda, AgdaCubical}; pub use idris2::Idris2; +pub use isabelle::Isabelle; pub use lean::Lean; pub use rocq::Coq; pub use smt::Smt; @@ -129,7 +131,13 @@ pub struct Probe { /// `false` only when the binary is absent / cannot be executed (never a /// guess). `detail` is the first output line, or the reason it failed. fn probe_tool(name: &str, kind: BackendKind, cmd: &str) -> Probe { - match Command::new(cmd).arg("--version").output() { + probe_tool_arg(name, kind, cmd, "--version") +} + +/// As [`probe_tool`], but with an explicit version-query argument — some +/// tools use a subcommand (`isabelle version`) rather than `--version`. +pub(crate) fn probe_tool_arg(name: &str, kind: BackendKind, cmd: &str, version_arg: &str) -> Probe { + match Command::new(cmd).arg(version_arg).output() { Ok(out) => { let mut combined = String::from_utf8_lossy(&out.stdout).into_owned(); combined.push_str(&String::from_utf8_lossy(&out.stderr)); diff --git a/tests/fixtures/isabelle/All.thy b/tests/fixtures/isabelle/All.thy new file mode 100644 index 0000000..7b12d7d --- /dev/null +++ b/tests/fixtures/isabelle/All.thy @@ -0,0 +1,2 @@ +theory All imports Main Base Util begin +end diff --git a/tests/fixtures/isabelle/Base.thy b/tests/fixtures/isabelle/Base.thy new file mode 100644 index 0000000..46c8fd9 --- /dev/null +++ b/tests/fixtures/isabelle/Base.thy @@ -0,0 +1,2 @@ +theory Base imports Main begin +end diff --git a/tests/fixtures/isabelle/Orphan.thy b/tests/fixtures/isabelle/Orphan.thy new file mode 100644 index 0000000..786da70 --- /dev/null +++ b/tests/fixtures/isabelle/Orphan.thy @@ -0,0 +1,2 @@ +theory Orphan imports Main begin +end diff --git a/tests/fixtures/isabelle/ROOT b/tests/fixtures/isabelle/ROOT new file mode 100644 index 0000000..dcd2414 --- /dev/null +++ b/tests/fixtures/isabelle/ROOT @@ -0,0 +1,4 @@ +session "Demo" = "HOL" + + options [document = false] + theories + All diff --git a/tests/fixtures/isabelle/Util.thy b/tests/fixtures/isabelle/Util.thy new file mode 100644 index 0000000..e8cc466 --- /dev/null +++ b/tests/fixtures/isabelle/Util.thy @@ -0,0 +1,2 @@ +theory Util imports Main Base begin +end diff --git a/tests/isabelle.rs b/tests/isabelle.rs new file mode 100644 index 0000000..1f04957 --- /dev/null +++ b/tests/isabelle.rs @@ -0,0 +1,92 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + +//! Isabelle/HOL backend, exercised through the backend-parametric graph/dag/ +//! reason path. These tests are hermetic — they only parse `.thy` text +//! (theory names, `imports` clauses) and the `ROOT` file, so they run with or +//! without the `isabelle` binary present. The real session build + verdict +//! classification (`check_file`) is covered by the unit test in +//! `src/prover/isabelle.rs` (honest either way) and by manual dogfooding +//! against Isabelle2025. + +use arghda_core::lint::unpinned_headline::DEFAULT_HEADLINE_PATTERN; +use arghda_core::{build_dag, build_reason, Backend, Isabelle, LintRule}; +use std::collections::{BTreeMap, BTreeSet}; +use std::path::PathBuf; + +fn isabelle_fixture() -> PathBuf { + let mut p = PathBuf::from(env!("CARGO_MANIFEST_DIR")); + p.push("tests"); + p.push("fixtures"); + p.push("isabelle"); + p +} + +fn no_rules() -> Vec> { + Vec::new() +} + +#[test] +fn isabelle_imports_graph_over_the_fixture() { + let root = isabelle_fixture(); + let roots = Isabelle.discover_roots(&root); + let dag = build_dag( + &root, + &roots, + &no_rules(), + DEFAULT_HEADLINE_PATTERN, + &Isabelle, + ) + .unwrap(); + + let mut ids: Vec<&str> = dag.nodes.iter().map(|n| n.id.as_str()).collect(); + ids.sort_unstable(); + assert_eq!(ids, vec!["All", "Base", "Orphan", "Util"]); + + // `imports` edges (Main is external and correctly dropped). + assert!(dag + .edges + .iter() + .any(|e| e.from == "All" && e.to == "Base" && e.kind == "imports")); + assert!(dag.edges.iter().any(|e| e.from == "All" && e.to == "Util")); + assert!(dag.edges.iter().any(|e| e.from == "Util" && e.to == "Base")); + assert!(!dag.edges.iter().any(|e| e.to == "Orphan")); + assert!( + !dag.edges.iter().any(|e| e.to == "Main"), + "stdlib import dropped" + ); +} + +#[test] +fn isabelle_discover_roots_reads_the_root_file() { + let root = isabelle_fixture(); + let roots = Isabelle.discover_roots(&root); + let names: Vec = roots + .iter() + .map(|p| p.file_name().unwrap().to_str().unwrap().to_string()) + .collect(); + // The ROOT's `theories` section lists only `All`. + assert_eq!(names, vec!["All.thy".to_string()]); +} + +#[test] +fn isabelle_reason_graph_wires_the_root_cone() { + let root = isabelle_fixture(); + let roots = Isabelle.discover_roots(&root); + let dag = build_dag( + &root, + &roots, + &no_rules(), + DEFAULT_HEADLINE_PATTERN, + &Isabelle, + ) + .unwrap(); + let doc = build_reason(dag, &Isabelle, &BTreeMap::new(), &BTreeSet::new()); + + assert_eq!(doc.crt_roots, vec!["All".to_string()]); + let wired = |id: &str| doc.nodes.iter().find(|n| n.id == id).unwrap().wired; + assert!(wired("All")); + assert!(wired("Util")); + assert!(wired("Base")); + assert!(!wired("Orphan"), "Orphan must be unwired"); +}