diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 9cf8ce7..09f9acc 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 = 95 }, { 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 = 92 }, + { 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 = 90 }, { name = "M9: Isabelle adapter (--heavy; dogfood tropical-resource-typing .thy)", completion = 90 }, @@ -114,6 +114,22 @@ milestones = [ # --backend idris2` over an ipkg fixture → crt_roots ['App'], App+Helper wired. # M4 now 95% (remaining: totality-hole `?name` + per-def `partial` lint). # +# M6 FOLLOW-ON landed 2026-07-01 (M6 → 100%): lake-env import resolution — the +# Lean audit now reaches IMPORTED files, not just import-free ones. When a +# `lakefile.lean`/`lakefile.toml` is found at/above the file (`lake_root`), both +# the elaboration and the `#print axioms` audit run via `lake env lean` with +# cwd = the lake root, so the project's LEAN_PATH resolves project-local imports +# (`run_lean` helper; falls back to bare `lean` when there's no lakefile, or if +# `lake` is absent). The audit copy stays in a clean temp dir — LEAN_PATH +# entries are absolute, so imports resolve regardless of the copy's location +# (ground-truthed). Assumes the project is already built (arghda checks proofs, +# it does not run `lake build` — a deliberate scope line, not a gap). 168 tests +# (+1 lake_root unit). DOGFOODED vs real Lean 4.13.0 + Lake 5.0.0 on a built +# lake project: the importing file `Demo.lean` (imports Demo.Basic) → proven +# (was an unresolved-import error pre-M6); leaf → proven; negative control (same +# file copied OUTSIDE the lake project) → error, confirming the fix is the +# lake-env resolution specifically. +# # M3 FOLLOW-ON landed 2026-07-01: workspace-fed verdicts + staleness in `reason` # — the reasoning graph now sources REAL verdicts from a four-state workspace's # `proven/` state, no re-check needed. New `arghda reason --workspace @@ -375,13 +391,13 @@ milestones = [ actions = [ "ENGINE-SPINE DELIVERABLE COMPLETE: M0-M7 + M11 all landed. v0.1 spec closed. Six backends (agda, agda-cubical, idris2, lean4 Assistant; z3, cvc5 Solver) + reasoning graph + doctor + groove + dispatch seam. Remaining work is refinement + the heavy tail:", "M7 follow-on: the real Echidna orchestrator HTTP client (feature-gated), once Echidna's API is confirmed — only Dispatch::run changes.", - "M6 follow-on: #print axioms audit DONE (import-free files promote honestly); remaining = lake-env/LEAN_PATH so imported files can be checked + audited too.", + "M6 follow-on: DONE (M6 → 100%) — lake-env resolution (`lake env lean` under a lakefile) so IMPORTED Lean files elaborate + get #print-axioms-audited too, not just import-free ones. Dogfooded on a built lake project.", "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 (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.", - "Next, climb up: M6 (lake-env/LEAN_PATH so imported Lean files get audited), M4 (totality-hole ?name + per-def partial lint for Idris2), M7 (real Echidna HTTP client, feature-gated). Each its own focused draft PR, gate green, real-tool dogfood where installed.", + "Next, climb up: M4 (totality-hole ?name + per-def partial lint for Idris2), M7 (real Echidna HTTP client, feature-gated — but FIRST confirm Echidna's API actually exists; if not, keep the honest stub). Each its own focused draft PR, gate green, real-tool dogfood where installed.", ] [maintenance-status] @@ -390,7 +406,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: 124 lib + 43 integration = 167 tests pass. codeql.yml added +# post-M6-followon: 125 lib + 43 integration = 168 tests pass. M6 lake-env +# import resolution dogfooded vs real Lean 4.13.0 + Lake 5.0.0 (imported file in +# a built lake project → proven; outside → error). codeql.yml added # (code-scanning gate fix). M10 Mizar adapter dogfooded vs real Mizar 8.1.15 # (proven/error via accom+verifier+.err; MIZFILES=/opt/mizar; doctor [OK] # mizar). M9 Isabelle dogfooded vs Isabelle2025; M8 Coq dogfooded vs coqc diff --git a/src/prover/lean.rs b/src/prover/lean.rs index 666fdb7..7de98f8 100644 --- a/src/prover/lean.rs +++ b/src/prover/lean.rs @@ -19,16 +19,19 @@ //! modules the bare temp-dir copy can't resolve), it stays `Verdict::Unknown`. //! * binary absent → [`Verdict::Unavailable`]. //! -//! The audit currently reaches import-free files (a temp-dir copy elaborates -//! them without `LEAN_PATH`); auditing imported files needs `lake env` -//! resolution — a documented follow-on. +//! Import resolution: when a `lakefile.lean`/`lakefile.toml` is found at or +//! above the file, both the elaboration and the `#print axioms` audit run +//! under `lake env lean` (cwd = the lake root), which injects the project's +//! `LEAN_PATH` — so IMPORTED files elaborate and get audited too, not just +//! import-free ones. (This assumes the project is already built; arghda checks +//! proofs, it does not run `lake build`.) With no lakefile, it falls back to +//! bare `lean ` (core + import-free files); if `lake` is somehow absent, +//! it also falls back to bare `lean`. //! //! 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). +//! dependency edge, so it is deliberately ignored. use super::{Backend, BackendKind, Outcome, Verdict}; use crate::graph; @@ -70,8 +73,11 @@ impl Backend for Lean { Some("#print axioms") } - fn check_file(&self, file: &Path, _include_root: &Path) -> Result { - let output = Command::new("lean").arg(file).output(); + fn check_file(&self, file: &Path, include_root: &Path) -> Result { + // Under a lake project, run via `lake env lean` so project-local + // imports resolve; otherwise bare `lean`. + let lake = lake_root(file, include_root); + let output = run_lean(file, lake.as_deref()); match output { Ok(out) => { let mut combined = String::from_utf8_lossy(&out.stdout).into_owned(); @@ -81,10 +87,10 @@ impl Backend for Lean { // `#print axioms` audit to promote it honestly: Proven if every // declaration depends only on the standard axioms, Postulated // if a non-standard axiom (e.g. `native_decide`'s) sneaks in, - // Admitted on sorryAx. If the audit can't run (imports need - // lake, no declarations, tool absent) it stays `Unknown`. + // Admitted on sorryAx. If the audit can't run (unbuilt imports, + // no declarations, tool absent) it stays `Unknown`. if verdict == Verdict::Unknown { - if let Some(audited) = axiom_audit(file) { + if let Some(audited) = axiom_audit(file, lake.as_deref()) { verdict = audited; } } @@ -268,12 +274,15 @@ fn classify_axioms(output: &str) -> Verdict { } /// Run a `#print axioms` audit on `file`'s declarations. Copies the source -/// into a fresh temp dir, appends `#print axioms ` per declaration, -/// and runs `lean`. Returns the classified verdict, or `None` when the audit -/// can't be trusted — no declarations, `lean` absent, or the copy fails to -/// elaborate (e.g. it imports modules that need `lake env`/`LEAN_PATH`, which -/// a bare temp dir lacks). `None` ⇒ the caller keeps the honest `Unknown`. -fn axiom_audit(file: &Path) -> Option { +/// into a fresh temp dir, appends `#print axioms ` per declaration, and +/// elaborates it — under `lake env lean` when `lake_root` is `Some` (so the +/// project's `LEAN_PATH` resolves imported modules), else bare `lean`. Because +/// `LEAN_PATH` entries are absolute, the audit copy can stay in a clean temp +/// dir even for imported files. Returns the classified verdict, or `None` when +/// the audit can't be trusted — no declarations, `lean` absent, or the copy +/// fails to elaborate (e.g. an import whose `.olean` isn't built). `None` ⇒ +/// the caller keeps the honest `Unknown`. +fn axiom_audit(file: &Path, lake_root: Option<&Path>) -> Option { let src = fs::read_to_string(file).ok()?; let names = decl_names(&src); if names.is_empty() { @@ -295,9 +304,9 @@ fn axiom_audit(file: &Path) -> Option { let audit_file = dir.join("Audit.lean"); let verdict = match fs::write(&audit_file, &body) { - Ok(()) => match Command::new("lean").arg(&audit_file).output() { + Ok(()) => match run_lean(&audit_file, lake_root) { // Only trust the audit if the copy elaborated cleanly; otherwise - // (imports unresolved in the temp dir, etc.) stay Unknown. + // (an import whose .olean isn't built, etc.) stay Unknown. Ok(out) if out.status.success() => { let mut combined = String::from_utf8_lossy(&out.stdout).into_owned(); combined.push_str(&String::from_utf8_lossy(&out.stderr)); @@ -312,6 +321,39 @@ fn axiom_audit(file: &Path) -> Option { verdict } +/// Find the lake project root at or above `file` (or `include_root`): the +/// nearest ancestor directory containing a `lakefile.lean` or `lakefile.toml`. +/// `None` ⇒ not a lake project (bare-`lean` fallback). +fn lake_root(file: &Path, include_root: &Path) -> Option { + let start = file.parent().unwrap_or(include_root); + for dir in start.ancestors().chain(include_root.ancestors()) { + if dir.join("lakefile.lean").is_file() || dir.join("lakefile.toml").is_file() { + return Some(dir.to_path_buf()); + } + } + None +} + +/// Elaborate `file` with Lean. Under a lake project (`lake_root` = `Some`), run +/// `lake env lean ` with cwd = the lake root so `LEAN_PATH` resolves +/// project imports; if `lake` itself is absent, fall back to bare `lean`. With +/// no lake project, run bare `lean `. +fn run_lean(file: &Path, lake_root: Option<&Path>) -> std::io::Result { + if let Some(root) = lake_root { + match Command::new("lake") + .arg("env") + .arg("lean") + .arg(file) + .current_dir(root) + .output() + { + Err(e) if e.kind() == std::io::ErrorKind::NotFound => {} // fall back to bare lean + other => return other, + } + } + Command::new("lean").arg(file).output() +} + #[cfg(test)] mod tests { use super::*; @@ -408,6 +450,24 @@ example : True := trivial\n\ assert_eq!(lean_verdict("error: type mismatch", false), Verdict::Error); } + #[test] + fn lake_root_found_at_ancestor() { + // A file two dirs below a lakefile resolves to the lake root; a tree + // with no lakefile resolves to None (bare-lean fallback). + let tmp = tempfile::tempdir().unwrap(); + let root = tmp.path(); + std::fs::write(root.join("lakefile.toml"), "name = \"demo\"\n").unwrap(); + std::fs::create_dir_all(root.join("Demo")).unwrap(); + let deep = root.join("Demo/Basic.lean"); + std::fs::write(&deep, "def x : Nat := 0\n").unwrap(); + assert_eq!(lake_root(&deep, root).as_deref(), Some(root)); + + let bare = tempfile::tempdir().unwrap(); + let f = bare.path().join("T.lean"); + std::fs::write(&f, "theorem t : True := trivial\n").unwrap(); + assert_eq!(lake_root(&f, bare.path()), None); + } + #[test] fn check_file_is_honest_about_availability() { let tmp = tempfile::tempdir().unwrap();