Checked example🔗

/-! # Reflexivity

Reflexivity for every natural number. -/
theorem reflexive (n : Nat) : n = n := rfl

lake-workspace-load-failed: unavailable: package directory not found: <example>/./missing

  ⋯ 7 unchanged lines
     "inherited": false,
     "dir":
     "<regula>",
-    "configFile": "lakefile.lean"},
-   {"type": "path",
-    "name": "unavailable",
-    "manifestFile": "lake-manifest.json",
-    "inherited": false,
-    "dir": "./missing",
     "configFile": "lakefile.lean"}],
   "name": "regula",
   "lakeDir": ".lake",
   "fixedToolchain": false}

  ⋯ 3 unchanged lines
    leanOptions := #[⟨`autoImplicit, false⟩, ⟨`relaxedAutoImplicit, false⟩, ⟨`linter.missingDocs, true⟩]
  require regula from "<regula>"
  @[default_target] lean_lib Example
- 
- require unavailable from "./missing"

The examples are the qualification runner's requests for the same Example.lean. The correction removes a Lake dependency that cannot be resolved (the violating workspace adds require unavailable from "./missing"); the Lean source is unchanged.

Checked by a fresh single-file audit of <example>/Example.lean (axiomGate --file, claim kernel-only, execution checked): violating run incomplete, corrected run completed.

How to fix it🔗

1. Read the original setup error in the diagnostic detail and fix it: a missing path dependency, an unresolvable Git revision, or a toolchain that does not match lean-toolchain.

2. Provision pinned dependencies (for example lake exe cache get for Mathlib) before auditing; provisioning is setup, not verification.

3. Rerun the audit; a new run produces new, complete evidence.

Why it matters🔗

Every conformance claim is about one exact elaboration environment: toolchain, dependency revisions and source state. A result under an unknown or different environment is not evidence for the declared one.

What triggers it🔗

Setup checks load the Lake workspace, resolve dependencies to exact source states, and establish the compiler assumptions the audit needs. A failure (for example lake-workspace-load-failed when a required package directory is missing) is reported with impact incomplete.

RG2001 is also the finding for any other error that escapes the audit before a more specific rule classifies it (for example a malformed Lake query result). Read the detail: it names the failing step. Such an error is INCOMPLETE, never a pass.

A checker worker that loads a built environment for inspection and fails (for example an import conflict, or Lean's maximum recursion depth) is RG2001 too: the detail names the environment it was inspecting and carries the worker's own error text, and the result lists the stages that completed before it.

What a passing result establishes🔗

A passing result was produced in the declared environment: Lake loaded the workspace with the exact toolchain and resolved dependency state the result reports. An unavailable or unidentified environment is incomplete and never accepted.

It does not establish:

• That a dependency checkout matches its recorded revision's content: dependency acquisition is a trusted mechanism.

• Anything about the source; no declaration was inspected.

It leaves these review obligations open: R-QUALIFY.

Configuration and exceptions🔗

There is no configuration that turns an incomplete setup into a pass.

Limitations and unsupported cases🔗

This page's example is a diagnostic demonstration: the violating run is INCOMPLETE by design and is not accepted negative evidence. Its corrected counterpart passed a completed positive check.

Sources🔗

Normative clauses

standard §7.1 Declare the Elaboration Environment

Checklist rows

DECL-01, DECL-04

Detector, policy and proof sources

lean/Regula/Checker/Workspace.lean, lean/Regula/Checker/Lake.lean, lean/Regula/Checker/ResultProtocol.lean

Proved linkage

None. Setup failures and escaped audit errors reach this rule by their error message prefix, failing closed to INCOMPLETE; that classification is not proved.