Merge main into nightly-testing

scripts/runLinter.lean

@@ -1,6 +1,7 @@
 import Lean.Util.SearchPath
 import Batteries.Tactic.Lint
 import Batteries.Data.Array.Basic
+import Lake.CLI.Main
 
 open Lean Core Elab Command Batteries.Tactic.Lint
 open System (FilePath)
@@ -17,26 +18,65 @@ def readJsonFile (α) [FromJson α] (path : System.FilePath) : IO α := do
 def writeJsonFile [ToJson α] (path : System.FilePath) (a : α) : IO Unit :=
   IO.FS.writeFile path <| toJson a |>.pretty.push '\n'
 
+open Lake
+
+/-- Returns the root modules of `lean_exe` or `lean_lib` default targets in the Lake workspace. -/
+def resolveDefaultRootModules : IO (Array Name) := do
+  -- load the Lake workspace
+  let (elanInstall?, leanInstall?, lakeInstall?) ← findInstall?
+  let config ← MonadError.runEIO <| mkLoadConfig { elanInstall?, leanInstall?, lakeInstall? }
+  let some workspace ← loadWorkspace config |>.toBaseIO
+    | throw <| IO.userError "failed to load Lake workspace"
+
+  -- resolve the default build specs from the Lake workspace (based on `lake build`)
+  let defaultBuildSpecs ← match resolveDefaultPackageTarget workspace workspace.root with
+    | Except.error e => IO.eprintln s!"Error getting default package target: {e}" *> IO.Process.exit 1
+    | Except.ok targets => pure targets
+
+  -- build an array of all root modules of `lean_exe` and `lean_lib` build targets
+  let defaultTargetModules := defaultBuildSpecs.flatMap <|
+    fun target => match target.info with
+      | BuildInfo.libraryFacet lib _ => lib.roots
+      | BuildInfo.leanExe exe => #[exe.config.root]
+      | _ => #[]
+  return defaultTargetModules
+
 /--
-Usage: `runLinter [--update] [Batteries.Data.Nat.Basic]`
+Parse args list for `runLinter`
+and return a pair of the update and specified module arguments.
 
-Runs the linters on all declarations in the given module (or `Batteries` by default).
-If `--update` is set, the `nolints` file is updated to remove any declarations that no longer need
-to be nolinted.
--/
-unsafe def main (args : List String) : IO Unit := do
-  let (update, args) :=
+Throws an exception if unable to parse the arguments.
+Returns `none` for the specified module if no module is specified.-/
+def parseLinterArgs (args: List String) : Except String (Bool × Option Name) :=
+  let (update, moreArgs) :=
     match args with
     | "--update" :: args => (true, args)
     | _ => (false, args)
-  let some module :=
-      match args with
-      | [] => some `Batteries
-      | [mod] => match mod.toName with
-        | .anonymous => none
-        | name => some name
-      | _ => none
-    | IO.eprintln "Usage: runLinter [--update] [Batteries.Data.Nat.Basic]" *> IO.Process.exit 1
+  match moreArgs with
+    | [] => Except.ok (update, none)
+    | [mod] => match mod.toName with
+      | .anonymous => Except.error "cannot convert module to Name"
+      | name => Except.ok (update, some name)
+    | _ => Except.error "cannot parse arguments"
+
+/--
+Return an array of the modules to lint.
+
+If `specifiedModule` is not `none` return an array containing only `specifiedModule`.
+Otherwise, resolve the default root modules from the Lake workspace. -/
+def determineModulesToLint (specifiedModule : Option Name) : IO (Array Name) := do
+  match specifiedModule with
+  | some module =>
+    println!"Running linter on specified module: {module}"
+    return #[module]
+  | none =>
+    println!"Automatically detecting modules to lint"
+    let defaultModules ← resolveDefaultRootModules
+    println!"Default modules: {defaultModules}"
+    return defaultModules
+
+/-- Run the Batteries linter on a given module and update the linter if `update` is `true`. -/
+unsafe def runLinterOnModule (update : Bool) (module : Name): IO Unit := do
   initSearchPath (← findSysroot)
   let mFile ← findOLean module
   unless (← mFile.pathExists) do
@@ -87,4 +127,26 @@ unsafe def main (args : List String) : IO Unit := do
         IO.print (← fmtResults.toString)
         IO.Process.exit 1
       else
-        IO.println "-- Linting passed."
+        IO.println "-- Linting passed for {module}."
+
+/--
+Usage: `runLinter [--update] [Batteries.Data.Nat.Basic]`
+
+Runs the linters on all declarations in the given module
+(or all root modules of Lake `lean_lib` and `lean_exe` default targets if no module is specified).
+If `--update` is set, the `nolints` file is updated to remove any declarations that no longer need
+to be nolinted.
+-/
+unsafe def main (args : List String) : IO Unit := do
+  let linterArgs := parseLinterArgs args
+  let (update, specifiedModule) ← match linterArgs with
+    | Except.ok args => pure args
+    | Except.error msg => do
+      IO.eprintln s!"Error parsing args: {msg}"
+      IO.eprintln "Usage: runLinter [--update] [Batteries.Data.Nat.Basic]"
+      IO.Process.exit 1
+
+  let modulesToLint ← determineModulesToLint specifiedModule
+
+  modulesToLint.forM <| runLinterOnModule update
+