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

[hyperpolymath]

What

The Lean #print axioms audit now reaches imported files, not just import-free ones — closing the last M6 follow-on (M6 → 100%).

When a lakefile.lean/lakefile.toml is found at or above the file, both the elaboration and the audit run via lake env lean (cwd = the lake root), injecting the project's LEAN_PATH so project-local imports resolve.

How

• lake_root(file, include_root) — the nearest ancestor directory with a lakefile, else None (bare-lean fallback).
• run_lean(file, lake_root) — lake env lean <file> under a lake project (cwd = root), falling back to bare lean when there's no lakefile or lake itself is absent. Both check_file and axiom_audit route through it.
• 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). With no lakefile the behaviour is unchanged (core + import-free files via bare lean).

Verification (actually run)

• cargo fmt --check — clean
• cargo clippy --all-targets -- -D warnings — clean
• cargo test — 168 pass (+1 lake_root unit)
• bash scripts/check-spdx.sh . — OK

Dogfooded vs real Lean 4.13.0 + Lake 5.0.0 on a built lake project:

file	before M6	now
Demo.lean (imports Demo.Basic), inside the built lake project	unresolved-import error	proven
Demo/Basic.lean (leaf, no imports)	proven	proven
same importing file copied outside a lake project	—	error (negative control — confirms the fix is the lake-env resolution)

Scope

M6 complete. The remaining climb: M4 (Idris2 totality-hole/partial lint), M7 (real Echidna client — pending confirmation its API exists).

🤖 Generated with Claude Code

https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7

---

Generated by Claude Code