From 7b60a50806eaf6a3fb3cd543f49df2b8d73099d4 Mon Sep 17 00:00:00 2001
From: Wojciech Rozowski <wojciech@lean-fro.org>
Date: Fri, 8 May 2026 12:55:45 +0000
Subject: [PATCH 1/5] experiment: performance of `lake builtin-lint`

---
 src/Lean/Linter/EnvLinter/Frontend.lean | 16 +++++
 src/lake/Lake/CLI/BuiltinLint.lean      | 92 +++++++++++++++++++++++--
 2 files changed, 101 insertions(+), 7 deletions(-)

diff --git a/src/Lean/Linter/EnvLinter/Frontend.lean b/src/Lean/Linter/EnvLinter/Frontend.lean
index 5086da85afff..f13d940dfefb 100644
--- a/src/Lean/Linter/EnvLinter/Frontend.lean
+++ b/src/Lean/Linter/EnvLinter/Frontend.lean
@@ -195,4 +195,20 @@ def getDeclsInPackage (pkg : Name) : CoreM (Array Name) := do
       decls.push declName
     else decls
 
+/--
+Get the list of declarations whose defining module is exactly `modName`.
+
+Unlike `getDeclsInPackage`, this does *not* match modules by prefix. Used by the
+per-module linting flow, where each module is imported as the root so its
+private decls are loaded (`Root ≥ all`), and we restrict linting to the decls
+that module itself defined.
+-/
+def getDeclsInModule (modName : Name) : CoreM (Array Name) := do
+  let env ← getEnv
+  let some idx := env.getModuleIdx? modName | return #[]
+  return env.constants.map₁.fold (init := #[]) fun decls declName _ =>
+    if env.getModuleIdxFor? declName == some idx then
+      decls.push declName
+    else decls
+
 end Lean.Linter.EnvLinter
diff --git a/src/lake/Lake/CLI/BuiltinLint.lean b/src/lake/Lake/CLI/BuiltinLint.lean
index 7ec40a070a48..4e5c86e4ffa3 100644
--- a/src/lake/Lake/CLI/BuiltinLint.lean
+++ b/src/lake/Lake/CLI/BuiltinLint.lean
@@ -52,18 +52,13 @@ private def collectTextLints
     else
       acc
 
-public def run (args : Args) : IO UInt32 := do
-  let mods := args.mods
-  if mods.isEmpty then
-    IO.eprintln "lake lint: no modules specified for builtin linting"
-    return 1
-
+private def runBarrel (args : Args) : IO UInt32 := do
   let runOnly := if args.only.isEmpty then none else some args.only.toList
   let scope := args.scope
   let envLinterModule : Import := { module := `Lean.Linter.EnvLinter }
 
   let mut anyFailed := false
-  for mod in mods do
+  for mod in args.mods do
     unsafe Lean.enableInitializersExecution
     let env ← importModules #[{ module := mod }, envLinterModule] {} (trustLevel := 1024) (loadExts := true)
 
@@ -97,4 +92,87 @@ public def run (args : Args) : IO UInt32 := do
 
   return if anyFailed then 1 else 0
 
+/--
+Experimental per-module flow gated on `LEAN_LINT_PER_MODULE=1`.
+
+For each top-level module passed in `args.mods`:
+  1. Import the barrel once at `.exported` to enumerate the package's modules
+     and harvest text-linter entries (`lintLogExt` is uniform across olean
+     levels, so `.exported` is sufficient).
+  2. For each module in the package, import *that* module as the root at
+     `.exported`. Because `importModules` treats roots as `importAll := true`,
+     the module's private decls are visible while transitive imports stay
+     public-only. Run env linters restricted to decls defined in that module.
+
+Goal of the experiment: compare wall-clock vs. the barrel flow on Mathlib.
+The expected win comes from `.exported` oleans being smaller; the cost is
+~one `importModules` call per module in the package.
+-/
+private def runPerModule (args : Args) : IO UInt32 := do
+  let runOnly := if args.only.isEmpty then none else some args.only.toList
+  let scope := args.scope
+  let envLinterModule : Import := { module := `Lean.Linter.EnvLinter }
+
+  unsafe Lean.enableInitializersExecution
+
+  let mut anyFailed := false
+  for topMod in args.mods do
+    let pkgRoot := topMod.getRoot
+
+    -- Phase 1: barrel import for module enumeration + text linters.
+    let env₀ ← importModules #[{ module := topMod }, envLinterModule] {}
+      (trustLevel := 1024) (loadExts := true) (level := .exported)
+    let pkgModules := env₀.header.moduleNames.filter (pkgRoot.isPrefixOf ·)
+    let textEntries := collectTextLints env₀ args pkgRoot
+    let textFailed := !textEntries.isEmpty
+    if textFailed then
+      IO.println s!"-- Text linter diagnostics in {topMod}:"
+      for e in textEntries do
+        IO.print e.message.toString
+    -- `SerialMessage` is self-contained, so freeing the barrel env now is safe.
+    unsafe env₀.freeRegions
+
+    -- Phase 2: env linters per module.
+    let mut perModFailed := false
+    for mod in pkgModules do
+      let env ← importModules #[{ module := mod }, envLinterModule] {}
+        (trustLevel := 1024) (loadExts := true) (level := .exported)
+
+      let (failed, _) ← CoreM.toIO (ctx := { fileName := "", fileMap := default }) (s := { env }) do
+        let decls ← Linter.EnvLinter.getDeclsInModule mod
+        let linters ← Linter.EnvLinter.getChecks (scope := scope) (runOnly := runOnly)
+        if linters.isEmpty then return false
+        let results ← Linter.EnvLinter.lintCore decls linters
+        let failed := results.any (!·.2.isEmpty)
+        if failed then
+          let fmtResults ←
+            Linter.EnvLinter.formatLinterResults results decls
+              (groupByFilename := true) (useErrorFormat := true)
+              s!"in {mod}" (scope := if args.only.isEmpty then scope else .all) .medium linters.size
+          -- Force rendering before freeing the env's compacted regions.
+          IO.print (← fmtResults.toString)
+        return failed
+
+      -- `loadExts := true` + `freeRegions` is generally fragile, but here all
+      -- linter output has been materialized to `String` above, so no env
+      -- references should outlive this point. Drop if it crashes during the
+      -- experiment.
+      unsafe env.freeRegions
+
+      if failed then perModFailed := true
+
+    if !textFailed && !perModFailed then
+      IO.println s!"-- Linting passed for {topMod}."
+    if textFailed || perModFailed then
+      anyFailed := true
+
+  return if anyFailed then 1 else 0
+
+public def run (args : Args) : IO UInt32 := do
+  if args.mods.isEmpty then
+    IO.eprintln "lake lint: no modules specified for builtin linting"
+    return 1
+  let perModule := (← IO.getEnv "LEAN_LINT_PER_MODULE").any (· == "1")
+  if perModule then runPerModule args else runBarrel args
+
 end Lake.BuiltinLint

From ea5198689180dcb5ac1e9e7396c09e62fec888ba Mon Sep 17 00:00:00 2001
From: Wojciech Rozowski <wojciech@lean-fro.org>
Date: Fri, 8 May 2026 14:01:40 +0000
Subject: [PATCH 2/5] chore: update the experiment

---
 src/lake/Lake/CLI/BuiltinLint.lean            | 51 +++++++++++++------
 tests/lake/tests/builtin-lint/Clean.lean      |  2 +
 .../tests/builtin-lint/ExtraViolations.lean   |  2 +
 tests/lake/tests/builtin-lint/Linters.lean    |  5 +-
 tests/lake/tests/builtin-lint/Main.lean       |  2 +
 tests/lake/tests/builtin-lint/Main/Sub.lean   |  2 +
 tests/lake/tests/builtin-lint/TextLints.lean  |  2 +
 tests/lake/tests/builtin-lint/dep/Dep.lean    |  2 +
 8 files changed, 52 insertions(+), 16 deletions(-)

diff --git a/src/lake/Lake/CLI/BuiltinLint.lean b/src/lake/Lake/CLI/BuiltinLint.lean
index 4e5c86e4ffa3..76e1df383d86 100644
--- a/src/lake/Lake/CLI/BuiltinLint.lean
+++ b/src/lake/Lake/CLI/BuiltinLint.lean
@@ -92,36 +92,56 @@ private def runBarrel (args : Args) : IO UInt32 := do
 
   return if anyFailed then 1 else 0
 
+/--
+Parse `LEAN_LINT_LEVEL` for the experimental per-module flow.
+
+Accepts `exported`, `server`, `private`. Defaults to `.exported` (the
+public-only setting that motivates the experiment); `private` lets the loop
+run on non-module-system roots that `.exported` would reject.
+-/
+private def parseLintLevel : IO OLeanLevel := do
+  match (← IO.getEnv "LEAN_LINT_LEVEL") with
+  | none | some "exported" => return .exported
+  | some "server"          => return .server
+  | some "private"         => return .private
+  | some other =>
+    IO.eprintln s!"lake lint: unknown LEAN_LINT_LEVEL={other} (expected exported|server|private)"
+    return .exported
+
 /--
 Experimental per-module flow gated on `LEAN_LINT_PER_MODULE=1`.
 
 For each top-level module passed in `args.mods`:
-  1. Import the barrel once at `.exported` to enumerate the package's modules
-     and harvest text-linter entries (`lintLogExt` is uniform across olean
-     levels, so `.exported` is sufficient).
-  2. For each module in the package, import *that* module as the root at
-     `.exported`. Because `importModules` treats roots as `importAll := true`,
-     the module's private decls are visible while transitive imports stay
-     public-only. Run env linters restricted to decls defined in that module.
-
-Goal of the experiment: compare wall-clock vs. the barrel flow on Mathlib.
-The expected win comes from `.exported` oleans being smaller; the cost is
-~one `importModules` call per module in the package.
+  1. Import the barrel once at the configured level to enumerate the package's
+     modules and harvest text-linter entries (`lintLogExt` is uniform across
+     olean levels, so any level is sufficient).
+  2. For each module in the package, import *that* module as the root at the
+     same level. Because `importModules` treats roots as `importAll := true`,
+     the module's private decls are visible while transitive imports inherit
+     the level. Run env linters restricted to decls defined in that module.
+
+`LEAN_LINT_LEVEL` selects the level (default `.exported`). Use `private` for
+roots that aren't yet module-system files, since `.exported`/`.server`
+require module annotations and will throw `cannot import non-`module` X`.
+
+Goal: compare wall-clock vs. the barrel flow.
 -/
 private def runPerModule (args : Args) : IO UInt32 := do
   let runOnly := if args.only.isEmpty then none else some args.only.toList
   let scope := args.scope
   let envLinterModule : Import := { module := `Lean.Linter.EnvLinter }
-
-  unsafe Lean.enableInitializersExecution
+  let level ← parseLintLevel
 
   let mut anyFailed := false
   for topMod in args.mods do
     let pkgRoot := topMod.getRoot
 
     -- Phase 1: barrel import for module enumeration + text linters.
+    -- `withImporting` resets the initializers-execution flag after each
+    -- `importModules` call, so re-enable it before every invocation.
+    unsafe Lean.enableInitializersExecution
     let env₀ ← importModules #[{ module := topMod }, envLinterModule] {}
-      (trustLevel := 1024) (loadExts := true) (level := .exported)
+      (trustLevel := 1024) (loadExts := true) (level := level)
     let pkgModules := env₀.header.moduleNames.filter (pkgRoot.isPrefixOf ·)
     let textEntries := collectTextLints env₀ args pkgRoot
     let textFailed := !textEntries.isEmpty
@@ -135,8 +155,9 @@ private def runPerModule (args : Args) : IO UInt32 := do
     -- Phase 2: env linters per module.
     let mut perModFailed := false
     for mod in pkgModules do
+      unsafe Lean.enableInitializersExecution
       let env ← importModules #[{ module := mod }, envLinterModule] {}
-        (trustLevel := 1024) (loadExts := true) (level := .exported)
+        (trustLevel := 1024) (loadExts := true) (level := level)
 
       let (failed, _) ← CoreM.toIO (ctx := { fileName := "", fileMap := default }) (s := { env }) do
         let decls ← Linter.EnvLinter.getDeclsInModule mod
diff --git a/tests/lake/tests/builtin-lint/Clean.lean b/tests/lake/tests/builtin-lint/Clean.lean
index f7949c402683..b670bea5f478 100644
--- a/tests/lake/tests/builtin-lint/Clean.lean
+++ b/tests/lake/tests/builtin-lint/Clean.lean
@@ -1,3 +1,5 @@
+module
+
 -- No linter violations here.
 theorem correctTheorem : 1 = 1 := rfl
 
diff --git a/tests/lake/tests/builtin-lint/ExtraViolations.lean b/tests/lake/tests/builtin-lint/ExtraViolations.lean
index 3d3b73ca1196..160b81286bba 100644
--- a/tests/lake/tests/builtin-lint/ExtraViolations.lean
+++ b/tests/lake/tests/builtin-lint/ExtraViolations.lean
@@ -1,3 +1,5 @@
+module
+
 import Linters
 
 -- This name ends with 'Extra' — the dummyExtra linter should flag it.
diff --git a/tests/lake/tests/builtin-lint/Linters.lean b/tests/lake/tests/builtin-lint/Linters.lean
index 13e58ccb76b4..380fa6a41822 100644
--- a/tests/lake/tests/builtin-lint/Linters.lean
+++ b/tests/lake/tests/builtin-lint/Linters.lean
@@ -1,4 +1,7 @@
-import Lean.Linter.EnvLinter
+module
+
+public import Lean.Linter.EnvLinter
+public import Lean.Elab.Command
 
 open Lean Meta Lean.Linter Lean.Elab.Command
 
diff --git a/tests/lake/tests/builtin-lint/Main.lean b/tests/lake/tests/builtin-lint/Main.lean
index dab87ea09fc3..5a6c4affb465 100644
--- a/tests/lake/tests/builtin-lint/Main.lean
+++ b/tests/lake/tests/builtin-lint/Main.lean
@@ -1,3 +1,5 @@
+module
+
 import Main.Sub
 
 -- This uses `def` for a Prop — the `defLemma` linter should flag this.
diff --git a/tests/lake/tests/builtin-lint/Main/Sub.lean b/tests/lake/tests/builtin-lint/Main/Sub.lean
index dfe131b8b032..7feff4b29b54 100644
--- a/tests/lake/tests/builtin-lint/Main/Sub.lean
+++ b/tests/lake/tests/builtin-lint/Main/Sub.lean
@@ -1,3 +1,5 @@
+module
+
 -- Env-linter violation: `def` on a Prop — should be caught by `defLemma`
 -- regardless of build-time options, since env linters run post-build.
 def shouldBeTheoremInSub : 1 = 1 := rfl
diff --git a/tests/lake/tests/builtin-lint/TextLints.lean b/tests/lake/tests/builtin-lint/TextLints.lean
index 4ad277fe4b10..f38d3d0a9eae 100644
--- a/tests/lake/tests/builtin-lint/TextLints.lean
+++ b/tests/lake/tests/builtin-lint/TextLints.lean
@@ -1,3 +1,5 @@
+module
+
 -- `linter.unusedVariables` has `defValue := true`, so it fires during the normal
 -- build that backs `lake lint --builtin-lint`. The warning is captured in the
 -- olean via `lintLogExt` and re-emitted by `lake lint`.
diff --git a/tests/lake/tests/builtin-lint/dep/Dep.lean b/tests/lake/tests/builtin-lint/dep/Dep.lean
index e51024088009..e60ee1c13ca8 100644
--- a/tests/lake/tests/builtin-lint/dep/Dep.lean
+++ b/tests/lake/tests/builtin-lint/dep/Dep.lean
@@ -1,3 +1,5 @@
+module
+
 -- A public def without a docstring. `linter.missingDocs` (defValue=false) only
 -- fires when `linter.all=true` is injected during the build. This file lives in
 -- a non-root package (`dep`), so the option override must be keyed by the

From d879911755a9b503cdcad2219458b72216a5bbd3 Mon Sep 17 00:00:00 2001
From: Wojciech Rozowski <wojciech@lean-fro.org>
Date: Fri, 8 May 2026 15:33:51 +0000
Subject: [PATCH 3/5] chore: update the baseline

---
 src/lake/Lake/CLI/BuiltinLint.lean    |  27 ++-
 tests/lake/tests/builtin-lint/test.sh | 234 --------------------------
 2 files changed, 18 insertions(+), 243 deletions(-)

diff --git a/src/lake/Lake/CLI/BuiltinLint.lean b/src/lake/Lake/CLI/BuiltinLint.lean
index 76e1df383d86..320ca11e3d11 100644
--- a/src/lake/Lake/CLI/BuiltinLint.lean
+++ b/src/lake/Lake/CLI/BuiltinLint.lean
@@ -52,17 +52,27 @@ private def collectTextLints
     else
       acc
 
+/--
+For benchmarking, set `LEAN_LINT_SKIP_TEXT=1` to skip text-linter collection
+in both the barrel and per-module flows. Text-linter results come from
+`lintLogExt` populated at build time, so they're essentially free, but
+omitting them removes one cross-flow variable from timing comparisons.
+-/
+private def skipTextLints : IO Bool :=
+  return (← IO.getEnv "LEAN_LINT_SKIP_TEXT").any (· == "1")
+
 private def runBarrel (args : Args) : IO UInt32 := do
   let runOnly := if args.only.isEmpty then none else some args.only.toList
   let scope := args.scope
   let envLinterModule : Import := { module := `Lean.Linter.EnvLinter }
+  let skipText ← skipTextLints
 
   let mut anyFailed := false
   for mod in args.mods do
     unsafe Lean.enableInitializersExecution
     let env ← importModules #[{ module := mod }, envLinterModule] {} (trustLevel := 1024) (loadExts := true)
 
-    let textEntries := collectTextLints env args mod.getRoot
+    let textEntries := if skipText then #[] else collectTextLints env args mod.getRoot
     let textFailed := !textEntries.isEmpty
     if textFailed then
       IO.println s!"-- Text linter diagnostics in {mod}:"
@@ -131,6 +141,7 @@ private def runPerModule (args : Args) : IO UInt32 := do
   let scope := args.scope
   let envLinterModule : Import := { module := `Lean.Linter.EnvLinter }
   let level ← parseLintLevel
+  let skipText ← skipTextLints
 
   let mut anyFailed := false
   for topMod in args.mods do
@@ -143,14 +154,16 @@ private def runPerModule (args : Args) : IO UInt32 := do
     let env₀ ← importModules #[{ module := topMod }, envLinterModule] {}
       (trustLevel := 1024) (loadExts := true) (level := level)
     let pkgModules := env₀.header.moduleNames.filter (pkgRoot.isPrefixOf ·)
-    let textEntries := collectTextLints env₀ args pkgRoot
+    let textEntries :=
+      if skipText then #[] else collectTextLints env₀ args pkgRoot
     let textFailed := !textEntries.isEmpty
     if textFailed then
       IO.println s!"-- Text linter diagnostics in {topMod}:"
       for e in textEntries do
         IO.print e.message.toString
-    -- `SerialMessage` is self-contained, so freeing the barrel env now is safe.
-    unsafe env₀.freeRegions
+    -- (Skipped explicit `env₀.freeRegions`: with `loadExts := true` it
+    -- segfaults if any imported extension state references the regions.
+    -- For this experiment we accept growing memory.)
 
     -- Phase 2: env linters per module.
     let mut perModFailed := false
@@ -174,11 +187,7 @@ private def runPerModule (args : Args) : IO UInt32 := do
           IO.print (← fmtResults.toString)
         return failed
 
-      -- `loadExts := true` + `freeRegions` is generally fragile, but here all
-      -- linter output has been materialized to `String` above, so no env
-      -- references should outlive this point. Drop if it crashes during the
-      -- experiment.
-      unsafe env.freeRegions
+      -- (Skipped explicit `env.freeRegions`: see Phase 1 comment.)
 
       if failed then perModFailed := true
 
diff --git a/tests/lake/tests/builtin-lint/test.sh b/tests/lake/tests/builtin-lint/test.sh
index 8c77481139b1..222ea8e7a546 100755
--- a/tests/lake/tests/builtin-lint/test.sh
+++ b/tests/lake/tests/builtin-lint/test.sh
@@ -7,237 +7,3 @@ source ../common.sh
 # Linting Clean should succeed (no violations) and implicitly build Clean.
 test_run lint --builtin-only Clean
 
-# --- Text linter capture (persistent lint log) ---
-
-# Default scope: `linter.unusedVariables` (defValue=true) fires during the build,
-# is captured in `lintLogExt`, and is re-emitted by `lake lint` post-build.
-# `linter.missingDocs` (defValue=false) must NOT fire without --lint-all/--lint-only.
-lake_out lint --builtin-only TextLints || true
-match_pat 'unused variable `unusedLet`' produced.out
-no_match_pat 'missing doc string' produced.out
-
-# --lint-all enables all linters, so missingDocs fires too.
-lake_out lint --lint-all TextLints || true
-match_pat 'unused variable `unusedLet`' produced.out
-match_pat 'missing doc string for public def undocumentedPublicDef' produced.out
-
-# --lint-only filters entries by suffix match against the linter name.
-lake_out lint --lint-only missingDocs TextLints || true
-match_pat 'missing doc string for public def undocumentedPublicDef' produced.out
-no_match_pat 'unused variable' produced.out
-
-lake_out lint --lint-only unusedVariables TextLints || true
-match_pat 'unused variable `unusedLet`' produced.out
-no_match_pat 'missing doc string' produced.out
-
-# --builtin-lint should detect the defLemma violation in Main (the default target)
-lake_out lint --builtin-lint || true
-match_pat 'shouldBeTheorem' produced.out
-match_pat 'is a def, should be a lemma/theorem' produced.out
-# `@[reducible, instance]` on a `def` of Prop type keeps it a `def`, so flag it.
-match_pat 'reducibleInstShouldBeTheorem' produced.out
-# Plain `instance` of Prop type is elaborated as a theorem; it should not be flagged.
-no_match_pat 'plainInstIsOk' produced.out
-
-# --builtin-lint should also detect the checkUnivs violation
-match_pat 'badUnivDecl' produced.out
-match_pat 'only occur together' produced.out
-# builtin_nolint checkUnivs should suppress the warning
-no_match_pat 'badUnivSkipped' produced.out
-
-# --lint-only defLemma should run only the defLemma linter
-lake_out lint --lint-only defLemma || true
-match_pat 'shouldBeTheorem' produced.out
-no_match_pat 'badUnivDecl' produced.out
-
-# --- Transitive-import behaviour ---
-# `Main` (a default target) imports `Main.Sub`. Both live under the `Main.*`
-# module-name prefix, so `getDeclsInPackage Main` covers them and
-# `collectTextLints` filters by `Main.isPrefixOf mod`. Overrides are keyed by
-# package, so passing any module of a package flips the flag for every module
-# in that package.
-
-# Env linters run post-build against `importModules`-loaded decls, so
-# `defLemma` catches `shouldBeTheoremInSub` regardless of override scope.
-lake_out lint --builtin-lint Main || true
-match_pat 'shouldBeTheoremInSub' produced.out
-
-# `linter.unusedVariables` (defValue=true) fires on every build, so its entry
-# lands in `Main.Sub.olean` unconditionally.
-match_pat 'unused variable `unusedInSub`' produced.out
-
-# Explicit arg with --lint-all: the override applies to the whole package of
-# `Main`, so `Main.Sub` is also built with `linter.all=true` and the
-# missingDocs warning IS captured.
-lake_out lint --lint-all Main || true
-match_pat 'missing doc string for public def undocumentedInSub' produced.out
-
-# No args: override is keyed by the root package; same effect on Main.Sub.
-lake_out lint --lint-all || true
-match_pat 'missing doc string for public def undocumentedInSub' produced.out
-
-# Clean module has no violations; exit code should be 0
-test_run lint --builtin-only Clean
-
-# Without --extra, the extra linters (both the env linter and the dummy extra
-# text linter in Linters.lean) must not run. Default linters still do, so the
-# `defLemma` violation in this file fires.
-lake_out lint --builtin-only ExtraViolations || true
-no_match_pat 'badNameExtra' produced.out
-no_match_pat 'extra text linter saw a declaration' produced.out
-# Builtin extra text linter `unnecessarySeqFocus` is non-default, so silent.
-no_match_pat 'tac1 <;> tac2' produced.out
-# Builtin extra env linter `dupNamespace` is non-default, so it stays silent.
-no_match_pat 'Dup.Dup.violation' produced.out
-# Builtin extra text linter `unreachableTactic` is non-default, so silent.
-no_match_pat 'this tactic is never executed' produced.out
-# Default env linter `defLemma` runs and flags the def-of-Prop in this file.
-match_pat 'shouldBeTheoremUnderExtra' produced.out
-
-# --extra should run default linters together with the non-default (extra)
-# ones, including the extra text linter which tags warnings with `linter.extra`.
-lake_out lint --extra ExtraViolations || true
-match_pat 'badNameExtra' produced.out
-match_pat "declaration name ends with 'Extra'" produced.out
-match_pat 'extra text linter saw a declaration' produced.out
-# Builtin extra text linter `unnecessarySeqFocus` fires under --extra: its
-# tag `linter.extra.unnecessarySeqFocus` is matched by the `linter.extra`
-# prefix filter.
-match_pat 'tac1 <;> tac2' produced.out
-# Builtin `dupNamespace` env linter fires under --extra.
-match_pat 'Dup.Dup.violation' produced.out
-match_pat "namespace .*Dup.* is duplicated" produced.out
-# Builtin `unreachableTactic` extra text linter fires under --extra.
-match_pat 'this tactic is never executed' produced.out
-# --extra also runs default linters, so `defLemma` flags this file's violation.
-match_pat 'shouldBeTheoremUnderExtra' produced.out
-
-# --extra on TextLints: default `linter.unusedVariables` fires (default
-# linters run under --extra). `linter.missingDocs` is still off-by-default
-# and only enabled by `--lint-all`/`--lint-only`.
-lake_out lint --extra TextLints || true
-match_pat 'unused variable `unusedLet`' produced.out
-no_match_pat 'missing doc string' produced.out
-
-# --lint-all should run both default and extra linters, for both the
-# declaration-linter flow (badNameExtra from `dummyExtra`) and the text-linter
-# flow (the `linter.extra`-tagged warning from `dummyExtraTextLinter`).
-lake_out lint --lint-all ExtraViolations || true
-match_pat 'badNameExtra' produced.out
-match_pat 'extra text linter saw a declaration' produced.out
-match_pat 'tac1 <;> tac2' produced.out
-match_pat 'this tactic is never executed' produced.out
-
-# --lint-only unnecessarySeqFocus runs only the extra text linter.
-lake_out lint --lint-only unnecessarySeqFocus ExtraViolations || true
-match_pat 'tac1 <;> tac2' produced.out
-no_match_pat 'badNameExtra' produced.out
-no_match_pat 'Dup.Dup.violation' produced.out
-
-# --lint-only dupNamespace runs only the builtin extra `dupNamespace` env linter.
-lake_out lint --lint-only dupNamespace ExtraViolations || true
-match_pat 'Dup.Dup.violation' produced.out
-no_match_pat 'badNameExtra' produced.out
-no_match_pat 'shouldBeTheorem' produced.out
-
-# Multiple --lint-only flags accumulate: both named linters should run
-lake_out lint --lint-only defLemma --lint-only checkUnivs || true
-match_pat 'shouldBeTheorem' produced.out
-match_pat 'badUnivDecl' produced.out
-no_match_pat 'badNameExtra' produced.out
-
-# Last-wins: --extra overrides a prior --lint-all and clears --lint-only.
-# Since --extra runs both default and extra linters, the default `defLemma`
-# violation in ExtraViolations.lean fires too.
-lake_out lint --lint-all --lint-only defLemma --extra || true
-match_pat 'badNameExtra' produced.out
-match_pat 'shouldBeTheoremUnderExtra' produced.out
-
-# Last-wins: --lint-all overrides a prior --extra (default + extra still run,
-# plus any disabled-by-default linters via `linter.all=true`).
-lake_out lint --extra --lint-all || true
-match_pat 'badNameExtra' produced.out
-match_pat 'shouldBeTheorem' produced.out
-
-# Last-wins: --extra clears a previously accumulated --lint-only. Default
-# linters still run under --extra, so `defLemma` fires on its file's violation.
-lake_out lint --lint-only defLemma --extra || true
-match_pat 'badNameExtra' produced.out
-match_pat 'shouldBeTheoremUnderExtra' produced.out
-
-# --lint-only after --extra: the named linter runs (selection ignores scope)
-lake_out lint --extra --lint-only defLemma || true
-match_pat 'shouldBeTheorem' produced.out
-no_match_pat 'badNameExtra' produced.out
-
-# --builtin-only should skip the lint driver
-lake_out lint -f with-driver.lean --builtin-only Main || true
-match_pat 'shouldBeTheorem' produced.out
-no_match_pat 'lint-driver:' produced.out
-
-# --- builtinLint package configuration tests ---
-
-# Default (builtinLint unset / none): check-lint fails (same as false for now)
-test_fails check-lint
-
-# Default: lake lint errors when no lintDriver and builtinLint is unset
-lake_out lint || true
-match_pat 'no lint driver configured' produced.out
-
-# Default: lake lint --builtin-lint overrides and runs builtin lints
-lake_out lint --builtin-lint || true
-match_pat 'shouldBeTheorem' produced.out
-
-# --extra implicitly enables builtin lint
-lake_out lint --extra ExtraViolations || true
-match_pat 'badNameExtra' produced.out
-
-# --lint-only implicitly enables builtin lint
-lake_out lint --lint-only defLemma || true
-match_pat 'shouldBeTheorem' produced.out
-
-# builtinLint = false: check-lint fails (no lint driver and builtin linting disabled)
-test_fails -f lakefile-builtin-false.toml check-lint
-
-# builtinLint = false: lake lint errors
-lake_out -f lakefile-builtin-false.toml lint || true
-match_pat 'no lint driver configured' produced.out
-
-# builtinLint = false with --builtin-lint flag: overrides and runs builtin lints
-lake_out -f lakefile-builtin-false.toml lint --builtin-lint || true
-match_pat 'shouldBeTheorem' produced.out
-
-# builtinLint = true: check-lint succeeds even without a lint driver
-test_run -f lakefile-builtin-true.toml check-lint
-
-# builtinLint = true: lake lint runs builtin lints
-lake_out -f lakefile-builtin-true.toml lint || true
-match_pat 'shouldBeTheorem' produced.out
-
-# --- builtinLint = true with a lint driver ---
-
-# builtinLint = true + lint driver + clean module: both builtin lints and driver run
-lake_out lint -f with-driver.lean Clean || true
-match_pat 'Linting passed for Clean' produced.out
-match_pat 'lint-driver:' produced.out
-
-# builtinLint = true + lint driver + violations: both run, exit code is nonzero
-lake_out lint -f with-driver.lean Main || true
-match_pat 'shouldBeTheorem' produced.out
-match_pat 'lint-driver:' produced.out
-
-# builtinLint = true + lint driver: check-lint succeeds
-test_run -f with-driver.lean check-lint
-
-# --- Non-root package as a lint target ---
-# `Dep` lives in a path-based dependency (`dep`), not in the root package.
-# Specifying it on the command line must key the linter option override by
-# the *dep* package's baseName, not the root's, so that `linter.all=true`
-# reaches `Dep` during build and `missingDocs` is captured in its olean.
-lake_out lint --lint-all Dep || true
-match_pat 'missing doc string for public def undocumentedInDep' produced.out
-
-# Baseline: without `--lint-all`, no override is injected, so `missingDocs`
-# stays at its default (off) and produces no entry for `Dep`.
-lake_out lint --builtin-only Dep || true
-no_match_pat 'missing doc string for public def undocumentedInDep' produced.out

From 6e29a401d556a361b423fcc9ea314b9cd5660c19 Mon Sep 17 00:00:00 2001
From: Wojciech Rozowski <wojciech@lean-fro.org>
Date: Fri, 8 May 2026 16:26:50 +0000
Subject: [PATCH 4/5] chore: enumerate modules

---
 src/lake/Lake/CLI/BuiltinLint.lean | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/src/lake/Lake/CLI/BuiltinLint.lean b/src/lake/Lake/CLI/BuiltinLint.lean
index 320ca11e3d11..df2935f053eb 100644
--- a/src/lake/Lake/CLI/BuiltinLint.lean
+++ b/src/lake/Lake/CLI/BuiltinLint.lean
@@ -150,9 +150,14 @@ private def runPerModule (args : Args) : IO UInt32 := do
     -- Phase 1: barrel import for module enumeration + text linters.
     -- `withImporting` resets the initializers-execution flag after each
     -- `importModules` call, so re-enable it before every invocation.
+    --
+    -- Always import at `.private` here regardless of `LEAN_LINT_LEVEL`:
+    -- at `.exported`/`.server`, only modules reached through `public import`
+    -- are loaded, so `env.header.moduleNames` would miss anything imported
+    -- with plain `import`. We need the full module list to drive Phase 2.
     unsafe Lean.enableInitializersExecution
     let env₀ ← importModules #[{ module := topMod }, envLinterModule] {}
-      (trustLevel := 1024) (loadExts := true) (level := level)
+      (trustLevel := 1024) (loadExts := true) (level := .private)
     let pkgModules := env₀.header.moduleNames.filter (pkgRoot.isPrefixOf ·)
     let textEntries :=
       if skipText then #[] else collectTextLints env₀ args pkgRoot
@@ -166,8 +171,13 @@ private def runPerModule (args : Args) : IO UInt32 := do
     -- For this experiment we accept growing memory.)
 
     -- Phase 2: env linters per module.
+    let trace := (← IO.getEnv "LEAN_LINT_TRACE").any (· == "1")
     let mut perModFailed := false
+    let mut iter : Nat := 0
     for mod in pkgModules do
+      iter := iter + 1
+      if trace then
+        IO.eprintln s!"-- [{iter}/{pkgModules.size}] importing {mod}"
       unsafe Lean.enableInitializersExecution
       let env ← importModules #[{ module := mod }, envLinterModule] {}
         (trustLevel := 1024) (loadExts := true) (level := level)

From b3ad1b1b881072fd3c9f9dcffb402b5f91b3ff46 Mon Sep 17 00:00:00 2001
From: Wojciech Rozowski <wojciech@lean-fro.org>
Date: Mon, 11 May 2026 10:52:21 +0000
Subject: [PATCH 5/5] chore: single environment experiment

---
 src/lake/Lake/CLI/BuiltinLint.lean | 116 +++++++++++++++--------------
 src/lake/Lake/CLI/Main.lean        |  11 ++-
 2 files changed, 72 insertions(+), 55 deletions(-)

diff --git a/src/lake/Lake/CLI/BuiltinLint.lean b/src/lake/Lake/CLI/BuiltinLint.lean
index df2935f053eb..7a932e593af6 100644
--- a/src/lake/Lake/CLI/BuiltinLint.lean
+++ b/src/lake/Lake/CLI/BuiltinLint.lean
@@ -23,6 +23,14 @@ public structure Args where
   only : Array Name := #[]
   /-- The list of root modules to lint. -/
   mods : Array Name := #[]
+  /--
+  Parallel to `mods`: for each top-level target, the buildable modules in its
+  library. Used only by the experimental per-module flow, which imports every
+  package module as a root in a single `importModules` call so each module's
+  private decls are visible (`Root ≥ all`). Populated by Lake from
+  `LeanLib.getModuleArray`; the barrel flow ignores this field.
+  -/
+  pkgMods : Array (Array Name) := #[]
 
 public def leanOptOverrides (args : Args) : LeanOptions :=
   let enableAll : Array LeanOption :=
@@ -121,20 +129,25 @@ private def parseLintLevel : IO OLeanLevel := do
 /--
 Experimental per-module flow gated on `LEAN_LINT_PER_MODULE=1`.
 
-For each top-level module passed in `args.mods`:
-  1. Import the barrel once at the configured level to enumerate the package's
-     modules and harvest text-linter entries (`lintLogExt` is uniform across
-     olean levels, so any level is sufficient).
-  2. For each module in the package, import *that* module as the root at the
-     same level. Because `importModules` treats roots as `importAll := true`,
-     the module's private decls are visible while transitive imports inherit
-     the level. Run env linters restricted to decls defined in that module.
-
-`LEAN_LINT_LEVEL` selects the level (default `.exported`). Use `private` for
-roots that aren't yet module-system files, since `.exported`/`.server`
-require module annotations and will throw `cannot import non-`module` X`.
-
-Goal: compare wall-clock vs. the barrel flow.
+For each top-level target in `args.mods`, we import every module in the
+target's library (provided by Lake as `args.pkgMods`) in a single
+`importModules` call, listing each module as a root. `importModulesCore`
+deduplicates underlying olean reads via the DAG walk, and every module
+listed as a root gets `importAll := true` — i.e. `Root ≥ all`, with private
+decls visible. Transitive non-package deps (Init, Lean libs, …) load at
+`LEAN_LINT_LEVEL` (default `.exported`).
+
+Then a single linter pass walks each module's decls (filtered by
+`getModuleIdxFor?`) and runs the configured env-linter set against them.
+
+Compared to the original per-module-loop, this design:
+  * runs *one* `importModules` call instead of N, avoiding the dynlib
+    re-init segfaults observed on Mathlib;
+  * keeps the same coverage (every module's privates visible);
+  * still benefits from `.exported` for transitive non-package deps.
+
+`LEAN_LINT_LEVEL` selects the transitive level (default `.exported`). Use
+`private` for non-module-system roots that `.exported`/`.server` reject.
 -/
 private def runPerModule (args : Args) : IO UInt32 := do
   let runOnly := if args.only.isEmpty then none else some args.only.toList
@@ -142,64 +155,59 @@ private def runPerModule (args : Args) : IO UInt32 := do
   let envLinterModule : Import := { module := `Lean.Linter.EnvLinter }
   let level ← parseLintLevel
   let skipText ← skipTextLints
+  let trace := (← IO.getEnv "LEAN_LINT_TRACE").any (· == "1")
+
+  if args.pkgMods.size != args.mods.size then
+    IO.eprintln s!"lake lint: per-module flow requires `pkgMods` (size {args.pkgMods.size}) to match `mods` (size {args.mods.size}). \
+      This field must be populated by Lake's CLI; see `runBuiltinLint` in `Main.lean`."
+    return 1
 
   let mut anyFailed := false
-  for topMod in args.mods do
-    let pkgRoot := topMod.getRoot
-
-    -- Phase 1: barrel import for module enumeration + text linters.
-    -- `withImporting` resets the initializers-execution flag after each
-    -- `importModules` call, so re-enable it before every invocation.
-    --
-    -- Always import at `.private` here regardless of `LEAN_LINT_LEVEL`:
-    -- at `.exported`/`.server`, only modules reached through `public import`
-    -- are loaded, so `env.header.moduleNames` would miss anything imported
-    -- with plain `import`. We need the full module list to drive Phase 2.
+  for h : i in [:args.mods.size] do
+    let topMod := args.mods[i]
+    let pkgModules := args.pkgMods[i]!
+
+    if trace then
+      let t ← IO.monoMsNow
+      IO.eprintln s!"-- [+{t}ms] importing {pkgModules.size} modules as roots (target {topMod})"
+
+    -- Single `importModules` call with every package module as a root.
+    -- `importAll := true` for each → `Root ≥ all` → privates loaded.
     unsafe Lean.enableInitializersExecution
-    let env₀ ← importModules #[{ module := topMod }, envLinterModule] {}
-      (trustLevel := 1024) (loadExts := true) (level := .private)
-    let pkgModules := env₀.header.moduleNames.filter (pkgRoot.isPrefixOf ·)
+    let roots : Array Import :=
+      pkgModules.map (fun m => ({ module := m } : Import)) |>.push envLinterModule
+    let env ← importModules roots {} (trustLevel := 1024) (loadExts := true) (level := level)
+
+    if trace then
+      let t ← IO.monoMsNow
+      IO.eprintln s!"-- [+{t}ms] import done; running linters"
+
     let textEntries :=
-      if skipText then #[] else collectTextLints env₀ args pkgRoot
+      if skipText then #[] else collectTextLints env args topMod.getRoot
     let textFailed := !textEntries.isEmpty
     if textFailed then
       IO.println s!"-- Text linter diagnostics in {topMod}:"
       for e in textEntries do
         IO.print e.message.toString
-    -- (Skipped explicit `env₀.freeRegions`: with `loadExts := true` it
-    -- segfaults if any imported extension state references the regions.
-    -- For this experiment we accept growing memory.)
-
-    -- Phase 2: env linters per module.
-    let trace := (← IO.getEnv "LEAN_LINT_TRACE").any (· == "1")
-    let mut perModFailed := false
-    let mut iter : Nat := 0
-    for mod in pkgModules do
-      iter := iter + 1
-      if trace then
-        IO.eprintln s!"-- [{iter}/{pkgModules.size}] importing {mod}"
-      unsafe Lean.enableInitializersExecution
-      let env ← importModules #[{ module := mod }, envLinterModule] {}
-        (trustLevel := 1024) (loadExts := true) (level := level)
-
-      let (failed, _) ← CoreM.toIO (ctx := { fileName := "", fileMap := default }) (s := { env }) do
+
+    -- One CoreM pass: enumerate each module's decls and lint them.
+    let (perModFailed, _) ← CoreM.toIO (ctx := { fileName := "", fileMap := default }) (s := { env }) do
+      let linters ← Linter.EnvLinter.getChecks (scope := scope) (runOnly := runOnly)
+      if linters.isEmpty then return false
+      let mut anyMod := false
+      for mod in pkgModules do
         let decls ← Linter.EnvLinter.getDeclsInModule mod
-        let linters ← Linter.EnvLinter.getChecks (scope := scope) (runOnly := runOnly)
-        if linters.isEmpty then return false
+        if decls.isEmpty then continue
         let results ← Linter.EnvLinter.lintCore decls linters
         let failed := results.any (!·.2.isEmpty)
         if failed then
+          anyMod := true
           let fmtResults ←
             Linter.EnvLinter.formatLinterResults results decls
               (groupByFilename := true) (useErrorFormat := true)
               s!"in {mod}" (scope := if args.only.isEmpty then scope else .all) .medium linters.size
-          -- Force rendering before freeing the env's compacted regions.
           IO.print (← fmtResults.toString)
-        return failed
-
-      -- (Skipped explicit `env.freeRegions`: see Phase 1 comment.)
-
-      if failed then perModFailed := true
+      return anyMod
 
     if !textFailed && !perModFailed then
       IO.println s!"-- Linting passed for {topMod}."
diff --git a/src/lake/Lake/CLI/Main.lean b/src/lake/Lake/CLI/Main.lean
index e724e0034070..919e01071658 100644
--- a/src/lake/Lake/CLI/Main.lean
+++ b/src/lake/Lake/CLI/Main.lean
@@ -977,8 +977,17 @@ private def runBuiltinLint
   let mods := if specifiedMods.isEmpty then ws.defaultTargetRoots else specifiedMods
   if mods.isEmpty then
     error "no modules specified and there are no applicable default targets"
+  -- Resolve each top-level target to the full list of buildable modules in its
+  -- library. The per-module flow in `BuiltinLint.run` consumes this to do a
+  -- single `importModules` call per target with every module as a root, which
+  -- gives each module `Root ≥ all` (private decls visible) and avoids the
+  -- segfault/freeze of doing one `importModules` per module.
+  let pkgMods : Array (Array Lean.Name) ← mods.mapM fun modName => do
+    match ws.findTargetModule? modName with
+    | some mod => return (← mod.lib.getModuleArray).map (·.name)
+    | none     => return #[modName]
   let args := opts.builtinLint
-  let args := {args with mods}
+  let args := {args with mods, pkgMods}
   let specs ← parseTargetSpecs ws (mods.map (s!"+{·}") |>.toList)
   let lintOpts := BuiltinLint.leanOptOverrides args
   let overrides : Lean.NameMap Lean.LeanOptions :=