Checked example🔗

/-! # Identity

The identity function, with its type parameter declared. -/

/-- The identity function on any type `α`. -/
def identity {α : Type} (a : α) : α := a

community-configuration: `autoImplicit` is not set; set it to false; `relaxedAutoImplicit` is not set; set it to false; `linter.missingDocs` is not set; set it to true

  import Lake
  open Lake DSL
  
- package rule_examples
+ package rule_examples where
+   leanOptions := #[⟨`linter.missingDocs, true⟩, ⟨`autoImplicit, false⟩,
+     ⟨`relaxedAutoImplicit, false⟩]
  
  @[default_target]
  lean_lib Example
  ⋯ 2 unchanged lines

The examples are the package's lakefile.lean (the corpus run adds its require regula line). The correction adds the three options every claimed target sets, automatic implicits off and linter.missingDocs on, without changing the library or its source.

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

How to fix it🔗

1. Add ⟨`autoImplicit, false⟩, ⟨`relaxedAutoImplicit, false⟩, ⟨`linter.missingDocs, true⟩ to leanOptions (the same keys under [leanOptions] in lakefile.toml), then declare each universe and implicit the build reports as unknown and document each declaration it reports.

2. With Mathlib, also set weak.linter.mathlibStandardSet to true, weak.linter.hashCommand false, weak.linter.style.longFile 0 and weak.linter.style.header false, or true with weak.linter.style.header.license set to your license line.

3. Replace a target-wide ⟨`linter.X, false⟩ with set_option linter.X false in on the one declaration the community's guidance allows, with a comment (§6.2).

4. Delete each -D name=value in moreLeanArgs or weakLeanArgs that gives one of these options a value the rule does not admit or turns off another linter; other extra arguments may stay.

Why it matters🔗

An automatic implicit adds a binder the source does not show, so the elaborated statement can quantify over more than the text a reviewer compares with the intent. A linter reports only where it is on: without linter.missingDocs, or with a linter off for a whole target, the warning-free build (RG2003) never sees those warnings. A -D extra lean argument can override leanOptions, where the audit reads these options.

Standard §7.1 requires the options because they decide which binders a declaration's elaborated type has. Standard §6.7 adopts the community's linters as its conventions baseline, and a linter enforces its convention only where it is on: RG2003 rejects warnings, not a missing linter.

What triggers it🔗

After the claimed surfaces build, the checker reads Lake's resolved configuration of every claimed library and executable: its leanOptions (build type, package, then target, a later entry replacing an earlier one) and its weakLeanArgs and moreLeanArgs. The proved decision RegulaPolicy.Community.failures rejects the target, with applicability community-configuration, when autoImplicit or relaxedAutoImplicit is not set to false or linter.missingDocs is not set to true, when any other linter.… option than linter.style.header, linter.hashCommand and linter.style.longFile is set to false, or when a -D name=value among the extra arguments gives a required option a value the rule does not admit or sets such a linter to false.

A target of a surface whose loaded environments contain a Mathlib module must also set weak.linter.mathlibStandardSet to true, weak.linter.hashCommand to false and weak.linter.style.longFile to 0, and weak.linter.style.header to false, or to true when the target also gives weak.linter.style.header.license the license line Mathlib's header linter expects in leanOptions, with every value that leanOptions or any -D gives it a nonempty string; a -D alone does not configure the license line.

A key's leading weak. component is read as the option it sets; a target that gives one option under both spellings must give a value the rule admits under each. A string value counts as Lean parses it for the option: "false" is false and "0" is 0. One finding per target lists every failure.

Every -D that lean reads starts at the first D of an argument that begins with a single - (-D, or after flags as in -qD), with its value after the D or in the next argument; the rule reads every such candidate, so it can also reject one that lean does not read as a -D, such as the value of -o. Any other extra argument is allowed.

What a passing result establishes🔗

Every claimed library and executable is built through Lake with automatic implicits off and linter.missingDocs on, turns off no linter target-wide beyond the §6.7 exclusions and, in a Mathlib surface, enables the standard set with exactly those exclusions, or with the header linter on and its license line configured; no -D extra lean argument overrides these options.

It does not establish:

• That no module sets an option back in source, such as set_option autoImplicit true or a linter disable; review checks source options (§6.2).

• That the community linters' own checks pass, such as a docstring on every public declaration; their warnings are RG2003's.

• That extra lean arguments other than -D, such as --plugin or --setup, leave the options unchanged.

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

Configuration and exceptions🔗

The Lake configuration is the input; no manifest field, source option or command-line flag exempts a claimed target.

A Mathlib target that keeps the header linter on names its license line in leanOptions: ⟨`weak.linter.style.header, true⟩, ⟨`weak.linter.style.header.license, "Released under the MIT license as described in the repository LICENSE."⟩; a lakefile.toml gives both in the array form of leanOptions, since its [leanOptions] table cannot hold both keys. Without the license option the target must set the header linter to false.

Limitations and unsupported cases🔗

Options given on lake's own command line are not read; the rule reads what Lake resolves for the workspace the audit loads.

Whether a surface imports Mathlib is read from all of its loaded environments, so every claimed target of such a surface, including an executable whose own root does not import Mathlib, needs the Mathlib options.

The -D reading is assumed to cover the command-line parser of the Lean executable, as read from Lean's Lean.Shell source and its getopt handling; that correspondence is neither proved nor observed.

That Mathlib's header linter compares the second header line with linter.style.header.license is read from its source at the pinned release and assumed; the rule checks that the license option is configured, not that the modules' header lines match it.

The rule runs in project audits only; editor feedback does not read Lake configuration.

Sources🔗

Normative clauses

standard §7.1 Declare the Elaboration Environment, standard §6.7 Community Conventions and Linters, standard §6.2 Module Purpose and Linter Discipline

Checklist rows

DECL-01, DOC-01

Detector, policy and proof sources

lean/RegulaPolicy/Community.lean, lean/Regula/Checker/Lake.lean, lean/Regula/Checker/AxiomGate.lean, website/RegulaStandard/CodeOrganization.lean

Proved linkage

RegulaPolicy.Community.failures_eq_nil_iff, conforming_of_mathlib, conforming_missingDocs, conforming_header, header_on_unlicensed_fails, licensed_iff, licensed_header_passes, unlicensed_header_fails, leanArgument_mem_failures_iff and missingDocs_unset_fails. Reading Lake's target configuration is operational.