Inspect a Lean project

Inspection command map

A successful build tells you Lean accepted the project. It does not tell you which recorded target inputs changed, which module defines a declaration, or whether a theorem reaches an axiom through several definitions.

Project diagnosis

When a project fails on one machine but not another, the first useful artifact is usually a small inventory: which root did the command discover, which toolchain did it select, can the Lakefile and manifest be parsed, does the lock agree, and is there any build metadata to inspect? Bare lev inspect collects that without synchronizing, building, or repairing anything.

lev inspect
lev inspect --json
lev inspect --json > lev-diagnosis.json

Lev 1.0.0 diagnosis
host: linux-x86_64
start: /tmp/lev-doc-example.A1b2C3/project
cache: /tmp/lev-doc-example.A1b2C3/cache
toolchains: /tmp/lev-doc-example.A1b2C3/data/toolchains-v1

Project
  root: /tmp/lev-doc-example.A1b2C3/project
  toolchain: leanprover/lean4:v4.docs
  Lakefile: /tmp/lev-doc-example.A1b2C3/project/lakefile.toml (toml)
  manifest: /tmp/lev-doc-example.A1b2C3/project/lake-manifest.json (0 packages)
  lev.toml: absent
  configured tasks/checks: 0/0
  build metadata: absent
  runtime: elan

Checks
  PASS  project    found /tmp/lev-doc-example.A1b2C3/project
  PASS  lakefile   parsed lakefile.toml (0 direct dependencies)
  PASS  manifest   parsed lake-manifest.json (0 packages)
  WARN  lock       lev.lock is missing; run `lev lock`
  PASS  lev.toml   no lev.toml; ordinary Lake defaults are active
  PASS  toolchain  leanprover/lean4:v4.docs is available through elan

Summary: 5 passed, 1 warnings, 0 errors

Next
  lev inspect build
  lev inspect dependencies
  lev inspect performance --files
  lev inspect imports --coverage
  lev inspect trust
  lev check

Repeated project paths are shortened here so the page stays readable. The command itself prints complete paths, which is what you want in a bug report or CI artifact.

Check the machine without changing it

Use the environment report to see which lean and lake the checkout will run, where lev stores local state, and whether the directory belongs to a configured workspace.

The command checks Git and elan, resolves the selected runtime, asks that runtime for Lean and Lake versions, reads the project files, and inspects Lev's registry, artifact-cache path, workspace configuration, and managed-workspace marker. It does not synchronize dependencies, create cache directories, or crawl .lake.

lev inspect environment
lev inspect environment --json
lev inspect environment --json -o environment.json

# Visible direct command, same report
lev doctor --json -o environment.json

Lev 1.0.0 environment
Host: linux-x86_64

Locations
  project start: /tmp/lev-doc-env.Rt42/project
  lev cache: /tmp/lev-doc-env.Rt42/lev-cache
  toolchain data: /tmp/lev-doc-env.Rt42/lev-data/toolchains-v1

Tools
  Git: git version 2.50.1
  elan: elan 4.2.3 (b6cec7e10 2026-06-08)
  project: /tmp/lev-doc-env.Rt42/project
  toolchain: leanprover/lean4:v4.30.0
  runtime: elan
  Lean: Lean (version 4.30.0, x86_64-unknown-linux-gnu, commit d024af099ca4bf2c86f649261ebf59565dc8c622, Release)
  Lake: Lake version 5.0.0-src+d024af0 (Lean version 4.30.0)

Local state
  registry: /tmp/lev-doc-env.Rt42/lev-cache/projects-v1 (0 records, 0 stale)
  Lake artifact cache: /tmp/lev-doc-env.Rt42/lev-cache/lake-v1/95902a685e480b41 (not created)
  workspace: not configured
  managed local workspace: no

Findings
  PASS  environment.locations            resolved the project start, cache, and toolchain data paths
  PASS  environment.git.version          git version 2.50.1
  PASS  environment.elan.version         elan 4.2.3 (b6cec7e10 2026-06-08)
  PASS  project.discovery                found /tmp/lev-doc-env.Rt42/project
  PASS  project.toolchain_file           selected leanprover/lean4:v4.30.0
  PASS  project.lakefile                 parsed /tmp/lev-doc-env.Rt42/project/lakefile.toml with 0 direct dependencies
  WARN  project.manifest                 /tmp/lev-doc-env.Rt42/project/lake-manifest.json is missing
  WARN  project.lock                     /tmp/lev-doc-env.Rt42/project/lev.lock is missing
  PASS  project.lev_config               no lev.toml; Lake defaults are active
  PASS  environment.runtime.selected     leanprover/lean4:v4.30.0 will run through elan
  PASS  environment.lean.version         Lean (version 4.30.0, x86_64-unknown-linux-gnu, commit d024af099ca4bf2c86f649261ebf59565dc8c622, Release)
  PASS  environment.lake.version         Lake version 5.0.0-src+d024af0 (Lean version 4.30.0)
  PASS  cache.artifacts.path             selected cache directory has not been created at /tmp/lev-doc-env.Rt42/lev-cache/lake-v1/95902a685e480b41
  PASS  cache.registry.records           parsed 0 project records
  PASS  cache.registry.staleness         all parsed project records still match their project
  N/A   workspace.configuration          no ancestor lev.toml declares [workspace]
  N/A   workspace.validity               no ancestor lev.toml declares [workspace]
  N/A   workspace.lock                   no ancestor lev.toml declares [workspace]
  PASS  workspace.managed_local          /tmp/lev-doc-env.Rt42/project is a user-owned project

Summary: 14 passed, 2 warnings, 0 errors, 3 not applicable

The missing manifest and lock remain visible as findings. The inspector observes the machine and checkout without creating either file.

One finding, field by field

The JSON report uses the same Finding shape as Lev's other diagnostics. A finding records the observed condition and its evidence before any policy decides whether it should stop a run.

{
  "id": "environment.runtime.selected",
  "category": "environment",
  "state": "passed",
  "severity": "info",
  "title": "Selected runtime",
  "detail": "leanprover/lean4:v4.30.0 will run through elan",
  "evidence": {
    "source": "elan",
    "toolchain": "leanprover/lean4:v4.30.0"
  },
  "policy": "observe"
}

id is the stable key for scripts. state says whether the check passed, raised a finding, or did not apply. severity classifies what Lev observed. policy is separate: observe records the result, while fail makes a policy command reject it. Optional remediation and elapsed_ms fields appear when Lev has a concrete next step or timing.

Dependency revision selection

Lake can receive different revisions of the same package through different parents. In Lean issue #13084, reference-manual selected a subverso revision requested by versowebcomponents; the root requirement appeared earlier but did not win. David Christiansen suggested warning when direct dependencies pin an indirect dependency differently and naming which one wins. The report shows which revision was selected and what each parent requested.

lev inspect dependencies
lev inspect dependencies --json
lev inspect dependencies --json -o dependency-pins.json

dependency pins for root: 2 aligned, 1 conflict, 1 root override, 1 stale, 1 unknown
CONFLICT aaaaaaaaaaaa conflict
  requested by parent-a: aaaaaaaaaaaa
  requested by parent-b: bbbbbbbbbbbb
OVERRIDE aaaaaaaaaaaa override
  requested by parent-a: bbbbbbbbbbbb
  requested by root: aaaaaaaaaaaa
ALIGNED  aaaaaaaaaaaa parent-a
  requested by root: aaaaaaaaaaaa
ALIGNED  aaaaaaaaaaaa parent-b
  requested by root: aaaaaaaaaaaa
STALE    aaaaaaaaaaaa stale
  requested by parent-a: bbbbbbbbbbbb
  requested by parent-b: cccccccccccc
UNKNOWN  -            unknown
  requested by root: -

This example comes from a lev CLI contract test. The repeated letters make the three revisions easy to distinguish; they are not package commits from a real project.

Lev reads the root lake-manifest.json and each materialized parent's manifest. The command is read-only: it never runs dependency resolution, updates a revision, or edits a manifest. One missing parent makes any conclusion that depends on complete evidence unknown; Lev names the missing manifest in warnings. Only a provably stale selection fails the dependency phase of lev check.

Build trace changes

Lake records a trace beside a built target. The trace contains the inputs Lake used to decide whether the result was current. lev inspect build snapshots those files, runs lake --verbose build, then compares the snapshots. The verbose stream says what Lake labeled Built, Replayed, Reused, Fetched, Ran, or Unpacked. The trace comparison identifies changed source, dependency, option, toolchain, and configuration inputs when Lake labels them.

For a changed project source, Lev also reads the project's import graph in reverse. If B imports A and C imports B, changing A makes A, B, and C part of the potential source impact. That says where the edit could matter. It stays separate from the modules Lake reported as built during this run.

Lean issue #7280 shows how one failed dependency can produce a long tail of transitive build failures. Lev keeps location-bearing Lean diagnostics, removes duplicate messages, and lists failed targets separately. The compatibility field root_causes contains diagnostic leads; it does not claim that every early line caused every later failure.

In a February 2026 Zulip thread, a project appeared to compile Mathlib twice. The extra work came from an executable target created by the project template. Lake issue #153 records another case where files appeared to build twice instead of reusing prior work. The inspector puts target names, visible trace inputs, and observed build events beside each other so you can see exactly which evidence Lake left behind.

edited A.lean
   +-- Lake verbose event --------------> observed Built: A
   `-- reverse project imports ---------> potential: A, B, C
                                             A -> B -> C

lev inspect build
lev inspect build MyLibrary
lev inspect build --json -o build-inspection.json

build passed in 749.443 ms: 3 built, 0 replayed, 3 ran, 0 reused, 0 fetched, 0 unpacked
RAN                    job computation
RAN                    demo:extraDep
BUILT       234.000 ms  Demo.Root
BUILT       231.000 ms  Demo.UsesRoot
BUILT       228.000 ms  Demo
RAN                    demo/Demo:default
trace inputs:
  Demo [changed]: one or more labeled Lake trace inputs changed
    dependency: Demo:deps / deps / imports / Demo.UsesRoot transitive imports (legacy)
    dependency: Demo:deps / deps / imports / Demo.UsesRoot:importAllArts
  Demo.Root [changed]: one or more labeled Lake trace inputs changed
    source: /tmp/lev-doc-env.Rt42/project/Demo/Root.lean
  Demo.UsesRoot [changed]: one or more labeled Lake trace inputs changed
    dependency: Demo.UsesRoot:deps / deps / imports / Demo.Root:importAllArts
causality:
  changed source modules: Demo.Root
  Lake-reported built modules: Demo, Demo.Root, Demo.UsesRoot
  potential project impact: Demo, Demo.Root, Demo.UsesRoot
    could affect: Demo.Root -> Demo.UsesRoot -> Demo
    could affect: Demo.Root
    could affect: Demo.Root -> Demo.UsesRoot

This example starts from an initial build, edits Demo/Root.lean, then inspects the next verbose build. The elapsed values are ordinary command output; use the module lists and trace-input labels to understand why Lake considered work current or stale.

{
  "source_graph_available": true,
  "changed_project_modules": ["Demo.Root"],
  "observed_rebuilt_modules": [
    "Demo",
    "Demo.Root",
    "Demo.UsesRoot"
  ],
  "evidence_kinds": [
    "observed_trace",
    "source_import_graph"
  ],
  "potential_affected_modules": [
    "Demo",
    "Demo.Root",
    "Demo.UsesRoot"
  ],
  "missing_evidence": [],
  "warnings": []
}

The source graph records imports between project modules. Lake facets, custom needs, plugins, generated targets, external package internals, and Lake's complete job DAG remain outside that graph. A path such as A -> B -> C is the shortest source-import explanation Lev found; Lake may have scheduled the jobs through other dependencies.

Find a declaration without guessing the import

A declaration name is often easier to remember than its module. Lev searches bounded .ilean indexes from the project and its Lake dependencies. Once it has a candidate module, it writes a temporary Lean file containing that import and #check NAME. The displayed type therefore comes from the selected Lean environment, not from a text parser.

lev inspect declaration usesShared

lev inspect declaration Nat.add_comm \
  --from Mathlib.Data.Nat.Basic

lev inspect declaration usesShared --build --json

usesShared
  type:    shared = trustBase + 1
  module:  TrustSmoke.Basic
  import:  import TrustSmoke.Basic
  package: TrustSmoke
  source:  /tmp/lev-trust-432.jxybrG/TrustSmoke/Basic.lean:5:9

--build refreshes metadata before searching. --from MODULE skips index discovery when you already know the module or need a declaration from the Lean toolchain itself. If the same name appears in several indexed modules, lev asks you to choose rather than picking the first match.

Project-wide trust audit

A text search for sorry is useful while editing, but it answers a source-code question. Trust review needs the elaborated environment. A theorem can inherit sorryAx, Classical.choice, or a project axiom through declarations whose source contains none of those names. In mathlib issue #272, a nomatch term unexpectedly introduced sorryAx; searching for a literal sorry would not have explained that result.

The scratch project below is small enough to see the transitive case. usesShared mentions shared; both depend on trustBase.

axiom trustBase : Nat

noncomputable def shared : Nat := trustBase + 1

theorem usesShared : shared = trustBase + 1 := rfl

unsafe def unchecked : Nat := 1

trust: scanned 4 of 4 indexed declarations;
3 with axioms, 1 unsafe
AXIOMS        shared
  module: TrustSmoke.Basic
  axioms: trustBase
AXIOMS        trustBase
  module: TrustSmoke.Basic
  axioms: trustBase
UNSAFE        unchecked
  module: TrustSmoke.Basic
AXIOMS        usesShared
  module: TrustSmoke.Basic
  axioms: trustBase
policy: passed

Lev first reads the project's built .ilean files to obtain declaration names, owning modules, and source ranges. It then generates bounded Lean probes that import those modules and call Lean's built-in collectAxioms once for each indexed declaration. Each probe also reads the declaration's isUnsafe flag. Lev joins the returned records to the index; it does not reimplement Lean's axiom traversal in Rust.

That join must be complete. If Lean returns no record for an indexed name, or reports that the name was not found after its module was imported, lev counts a scan failure and exits with status 1. A partial scan cannot pass by quietly shrinking the denominator.

Source search, #print axioms, and project inspection

None of these labels an axiom as a mistake. Projects use axioms for different reasons, and Classical.choice is common in noncomputable mathematics. Lev keeps discovery separate from policy so the project can state what it forbids.

Trust policy

When the scan completes, a plain trust inspection exits successfully after reporting its findings. Add one or more --deny flags or --deny-unsafe to make those findings fail CI.

lev inspect trust --deny sorryAx
lev inspect trust --deny sorryAx --deny Classical.choice
lev inspect trust --deny-unsafe
lev inspect trust --deny trustBase --deny-unsafe --json
lev inspect trust --no-build --json > trust.json

{
  "schema": "lev.cli.inspect.trust/v1",
  "data": {
    "toolchain": "leanprover/lean4:v4.32.2",
    "status": "failed",
    "declarations_indexed": 4,
    "declarations_scanned": 4,
    "scan_failures": 0,
    "declarations_with_axioms": 3,
    "unsafe_declarations": 1,
    "denied_axioms": ["trustBase"],
    "deny_unsafe": true,
    "policy_violations": 4
  }
}

This excerpt keeps the counters together. The complete report also includes the project path, one structured entry per declaration in findings, and any index or scan messages in warnings.

--no-build is useful after a separate build step. Without it, lev builds first so the index and environment agree. A denied axiom, denied unsafe declaration, or incomplete scan returns status 1. Build failures and malformed or conflicting indexes return an error before policy evaluation; scan_failures remains separate from policy_violations in JSON.

What the reports can and cannot say

• Dependency inspection can explain only requests present in the root and materialized parent manifests. Missing parent manifests or revisions produce unknown, not a reconstructed guess. The report describes the recorded graph; it does not predict what a fresh Lake update would select.
• Build inspection reports changes visible in Lake's persisted trace format. A Built target with no matching changed trace target is reported as unattributed. Routine Ran jobs remain in the event list but are not classified as unexplained compilation.
• Build causality uses exact changed project-source paths as seeds. Reverse imports provide a potential project impact, while Lake's verbose Built events provide the observed rebuilt modules. Neither list is inferred from the other.
• The source graph does not include Lake facets, custom needs, plugins, generated targets, external package internals, or the complete Lake job DAG.
• Build event times come from Lake's verbose lines. End-to-end elapsed time includes the complete delegated process; neither value attributes time to tactics or functions.
• Declaration and trust inspection need built .ilean metadata. Stale duplicate declaration entries are rejected with a clean-and-rebuild instruction.
• Trust inspection scans declarations owned by the root project. Imported packages still appear in transitive axiom closures, but their declarations are not listed as project findings.
• An empty axiom list is one useful kernel-level fact. It is not a review of theorem statements, native code, foreign libraries, or the Lean kernel itself.