feat: public imports for environment linters inside of lake lint in module system mode

src/lake/Lake/CLI/BuiltinLint.lean

@@ -65,7 +65,14 @@ public def run (args : Args) : IO UInt32 := do
   let mut anyFailed := false
   for mod in mods do
     unsafe Lean.enableInitializersExecution
-    let env ← importModules #[{ module := mod }, envLinterModule] {} (trustLevel := 1024) (loadExts := true)
+    -- Peek at the .olean header to learn whether `mod` participates in the module system.
+    -- If so, import at the public (`exported`) level, mirroring `processHeaderCore`.
+    let modFile ← findOLean mod
+    let (modData, region) ← readModuleData modFile
+    let level := if modData.isModule then OLeanLevel.exported else OLeanLevel.private
+    unsafe region.free
+    let env ← importModules #[{ module := mod }, envLinterModule] {}
+      (trustLevel := 1024) (loadExts := true) (level := level)
 
     let textEntries := collectTextLints env args mod.getRoot
     let textFailed := !textEntries.isEmpty

tests/lake/tests/builtin-lint-module/Clean.lean

@@ -0,0 +1,6 @@
+module
+
+-- No linter violations here.
+public theorem correctTheorem : 1 = 1 := rfl
+
+public def correctDef : Nat := 42

tests/lake/tests/builtin-lint-module/Linters.lean

@@ -0,0 +1,18 @@
+module
+
+public import Lean.Linter.EnvLinter
+public import Lean.Elab.Command
+
+open Lean Meta Lean.Linter Lean.Elab.Command
+
+/-- Dummy env linter for the `lake lint --builtin-lint` module-system test.
+Default scope (no `extra`), and the test reads only the declaration name so
+it does not depend on whether bodies are exposed at the `.exported` import
+level. Flags any declaration whose name ends with the marker suffix. -/
+@[builtin_env_linter] public meta def dummyEnvLinter : EnvLinter.EnvLinter where
+  noErrorsFound := "No dummy linter violations found."
+  errorsFound := "DUMMY LINTER VIOLATIONS:"
+  test declName := do
+    if declName.toString.endsWith "DummyMarker" then
+      return some "name ends with 'DummyMarker'"
+    return none

tests/lake/tests/builtin-lint-module/Main.lean

@@ -0,0 +1,28 @@
+module
+
+public import Linters
+
+-- Public def whose name ends with the dummy linter's marker suffix. The
+-- dummy env linter (registered in `Linters.lean`, default-on) reads only
+-- the declaration name, so it does not depend on bodies being exposed at
+-- the `.exported` import level. This proves env linters still see imported
+-- public decls after the level switch.
+public def shouldBeFlaggedDummyMarker : Nat := 1
+
+-- Public def with an unused let. `linter.unusedVariables` (default-on)
+-- fires during the build, the warning is captured in `lintLogExt`, and
+-- `lake lint` re-emits it. `lintLogExt` writes uniform OLean entries, so
+-- this must survive loading at `.exported`.
+public def publicUnusedVarFixture : Nat :=
+  let publicUnusedLet := 5
+  3
+
+-- Private def with an unused let. Private declarations are elided from
+-- `env.constants` at the `.exported` import level, so env linters cannot
+-- see them. The text-linter warning is fundamentally different: it fires
+-- at elaboration time and is stored in `lintLogExt` keyed by module
+-- index, not by declaration. The entry therefore survives the level
+-- change and must still be replayed by `lake lint`.
+private def privateUnusedVarFixture : Nat :=
+  let privateUnusedLet := 7
+  3

tests/lake/tests/builtin-lint-module/clean.sh

@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+rm -rf .lake
+rm -f lake-manifest.json produced.out

tests/lake/tests/builtin-lint-module/lakefile.toml

@@ -0,0 +1,11 @@
+name = "lint-module"
+defaultTargets = ["Main", "Clean", "Linters"]
+
+[[lean_lib]]
+name = "Main"
+
+[[lean_lib]]
+name = "Clean"
+
+[[lean_lib]]
+name = "Linters"

tests/lake/tests/builtin-lint-module/lean-toolchain

@@ -0,0 +1 @@
+../../../../../build/release/stage1

tests/lake/tests/builtin-lint-module/test.sh

@@ -0,0 +1,33 @@
+#!/usr/bin/env bash
+source ../common.sh
+
+# Verifies `lake lint --builtin-lint` on module-system targets. The top-level
+# module is loaded at `OLeanLevel.exported` (the "public" level), and we want
+# both env-linter and text-linter (lintLogExt) results to be preserved.
+#
+# Uses a dummy env linter defined in `Linters.lean` so this test does not
+# couple to the behaviour of any production env linter (`defLemma`,
+# `checkUnivs`, ...).
+
+./clean.sh
+
+# Clean module-system file: builtin lint must succeed.
+test_run lint --builtin-only Clean
+
+lake_out lint --builtin-only Main || true
+
+# Dummy env linter (default-on, name-only test) flags the public def. This
+# proves env linters still see imported public decls at `.exported`.
+match_pat 'shouldBeFlaggedDummyMarker' produced.out
+match_pat "name ends with 'DummyMarker'" produced.out
+
+# `linter.unusedVariables` (default-on) entries land in `lintLogExt` during
+# the build. `lintLogExt` writes uniform OLean entries, so its data must
+# survive loading at `.exported`. The warning on a *public* def is replayed:
+match_pat 'Variable name `publicUnusedLet` is not explicitly referenced' produced.out
+
+# And — crucially — the warning on a *private* def is also replayed: even
+# though private decls are elided from `env.constants` at `.exported`, the
+# `lintLogExt` entry is keyed by module index, not by declaration, so the
+# text-linter warning survives the level change.
+match_pat 'Variable name `privateUnusedLet` is not explicitly referenced' produced.out