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..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 :=
@@ -52,22 +60,27 @@ 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
+/--
+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 mods do
+  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}:"
@@ -97,4 +110,117 @@ public def run (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 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
+  let scope := args.scope
+  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 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 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 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
+
+    -- 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
+        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
+          IO.print (← fmtResults.toString)
+      return anyMod
+
+    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
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 :=
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
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