feat(scripts): @[expose] removal-candidate report pipeline (draft)

.gitignore

@@ -8,3 +8,5 @@
 **/__pycache__/
 # Progress file from scripts/rm_set_option.py
 scripts/.rm_set_option_progress.jsonl
+# Output directory for `lake exe no_expose`
+scripts/.no_expose/

lakefile.lean

@@ -127,6 +127,25 @@ lean_exe «check_title_labels» where
 lean_exe «nightly-testing-checklist» where
   srcDir := "scripts"
 
+/-- Implementation modules for the `no_expose` exe (see below). Kept as a
+lib so multiple files under `scripts/NoExpose/` can `import` each other.
+The lib deliberately does NOT pull in Mathlib. -/
+lean_lib NoExpose where
+  srcDir := "scripts"
+  globs := #[`NoExpose.+]
+
+/-- `lake exe no_expose` is the user-facing tool for analysing and
+removing unnecessary `@[expose]` attributes in Mathlib (and downstream
+Mathlib-using projects). Subcommands:
+  * `collect` — build with diagnostics, scan env, produce report data
+  * `report`  — render per-file recommendations (no build)
+  * `edit`    — apply removals (with safety checks + audit trail)
+The exe deliberately does NOT `import Mathlib` so that it builds in
+seconds; it loads Mathlib at runtime via `Lean.withImportModules`. -/
+lean_exe no_expose where
+  srcDir := "scripts"
+  supportInterpreter := true
+
 lean_exe mathlib_test_executable where
   root := `MathlibTest.MathlibTestExecutable
 

scripts/NoExpose/Cli.lean

@@ -0,0 +1,124 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+/-!
+# `NoExpose.Cli` — argument parsing for `lake exe no_expose`
+
+Subcommands: `collect`, `report`, `edit`, plus `clean` for removing the
+data directory.
+-/
+
+namespace NoExpose
+
+/-- Format option for `report` output. -/
+inductive ReportFormat where
+  | text
+  | json
+  deriving Repr, BEq
+
+structure CollectArgs where
+  skipBuild : Bool := false
+  /-- Extra files to insert `set_option diagnostics false` into. -/
+  patchFiles : Array String := #[]
+
+structure ReportArgs where
+  paths : Array String := #[]
+  format : ReportFormat := .text
+
+structure EditArgs where
+  paths : Array String := #[]
+  dryRun : Bool := false
+  verify : Bool := false
+  forceDirty : Bool := false
+  forceStale : Bool := false
+
+inductive Subcommand where
+  | help
+  | collect (args : CollectArgs)
+  | report  (args : ReportArgs)
+  | edit    (args : EditArgs)
+  | clean
+
+/-- Top-level help text. -/
+def helpText : String := "\
+USAGE:
+  lake exe no_expose <subcommand> [args...]
+
+SUBCOMMANDS:
+  collect [--skip-build] [--patch-file FILE]...
+      Build Mathlib with `set_option diagnostics true`, walk the env,
+      and write report data to scripts/.no_expose/.
+
+  report [PATH...] [--format text|json]
+      Render per-file recommendations from existing report data.
+      With no PATH, renders every file in the report. Default
+      `--format text` lists `safe-to-unexpose` and
+      `needed-downstream` decls in each file.
+
+  edit [PATH...] [--dry-run] [--verify] [--force-dirty] [--force-stale]
+      Apply (default) or preview (--dry-run) the un-expose edits to
+      each PATH. Refuses on dirty git tree or stale report unless the
+      corresponding --force-* flag is given. With --verify, runs
+      `lake build` on the touched lib after applying.
+
+  clean
+      Remove scripts/.no_expose/ entirely.
+
+  help, --help, -h
+      Show this message.
+"
+
+private def parseFormat : String → Except String ReportFormat
+  | "text" => .ok .text
+  | "json" => .ok .json
+  | s      => .error s!"unknown --format value: {s} (expected text|json)"
+
+/-- Parse a `collect` argument list. -/
+private partial def parseCollect (rest : List String) : Except String CollectArgs := loop rest {} where
+  loop : List String → CollectArgs → Except String CollectArgs
+    | [], acc => .ok acc
+    | "--skip-build" :: rest, acc => loop rest { acc with skipBuild := true }
+    | "--patch-file" :: f :: rest, acc =>
+      loop rest { acc with patchFiles := acc.patchFiles.push f }
+    | flag :: _, _ => .error s!"collect: unknown argument {flag}"
+
+/-- Parse a `report` argument list. -/
+private partial def parseReport (rest : List String) : Except String ReportArgs := loop rest {} where
+  loop : List String → ReportArgs → Except String ReportArgs
+    | [], acc => .ok acc
+    | "--format" :: v :: rest, acc => do
+      let f ← parseFormat v
+      loop rest { acc with format := f }
+    | arg :: rest, acc =>
+      if arg.startsWith "--" then .error s!"report: unknown flag {arg}"
+      else loop rest { acc with paths := acc.paths.push arg }
+
+/-- Parse an `edit` argument list. -/
+private partial def parseEdit (rest : List String) : Except String EditArgs := loop rest {} where
+  loop : List String → EditArgs → Except String EditArgs
+    | [], acc => .ok acc
+    | "--dry-run" :: rest, acc => loop rest { acc with dryRun := true }
+    | "--verify" :: rest, acc => loop rest { acc with verify := true }
+    | "--force-dirty" :: rest, acc => loop rest { acc with forceDirty := true }
+    | "--force-stale" :: rest, acc => loop rest { acc with forceStale := true }
+    | arg :: rest, acc =>
+      if arg.startsWith "--" then .error s!"edit: unknown flag {arg}"
+      else loop rest { acc with paths := acc.paths.push arg }
+
+/-- Top-level dispatch. -/
+def parseArgs : List String → Except String Subcommand
+  | []                       => .ok .help
+  | "help" :: _              => .ok .help
+  | "--help" :: _            => .ok .help
+  | "-h" :: _                => .ok .help
+  | "collect" :: rest        => .collect <$> parseCollect rest
+  | "report"  :: rest        => .report  <$> parseReport rest
+  | "edit"    :: rest        => .edit    <$> parseEdit rest
+  | "clean" :: []            => .ok .clean
+  | "clean" :: rest          => .error s!"clean: unexpected arguments: {String.intercalate " " rest}"
+  | sub :: _                 => .error s!"unknown subcommand: {sub} (try `--help`)"
+
+end NoExpose

scripts/NoExpose/Collect.lean

@@ -0,0 +1,89 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+import NoExpose.Cli
+import NoExpose.Diagnostics
+import NoExpose.Env
+import NoExpose.Paths
+import NoExpose.Report
+import NoExpose.Restore
+
+/-!
+# `NoExpose.Collect` — orchestrator for the `collect` subcommand
+
+Owns the high-level sequence:
+1. `NoExpose.Diagnostics`: patch lakefile, run `lake build`, parse log
+   into `diagnostics.jsonl`. Skipped under `--skip-build`.
+2. `NoExpose.Env`: open env via `withImportModules`; emit
+   `exposed.jsonl`, `static_refs.jsonl`, `decl_refs.jsonl`.
+3. `NoExpose.Report.build`: join everything into `report.jsonl`.
+-/
+
+open Lean
+
+namespace NoExpose
+
+/-- Run the env-scan portion of `collect`: opens the env once via
+`withImportModules`, gathers static/decl refs, returns enumerated
+candidates; then post-scans source files and writes `exposed.jsonl`. -/
+unsafe def runEnvScan (_project : ProjectInfo) (modules : Array Name)
+    (scopePrefix : Array Name) : IO Unit := do
+  IO.FS.createDirAll dataDir
+  let searchPath ← addSearchPathFromEnv (← getBuiltinSearchPath (← findSysroot))
+  -- All env-dependent work happens inside `withImportModules`. The
+  -- `DeclRecord` fields are stringified (and `Name` references dropped)
+  -- before any iteration of the records, so the data is safe to write
+  -- without lifetime worries.
+  withImportModules modules
+      (searchPath := searchPath) (trustLevel := 1024) do
+    let env ← getEnv
+    -- Static refs → static_refs.jsonl
+    let refs ← collectStaticRefs
+    IO.FS.withFile staticRefsPath .write fun h => writeStaticRefs env refs h
+    IO.eprintln s!"[no_expose collect] wrote {refs.size} static-refs pairs to {staticRefsPath}"
+    -- Per-decl refs → decl_refs.jsonl
+    IO.FS.withFile declRefsPath .write fun h => writeDeclRefs env h
+    IO.eprintln s!"[no_expose collect] wrote per-decl refs to {declRefsPath}"
+    -- Source-driven enumeration: walk source for `@[expose]`,
+    -- intersect with env decl ranges.
+    let recs ← enumerate scopePrefix
+    IO.FS.withFile exposedPath .write fun h => do
+      for r in recs do h.putStrLn r.toJsonLine
+    IO.eprintln s!"[no_expose collect] wrote {recs.size} exposed records to {exposedPath}"
+
+/-- Run the `collect` subcommand. -/
+unsafe def runCollect (args : CollectArgs) : IO UInt32 := do
+  -- On every startup, restore any orphaned backups left by an
+  -- interrupted previous run. (No-op if state.json is absent.)
+  detectOrphan
+  let project ← detectProjectInfo
+  IO.eprintln s!"[no_expose collect] project: {project.name} \
+    (libs: {project.libRoots})"
+  -- Step 1: full build with diagnostics, unless skipped.
+  unless args.skipBuild do
+    if project.name.toString != "mathlib" then
+      IO.eprintln s!"no_expose collect: full-build mode is Mathlib-only \
+        (detected project: {project.name}); pass --skip-build."
+      return 1
+    let extraOff : Array System.FilePath := args.patchFiles.map .mk
+    let rc ← runDiagnostics project.lakefilePath extraOff
+    if rc != 0 then
+      IO.eprintln s!"[no_expose collect] lake build returned {rc}; \
+        diagnostics.jsonl reflects the partial log. Continuing with env scan."
+  -- Step 2: env scan.
+  -- For Mathlib, the canonical target is just `Mathlib` (the union module).
+  -- For downstream projects, pick the first lib root.
+  let modules : Array Name :=
+    if project.libRoots.contains `Mathlib then #[`Mathlib]
+    else project.libRoots.take 1
+  let scopePrefix : Array Name :=
+    if project.libRoots.contains `Mathlib then #[`Mathlib]
+    else project.libRoots
+  runEnvScan project modules scopePrefix
+  -- Step 3: join.
+  build exposedPath diagnosticsPath staticRefsPath declRefsPath reportPath
+  return 0
+
+end NoExpose