ArghDA M6 follow-on: lake-env import resolution (M6 → 100%)

.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 <path> --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 <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 (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

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 <file>` (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 <file>` 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<Outcome> {
-        let output = Command::new("lean").arg(file).output();
+    fn check_file(&self, file: &Path, include_root: &Path) -> Result<Outcome> {
+        // 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 <name>` 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<Verdict> {
+/// into a fresh temp dir, appends `#print axioms <name>` 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<Verdict> {
     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<Verdict> {
     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> {
     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<PathBuf> {
+    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 <file>` 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 <file>`.
+fn run_lean(file: &Path, lake_root: Option<&Path>) -> std::io::Result<std::process::Output> {
+    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();