Checked example🔗

{
  "schema-version": 2,
  "surfaces": [
    {
      "library": "Example",
      "claim": "standard-logical",
      "execution": "report",
      "rationale": "Exact fixture claim, with the executable whose root the library contains."
    }
  ],
  "excluded-libraries": [],
  "excluded-executables": [
    { "executable": "cli", "rationale": "Entry point left out of the claim." }
  ]
}

/-! # Reflexivity

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

manifest-conflict: excluded executable 'cli' root Example.Cli is a module of claimed library 'Example': a root keeps its library's claim, so list 'cli' in the executables of surface 'Example'

  ⋯ 2 unchanged lines
    "surfaces": [
      {
        "library": "Example",
-       "claim": "standard-logical",
-       "execution": "report",
-       "rationale": "Exact fixture claim, with the executable whose root the library contains."
-     }
-   ],
-   "excluded-libraries": [],
-   "excluded-executables": [
-     { "executable": "cli", "rationale": "Entry point left out of the claim." }
-   ]
+       "executables": ["cli"],
+       "claim": "standard-logical",
+       "execution": "report",
+       "rationale": "Exact fixture claim, with the executable whose root the library contains."
+     }
+   ],
+   "excluded-libraries": [],
+   "excluded-executables": []
  }

{
  "schema-version": 2,
  "surfaces": [
    {
      "library": "Example",
      "executables": ["cli"],
      "claim": "standard-logical",
      "execution": "report",
      "rationale": "Exact fixture claim, with the executable whose root the library contains."
    }
  ],
  "excluded-libraries": [],
  "excluded-executables": []
}

The examples are foundation_manifest.json files for one layout: library Example globs its submodules (globs := #[.andSubmodules `Example]), among them Example.Cli, the root of lean_exe cli. Excluding the executable conflicts with the claimed library that contains its root; the correction claims it with that library's surface instead, without changing the library, profile or execution requirement.

Checked by a fresh whole-project audit of <example> (axiomGate): violating run rejected, corrected run completed.

How to fix it🔗

1. Remove or correct unknown keys and invalid values; the diagnostic names them.

2. Add each root library and executable to surfaces or to the matching exclusion array, with a rationale.

3. An executable whose root module belongs to a library is classified with it: list it in the executables of that library's surface, where its root keeps the library's claim and is inspected in the executable's own environment with its import closure. Its root in an excluded library, or in the library of another surface, and an excluded executable whose root is in a claimed library, are manifest conflicts.

4. Run lake lint -- --explain-config to see the manifest, scope, profiles and stages the driver would use, without auditing.

Why it matters🔗

Coverage is only meaningful against a complete, exact classification. Silently ignoring an unknown key or an unclassified target would let modules escape the audit or let a typo change the claim.

What triggers it🔗

The checker parses the manifest and reconciles it with Lake's elaborated root package. Unknown keys, duplicates, a wrong schema version, an unknown execution value, an empty surfaces array, a missing rationale, an unclassified or unknown target, and an executable whose root module belongs to a library classified differently (claimed in another surface, or claimed where the library is excluded, or the reverse) are rejected (manifest-schema, manifest-incomplete, manifest-conflict and related subreasons). A claimed executable whose root belongs to its own surface's library is accepted unless every module of that library is such a root; the root is then inspected once, in the executable's environment.

In the editor, an invalid local request (for example an unknown regula.localFoundation value) is reported under this rule for the current file only.

What a passing result establishes🔗

The manifest has the exact schema and classifies every root-package library and executable exactly once, each executable alike with every library that contains its root module.

It does not establish:

• That the chosen claims and exclusions are appropriate for the project; that is reviewed with each rationale.

• Exclusions do not permit a claimed module to import an excluded one (RG2004).

It leaves these review obligations open: R-QUALIFY, R-INTENT, R-INVARIANT.

Configuration and exceptions🔗

The manifest is the configuration; there is no flag that accepts an invalid manifest, and the schema requires at least one nonempty library surface. --manifest PATH and --project DIR select which files are audited, not how strictly.

lake lint exits 2 (INVALID CONFIGURATION) when only this rule rejects.

Limitations and unsupported cases🔗

Executable-only packages are valid Lean projects but unsupported by manifest schema 2.

A claimed library needs a module besides its claimed executables' roots: its own environment would otherwise be empty, which the checker does not support.

The editor never guesses an omitted project scope.

Sources🔗

Normative clauses

standard §7.2 Define Surfaces Through Lake Semantics

Checklist rows

DECL-04, SCOPE-05, BUILD-04, DECL-01, BUILD-01

Detector, policy and proof sources

lean/Regula/Checker/Manifest.lean, lean/Regula/Checker/Lake.lean, lean/Regula/Checker/AxiomGate.lean, lean/RegulaPolicy/Plan.lean, lean/Regula/Findings.lean

Proved linkage

Regula.Checker.Manifest.parse_sound and parseValue_complete for the manifest (kernel-checked in the excluded Regula library) and Regula.Linter.checked_editorRequest for the editor's request. An executable root's classification is RegulaPolicy.RootsClassifiedAlike: AxiomGate.checkClassification decides it before the build of the project audit, lake lint and the build linter, and in doctor and --explain-config, and every accepted project claim decides it again in TargetPartitionOK; the nonempty-library check decides ClaimCandidate.Valid's condition over the executed surface assignment. Routing a failure to this rule by its manifest- prefix is not proved.