diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 78fc455..4853400 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -46,7 +46,7 @@ milestones = [ { name = "M3: Flying-Logic reasoning graph (src/reason: And|Or juncts, demote-only cycle-safe Verdict propagation, additive studio JSON)", completion = 100 }, { name = "M4: Idris2 adapter (core/ABI language: .ipkg/--check/totality; escape-hatches)", completion = 90 }, { name = "M5: SMT solver backends (Z3, CVC5): SMT-LIB2 -> sat/unsat/unknown -> Verdict", completion = 100 }, - { name = "M6: Lean4 adapter (lake build + #print axioms audit)", completion = 0 }, + { name = "M6: Lean4 adapter (lake build + #print axioms audit)", completion = 85 }, { name = "M7: Echidna dispatch seam (optional route to orchestrator :8090, same Outcome)", completion = 0 }, { name = "M8: Coq/Rocq adapter (--heavy provisioning; Section-aware postulate classifier)", completion = 0 }, { name = "M9: Isabelle adapter (--heavy; dogfood tropical-resource-typing .thy)", completion = 0 }, @@ -60,6 +60,28 @@ milestones = [ # Remaining M0: `arghda doctor` Rust subcommand (interim: `just doctor` shells # the script's --verify-only table). # +# M6 landed 2026-07-01 (85%): the Lean4 backend — sixth backend. src/prover/ +# lean.rs: `lean ` elaboration. The honesty subtlety Lean forces: a green +# exit does NOT mean proven (sorry is only a warning; exit 0). So the verdict is +# NOT exit-code-only like agda/idris2 — it PARSES output: exit≠0→Error; exit 0 + +# "sorry" in output→Admitted; exit 0 clean→Unknown (elaborated but NOT audited — +# arghda refuses to claim Proven without a #print axioms audit; matches the plan's +# "honest Unknown when the audit is absent"). Dotted modules reuse module_name_of; +# .lean module_to_path; import parser (top-level `import Mod`; `open` is a +# namespace directive, NOT an edge — deliberately ignored); Main.lean roots. +# src/lint/lean.rs: LeanEscapeHatch (sorry/admit/native_decide/unsafe) named +# "escape-hatch". Wired via --backend lean4. Ground-truthed vs Lean 4.13.0. +# HONESTY FIX exposed by M6 (applies to ALL backends): the `check` command's +# verdict was collapsing to proven-eligible/rejected, mislabelling a clean Lean +# file "rejected" and an SMT `sat` "rejected". Now reports the real verdict word +# (proven-eligible/refuted/unknown/admitted/postulated/rejected); the human line +# drops the assistant-centric ok/FAILED. 119 tests (86 lib + 33 integration; +# +5 lean unit +4 lean-escape unit +2 lean integration). Dogfooded REAL lean: +# clean proof→unknown, sorry→admitted; re-dogfooded z3 sat→refuted, unsat→ +# proven-eligible, agda→proven-eligible; doctor now 6 backends. Follow-ons (the +# 15%): lake-env/LEAN_PATH for project-wide multi-file resolution; the per-decl +# #print axioms audit to promote Unknown→Proven. +# # M0 COMPLETED 2026-07-01: the `arghda doctor` subcommand lands, closing the # last M0 gap. Probes every known backend by running ` --version`; # reports runnable/detail honestly (runnable=false only when the binary truly @@ -162,10 +184,10 @@ milestones = [ [critical-next-actions] actions = [ - "M0 + M1 + M2 + M3 + M4 + M5 DONE. Five backends across both interaction models (agda, agda-cubical, idris2 Assistant; z3, cvc5 Solver) + reasoning graph + doctor. Engine spine core complete. Next:", - "Flying-Logic epic M6: Lean4 adapter (lake build + #print axioms audit → honest Unknown soundness when the audit is absent). Lean 4.13.0 provisioned. Sixth backend.", - "Flying-Logic epic M11: studio JSON freeze (reason/0.1) + Groove /.well-known/groove manifest (the one open v0.1 milestone; `arghda doctor` output feeds it).", + "M0-M6 DONE. SIX backends (agda, agda-cubical, idris2, lean4 Assistant; z3, cvc5 Solver) + reasoning graph + doctor. Engine spine essentially complete. Next:", + "Flying-Logic epic M11: studio JSON freeze (reason/0.1) + Groove /.well-known/groove manifest (the one open v0.1 milestone; `arghda doctor` output feeds the manifest).", "Flying-Logic epic M7: Echidna dispatch seam (feature-gated client, same Outcome).", + "M6 follow-on (15%): lake-env/LEAN_PATH multi-file resolution; per-decl #print axioms audit to promote Unknown→Proven.", "M4 follow-on: .ipkg-declared roots; totality-hole (?name) + per-def `partial` lint.", "M3 follow-on: feed real verdicts into `reason` from a workspace `proven/` state + wire staleness from the content-hash closure (proven.rs).", "M8-M10 heavy tail (Coq/Rocq, Isabelle, Mizar) — gated on --heavy provisioning.", @@ -177,10 +199,10 @@ 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-M0-doctor: 80 lib + 28 integration = 108 tests pass. `arghda doctor` -# dogfooded: 5/5 backends runnable. All five backends dogfooded via real CLI: -# agda + agda-cubical + idris2 (Assistant), z3 + cvc5 (Solver). Dogfooded -# historically against echo-types + agda-unused. +# post-M6: 86 lib + 33 integration = 119 tests pass. `arghda doctor` dogfooded: +# 6/6 backends runnable. All six dogfooded via real CLI: agda + agda-cubical + +# idris2 + lean4 (Assistant), z3 + cvc5 (Solver). Dogfooded historically against +# echo-types + agda-unused. [ecosystem] part-of = ["arghda"] diff --git a/src/lib.rs b/src/lib.rs index 3864c95..7d103bf 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -31,7 +31,8 @@ pub use event::{Event, EventKind}; pub use graph::{build as build_graph, ImportGraph}; pub use lint::{default_rules, rules_with_config, run_lints, LintRule, RuleConfig}; pub use prover::{ - default_backend, Agda, AgdaCubical, Backend, BackendKind, Idris2, Outcome, Probe, Smt, Verdict, + default_backend, Agda, AgdaCubical, Backend, BackendKind, Idris2, Lean, Outcome, Probe, Smt, + Verdict, }; pub use reason::{build as build_reason, Junct, ReasonDocument, ReasonEdge, ReasonNode}; pub use workspace::{StaleEntry, State, Workspace}; diff --git a/src/lint/lean.rs b/src/lint/lean.rs new file mode 100644 index 0000000..9b3bd45 --- /dev/null +++ b/src/lint/lean.rs @@ -0,0 +1,116 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + +//! Lean4 `escape-hatch` (warn) — surface soundness escape hatches. +//! +//! The Lean4 analogue of the Agda/Idris2 escape-hatch rules; shares the rule +//! *name* `escape-hatch` so the reasoning graph caps any hit at amber. +//! +//! Flags `sorry` and `admit` (proof holes), `native_decide` (trusts the +//! compiler's evaluation, outside the kernel) and `unsafe` (bypasses the +//! termination/positivity checks). Lean `--check`/elaboration exits 0 even +//! with `sorry` present (it is only a *warning*), so without this rule — and +//! without the `#print axioms` audit — such gaps ride along invisibly. That +//! is why the Lean backend's own verdict is at best `Unknown` on a green +//! elaboration absent the audit. + +use super::{LintContext, LintRule}; +use crate::diagnostic::{Diagnostic, LintReport, Severity}; +use anyhow::{Context, Result}; +use std::fs; +use std::path::Path; + +pub struct LeanEscapeHatch; + +const ESCAPE_TOKENS: &[&str] = &["sorry", "admit", "native_decide", "unsafe"]; + +impl LintRule for LeanEscapeHatch { + 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, line) in contents.lines().enumerate() { + let trimmed = line.trim_start(); + if trimmed.starts_with("--") { + continue; // whole-line comment + } + let code = line.split(" --").next().unwrap_or(line); + 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), + } +} + +/// `tok` appears in `s` as a delimited token (so `sorryAx_helper` or a +/// namespaced `Foo.admit` do not spuriously match the bare keyword). +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(LeanEscapeHatch)]; + run_lints(tmp.path(), &ctx, &rules).unwrap() + } + + #[test] + fn sorry_is_warned_under_escape_hatch() { + let r = lint_str("theorem t : 1 = 1 := by sorry\n"); + assert_eq!(r.warns().count(), 1); + assert_eq!(r.diagnostics[0].rule, "escape-hatch"); + assert!(r.diagnostics[0].message.contains("sorry")); + } + + #[test] + fn native_decide_and_unsafe_are_warned() { + let r = lint_str("unsafe def f : Nat := 0\nexample : P := by native_decide\n"); + assert_eq!(r.warns().count(), 2); + } + + #[test] + fn escape_token_in_comment_is_ignored() { + let r = lint_str("def x : Nat := 0 -- TODO: no sorry here\n"); + assert!(r.diagnostics.is_empty()); + } + + #[test] + fn clean_lean_file_is_silent() { + let r = lint_str("theorem t : 1 = 1 := rfl\n"); + assert!(r.diagnostics.is_empty()); + } +} diff --git a/src/lint/mod.rs b/src/lint/mod.rs index 878db4b..7f8390f 100644 --- a/src/lint/mod.rs +++ b/src/lint/mod.rs @@ -7,6 +7,7 @@ use std::path::{Path, PathBuf}; pub mod escape_hatch; pub mod idris2; +pub mod lean; pub mod orphan_module; pub mod postulate; pub mod safe_pragma; diff --git a/src/main.rs b/src/main.rs index 38feaab..daa8d44 100644 --- a/src/main.rs +++ b/src/main.rs @@ -5,7 +5,7 @@ use anyhow::{Context, Result}; use arghda_core::lint::LintContext; use arghda_core::{ build_dag, build_reason, event, run_lints, unused, watcher, Agda, AgdaCubical, Backend, - BackendKind, Idris2, LintRule, RuleConfig, Smt, State, Workspace, + BackendKind, Idris2, Lean, LintRule, RuleConfig, Smt, State, Verdict, Workspace, }; use clap::{Parser, Subcommand}; use std::path::{Path, PathBuf}; @@ -16,7 +16,7 @@ use walkdir::WalkDir; type RuleSet = Vec>; /// Every backend `--backend` accepts and `doctor` probes. -const KNOWN_BACKENDS: &[&str] = &["agda", "agda-cubical", "idris2", "z3", "cvc5"]; +const KNOWN_BACKENDS: &[&str] = &["agda", "agda-cubical", "idris2", "lean4", "z3", "cvc5"]; /// Resolve a `--backend` name to a backend instance. Agda is the default and /// v0.1 reference; Idris2 is the estate ABI language. @@ -25,11 +25,12 @@ fn backend_for(name: &str) -> Result> { "agda" => Ok(Box::new(Agda)), "agda-cubical" => Ok(Box::new(AgdaCubical)), "idris2" => Ok(Box::new(Idris2)), + "lean4" => Ok(Box::new(Lean)), "z3" => Ok(Box::new(Smt::z3())), "cvc5" => Ok(Box::new(Smt::cvc5())), - other => { - anyhow::bail!("unknown backend `{other}` (known: agda, agda-cubical, idris2, z3, cvc5)") - } + other => anyhow::bail!( + "unknown backend `{other}` (known: agda, agda-cubical, idris2, lean4, z3, cvc5)" + ), } } @@ -37,7 +38,7 @@ fn backend_for(name: &str) -> Result> { #[command( name = "arghda", version, - about = "Proof-workspace manager for provers/solvers (Agda, Cubical, Idris2, Z3, CVC5)" + about = "Proof-workspace manager for provers/solvers (Agda, Cubical, Idris2, Lean4, Z3, CVC5)" )] struct Cli { #[command(subcommand)] @@ -64,7 +65,8 @@ enum Cmd { /// `/.arghda/config.toml` if present. #[arg(long)] config: Option, - /// Backend: `agda` (default), `agda-cubical`, `idris2`, `z3`, `cvc5`. + /// Backend: `agda` (default), `agda-cubical`, `idris2`, `lean4`, + /// `z3`, `cvc5`. #[arg(long, default_value = "agda")] backend: String, /// Also run the external `agda-unused` analyser and re-emit its @@ -83,7 +85,8 @@ enum Cmd { /// Include root (search path). Defaults to the file's directory. #[arg(long)] include_root: Option, - /// Backend: `agda` (default), `agda-cubical`, `idris2`, `z3`, `cvc5`. + /// Backend: `agda` (default), `agda-cubical`, `idris2`, `lean4`, + /// `z3`, `cvc5`. #[arg(long, default_value = "agda")] backend: String, /// Emit the report as JSON. @@ -106,7 +109,8 @@ enum Cmd { /// `/.arghda/config.toml` if present. #[arg(long)] config: Option, - /// Backend: `agda` (default), `agda-cubical`, `idris2`, `z3`, `cvc5`. + /// Backend: `agda` (default), `agda-cubical`, `idris2`, `lean4`, + /// `z3`, `cvc5`. #[arg(long, default_value = "agda")] backend: String, }, @@ -129,7 +133,8 @@ enum Cmd { /// `/.arghda/config.toml` if present. #[arg(long)] config: Option, - /// Backend: `agda` (default), `agda-cubical`, `idris2`, `z3`, `cvc5`. + /// Backend: `agda` (default), `agda-cubical`, `idris2`, `lean4`, + /// `z3`, `cvc5`. #[arg(long, default_value = "agda")] backend: String, /// Run the backend on every node to populate REAL prover verdicts @@ -405,12 +410,24 @@ fn check(file: &Path, include_root: Option<&Path>, backend_name: &str, json: boo run_lints(file, &ctx, &rules).with_context(|| format!("linting {}", file.display()))?; let outcome = backend.check_file(file, include_root)?; + // Honest verdict: a lint hard-block rejects; otherwise report the + // backend's ACTUAL verdict word. Only `Proven` (with no hard block) is + // "proven-eligible" — a clean-but-unaudited Lean file is `unknown`, an + // SMT `sat` is `refuted`, never silently "rejected"/"ok". let verdict = if !outcome.available { "backend-unavailable" - } else if outcome.ok && !report.has_hard_block() { - "proven-eligible" - } else { + } else if report.has_hard_block() { "rejected" + } else { + match outcome.verdict { + Verdict::Proven => "proven-eligible", + Verdict::Refuted => "refuted", + Verdict::Unknown => "unknown", + Verdict::Admitted => "admitted", + Verdict::Postulated => "postulated", + Verdict::Error => "rejected", + Verdict::Unavailable => "backend-unavailable", + } }; if json { @@ -426,13 +443,12 @@ fn check(file: &Path, include_root: Option<&Path>, backend_name: &str, json: boo println!("{}", file.display()); if outcome.available { println!( - " {}: exit {}, {}", + " {}: exit {}", backend.name(), outcome .exit_code .map(|c| c.to_string()) .unwrap_or_else(|| "?".into()), - if outcome.ok { "ok" } else { "FAILED" } ); } else { println!( diff --git a/src/prover/lean.rs b/src/prover/lean.rs new file mode 100644 index 0000000..884c5db --- /dev/null +++ b/src/prover/lean.rs @@ -0,0 +1,241 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + +//! The Lean4 backend. +//! +//! Assistant model, but with a soundness subtlety Lean forces us to be +//! honest about: `lean ` elaborates and exits 0 *even when the file +//! contains `sorry`* (it is only a warning). A green exit therefore does NOT +//! mean "proven". Ground-truthed against Lean 4.13.0: +//! * exit non-zero → [`Verdict::Error`] (elaboration failed). +//! * exit 0, output mentions `sorry` → [`Verdict::Admitted`] (a hole rode +//! along on a green elaboration). +//! * exit 0, clean → [`Verdict::Unknown`] — the file elaborates, but without +//! a `#print axioms` audit arghda will NOT claim it proven (it could still +//! use `native_decide`, `sorryAx`, or other axioms). Promoting `Unknown` → +//! `Proven` via a per-declaration `#print axioms` audit is the follow-on. +//! * binary absent → [`Verdict::Unavailable`]. +//! +//! Lean modules are dotted (`Mathlib.Data.Nat` ↔ `Mathlib/Data/Nat.lean`), +//! so [`crate::graph::module_name_of`] is reused. Imports are top-level +//! `import Mod` lines; Lean `open` is a *namespace* directive, not a +//! dependency edge, so it is deliberately ignored. Project-wide module +//! resolution (via `lake env` / `LEAN_PATH`) is a documented follow-on; +//! this baseline runs `lean ` directly (core + import-free files). + +use super::{Backend, BackendKind, Outcome, Verdict}; +use crate::graph; +use crate::lint::{lean::LeanEscapeHatch, LintRule, RuleConfig}; +use anyhow::{Context, Result}; +use std::fs; +use std::path::{Path, PathBuf}; +use std::process::Command; +use walkdir::WalkDir; + +const TAIL_LINES: usize = 40; + +/// The Lean4 theorem prover. +#[derive(Clone, Copy, Debug, Default)] +pub struct Lean; + +impl Backend for Lean { + fn name(&self) -> &'static str { + "lean4" + } + + fn kind(&self) -> BackendKind { + BackendKind::Assistant + } + + fn extensions(&self) -> &'static [&'static str] { + &["lean"] + } + + fn safe_mode(&self) -> Option<&'static str> { + // Soundness is established per-declaration via `#print axioms`, not a + // global flag. + Some("#print axioms") + } + + fn check_file(&self, file: &Path, _include_root: &Path) -> Result { + let output = Command::new("lean").arg(file).output(); + 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 verdict = lean_verdict(&combined, 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("lean"); + p + } + + fn direct_imports(&self, file: &Path) -> Result> { + let contents = + fs::read_to_string(file).with_context(|| format!("reading {}", file.display()))?; + let mut out = Vec::new(); + for line in contents.lines() { + let trimmed = line.trim_start(); + if trimmed.starts_with("--") { + continue; + } + let code = trimmed.split(" --").next().unwrap_or(trimmed); + let tokens: Vec<&str> = code.split_whitespace().collect(); + // Top-level `import Mod`. (`open` is a namespace directive, not + // an edge — deliberately not matched.) + if tokens.first() != Some(&"import") { + continue; + } + if let Some(module) = tokens.get(1) { + let cleaned = + module.trim_end_matches(|c: char| !c.is_alphanumeric() && c != '.' && c != '_'); + if !cleaned.is_empty() { + out.push(cleaned.to_string()); + } + } + } + Ok(out) + } + + fn discover_roots(&self, include_root: &Path) -> Vec { + // Lean's roots are declared in a lakefile (a documented follow-on); + // the executable convention is `Main.lean`. + 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.extension().and_then(|s| s.to_str()) != Some("lean") { + continue; + } + if path.file_name().and_then(|s| s.to_str()) == Some("Main.lean") { + roots.push(path.to_path_buf()); + } + } + roots.sort(); + roots + } + + fn lint_rules(&self, _cfg: &RuleConfig) -> Result>> { + Ok(vec![Box::new(LeanEscapeHatch)]) + } + + fn command(&self) -> &'static str { + "lean" + } +} + +/// Map Lean output + exit status to a [`Verdict`], honestly: a green exit is +/// only `Unknown` (elaborated, un-audited) unless `sorry` is present, which +/// makes it `Admitted`. Never `Proven` without a `#print axioms` audit. +fn lean_verdict(output: &str, exit_ok: bool) -> Verdict { + if !exit_ok { + return Verdict::Error; + } + // Lean prints `declaration uses 'sorry'` (and `#print axioms` shows + // `sorryAx`) — parse the tool's own diagnostic, not the source. + if output.contains("sorry") { + return Verdict::Admitted; + } + Verdict::Unknown +} + +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") +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn lean_backend_identity() { + assert_eq!(Lean.name(), "lean4"); + assert_eq!(Lean.kind(), BackendKind::Assistant); + assert_eq!(Lean.extensions(), &["lean"]); + assert_eq!(Lean.command(), "lean"); + } + + #[test] + fn module_to_path_uses_lean_extension() { + assert_eq!( + Lean.module_to_path("Mathlib.Data.Nat", Path::new("/r")), + PathBuf::from("/r/Mathlib/Data/Nat.lean") + ); + } + + #[test] + fn imports_parsed_open_ignored() { + let tmp = tempfile::NamedTempFile::new().unwrap(); + std::fs::write( + tmp.path(), + "import Mathlib.Data.Nat\n\ + open Nat\n\ + import Std.Data.List\n\ + -- import Ignored\n", + ) + .unwrap(); + let imports = Lean.direct_imports(tmp.path()).unwrap(); + assert!(imports.contains(&"Mathlib.Data.Nat".to_string())); + assert!(imports.contains(&"Std.Data.List".to_string())); + assert!(!imports.iter().any(|i| i == "Nat"), "`open` is not an edge"); + assert!(!imports.iter().any(|i| i.contains("Ignored"))); + } + + #[test] + fn verdict_is_honest_about_sorry_and_the_missing_audit() { + // A green elaboration is only Unknown without a #print axioms audit; + // a sorry warning makes it Admitted; a failure is Error. + assert_eq!(lean_verdict("", true), Verdict::Unknown); + assert_eq!( + lean_verdict("Foo.lean:1:8: warning: declaration uses 'sorry'", true), + Verdict::Admitted + ); + assert_eq!(lean_verdict("error: type mismatch", false), Verdict::Error); + } + + #[test] + fn check_file_is_honest_about_availability() { + let tmp = tempfile::tempdir().unwrap(); + let f = tmp.path().join("T.lean"); + std::fs::write(&f, "theorem t : 1 = 1 := rfl\n").unwrap(); + let out = Lean.check_file(&f, tmp.path()).unwrap(); + if out.available { + // Never fabricated Proven: a clean Lean file is Unknown (audit + // absent), a sorry file Admitted, a broken file Error. + assert!(matches!( + out.verdict, + Verdict::Unknown | Verdict::Admitted | Verdict::Error + )); + assert!(!out.ok, "lean never reports `ok` without an axioms audit"); + } else { + assert_eq!(out.verdict, Verdict::Unavailable); + } + } +} diff --git a/src/prover/mod.rs b/src/prover/mod.rs index 7d5cbca..04a06e1 100644 --- a/src/prover/mod.rs +++ b/src/prover/mod.rs @@ -29,10 +29,12 @@ use std::process::Command; pub mod agda; pub mod idris2; +pub mod lean; pub mod smt; pub use agda::{Agda, AgdaCubical}; pub use idris2::Idris2; +pub use lean::Lean; pub use smt::Smt; /// The two backend interaction models. diff --git a/tests/fixtures/lean/Main.lean b/tests/fixtures/lean/Main.lean new file mode 100644 index 0000000..43849be --- /dev/null +++ b/tests/fixtures/lean/Main.lean @@ -0,0 +1,3 @@ +import Util + +def main : IO Unit := IO.println greeting diff --git a/tests/fixtures/lean/Util.lean b/tests/fixtures/lean/Util.lean new file mode 100644 index 0000000..de95446 --- /dev/null +++ b/tests/fixtures/lean/Util.lean @@ -0,0 +1 @@ +def greeting : String := "hi" diff --git a/tests/lean.rs b/tests/lean.rs new file mode 100644 index 0000000..1bf7378 --- /dev/null +++ b/tests/lean.rs @@ -0,0 +1,58 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell + +//! Lean4 backend, exercised through the backend-parametric graph/dag/reason +//! path. Hermetic — parses `.lean` text only, so it runs with or without the +//! `lean` binary. The real elaboration + honest-verdict path (`check_file`) +//! is covered by the unit tests in `src/prover/lean.rs` and by dogfooding. + +use arghda_core::lint::unpinned_headline::DEFAULT_HEADLINE_PATTERN; +use arghda_core::{build_dag, build_reason, Backend, Lean, LintRule}; +use std::collections::{BTreeMap, BTreeSet}; +use std::path::PathBuf; + +fn lean_fixture() -> PathBuf { + let mut p = PathBuf::from(env!("CARGO_MANIFEST_DIR")); + p.push("tests"); + p.push("fixtures"); + p.push("lean"); + p +} + +fn no_rules() -> Vec> { + Vec::new() +} + +#[test] +fn lean_import_graph_and_root() { + let root = lean_fixture(); + let roots = Lean.discover_roots(&root); + let names: Vec = roots + .iter() + .map(|p| p.file_name().unwrap().to_str().unwrap().to_string()) + .collect(); + assert_eq!(names, vec!["Main.lean".to_string()]); + + let dag = build_dag(&root, &roots, &no_rules(), DEFAULT_HEADLINE_PATTERN, &Lean).unwrap(); + let mut ids: Vec<&str> = dag.nodes.iter().map(|n| n.id.as_str()).collect(); + ids.sort_unstable(); + assert_eq!(ids, vec!["Main", "Util"]); + // `import Util` becomes an edge; `open` (none here) would not. + assert!(dag + .edges + .iter() + .any(|e| e.from == "Main" && e.to == "Util" && e.kind == "imports")); +} + +#[test] +fn lean_reason_graph_wires_the_main_cone() { + let root = lean_fixture(); + let roots = Lean.discover_roots(&root); + let dag = build_dag(&root, &roots, &no_rules(), DEFAULT_HEADLINE_PATTERN, &Lean).unwrap(); + let doc = build_reason(dag, &Lean, &BTreeMap::new(), &BTreeSet::new()); + + assert_eq!(doc.crt_roots, vec!["Main".to_string()]); + let wired = |id: &str| doc.nodes.iter().find(|n| n.id == id).unwrap().wired; + assert!(wired("Main")); + assert!(wired("Util")); +}