This page documents Regula 4.34.0. The latest release is Regula 0.11.1: this page in Regula 0.11.1.

RG2002: Configuration must classify the complete Lake surface🔗

Category Configuration
Scope project
Subreason configuration

The surface manifest (foundation_manifest.json, schema 2) is invalid or does not classify every root-package library and executable exactly once.

What to do. Fix the manifest: exactly the four top-level keys, one entry per root lean_lib and lean_exe (claimed or excluded with a rationale), and valid claim and execution values.

Requirement: foundation_manifest.json is valid schema 2 and classifies every root lean_lib and lean_exe exactly once.
Reported in: EditorProjectSingle file
Enforcement: Strict, like every rule: see how rules are enforced.

Checked example🔗

Violating input

✗ Rejectedfoundation_manifest.jsonsource examples/rules/RG2002/Violation.json

{
  "schema-version": 2,
  "surfaces": [
    {
      "library": "Example",
      "claim": "kernel-only",
      "execution": "checked",
      "rationale": "Exact fixture source claim."
    }
  ],
  "excluded-libraries": [],
  "excluded-executables": [],
  "unknown": true
}

Unchanged input

Example.leansource examples/rules/RG2002/Example.lean

/-! # Reflexivity

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

Findings of the violating run

RG2002 error violation fresh project

Subject <example> at project <example>

manifest-schema: top level has unknown key(s): ["unknown"]

Correction

Change to foundation_manifest.json

  ⋯ 8 unchanged lines
      }
    ],
    "excluded-libraries": [],
-   "excluded-executables": [],
-   "unknown": true
+   "excluded-executables": []
  }

✓ Passesfoundation_manifest.jsonsource examples/rules/RG2002/Fixed.json

{
  "schema-version": 2,
  "surfaces": [
    {
      "library": "Example",
      "claim": "kernel-only",
      "execution": "checked",
      "rationale": "Exact fixture source claim."
    }
  ],
  "excluded-libraries": [],
  "excluded-executables": []
}

The examples are foundation_manifest.json files. The correction removes the unknown manifest key without changing the selected source, profile or execution requirement.

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

How to fix it🔗

Remove or correct unknown keys and invalid values; the diagnostic names them.
Add each root library and executable to surfaces or to the matching exclusion array, with a rationale.
A claimed executable must be a standalone root such as Main; its root module cannot belong to a manifested library.
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 claimed/excluded conflicts are rejected (manifest-schema, manifest-incomplete and related subreasons).

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.

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.

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/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. Routing a failure to this rule by its manifest- prefix is not proved.