Merge remote-tracking branch 'origin/main' into bump/v4.15.0

Batteries/Tactic/OpenPrivate.lean

@@ -99,7 +99,7 @@ name component.
 It is also possible to specify the module instead with
 `open private a b c from Other.Module`.
 -/
-syntax (name := openPrivate) "open private" (ppSpace ident)*
+syntax (name := openPrivate) "open" ppSpace "private" (ppSpace ident)*
   (" in" (ppSpace ident)*)? (" from" (ppSpace ident)*)? : command
 
 /-- Elaborator for `open private`. -/
@@ -119,7 +119,7 @@ It will also open the newly created alias definition under the provided short na
 It is also possible to specify the module instead with
 `export private a b c from Other.Module`.
 -/
-syntax (name := exportPrivate) "export private" (ppSpace ident)*
+syntax (name := exportPrivate) "export" ppSpace "private" (ppSpace ident)*
   (" in" (ppSpace ident)*)? (" from" (ppSpace ident)*)? : command
 
 /-- Elaborator for `export private`. -/

BatteriesTest/OpenPrivateDefs.lean

@@ -0,0 +1,4 @@
+/-!
+This file contains a private declaration. It's tested in `openPrivate.lean`.
+-/
+private def secretNumber : Nat := 2

BatteriesTest/openPrivate.lean

@@ -0,0 +1,37 @@
+
+import Batteries.Tactic.OpenPrivate
+
+import BatteriesTest.OpenPrivateDefs
+
+
+
+/-- error: unknown identifier 'secretNumber' -/
+#guard_msgs in
+#eval secretNumber
+
+
+-- It works with one space between the tokens
+/-- info: 2 -/
+#guard_msgs in
+open private secretNumber from BatteriesTest.OpenPrivateDefs in
+#eval secretNumber
+
+
+-- It also works with other kinds of whitespace between the tokens
+
+/-- info: 2 -/
+#guard_msgs in
+open      private secretNumber from BatteriesTest.OpenPrivateDefs in
+#eval secretNumber
+
+
+/-- info: 2 -/
+#guard_msgs in
+open
+  private secretNumber from BatteriesTest.OpenPrivateDefs in
+#eval secretNumber
+
+/-- info: 2 -/
+#guard_msgs in
+open /- Being sneaky! -/ private secretNumber from BatteriesTest.OpenPrivateDefs in
+#eval secretNumber

scripts/runLinter.lean

@@ -104,30 +104,31 @@ unsafe def runLinterOnModule (update : Bool) (module : Name): IO Unit := do
     readJsonFile NoLints nolintsFile
   else
     pure #[]
-  withImportModules #[module, lintModule] {} (trustLevel := 1024) fun env =>
-    let ctx := { fileName := "", fileMap := default }
-    let state := { env }
-    Prod.fst <$> (CoreM.toIO · ctx state) do
-      let decls ← getDeclsInPackage module.getRoot
-      let linters ← getChecks (slow := true) (runAlways := none) (runOnly := none)
-      let results ← lintCore decls linters
-      if update then
-        writeJsonFile (α := NoLints) nolintsFile <|
-          .qsort (lt := fun (a, b) (c, d) => a.lt c || (a == c && b.lt d)) <|
-          .flatten <| results.map fun (linter, decls) =>
-          decls.fold (fun res decl _ => res.push (linter.name, decl)) #[]
-      let results := results.map fun (linter, decls) =>
-        .mk linter <| nolints.foldl (init := decls) fun decls (linter', decl') =>
-          if linter.name == linter' then decls.erase decl' else decls
-      let failed := results.any (!·.2.isEmpty)
-      if failed then
-        let fmtResults ←
-          formatLinterResults results decls (groupByFilename := true) (useErrorFormat := true)
-            s!"in {module}" (runSlowLinters := true) .medium linters.size
-        IO.print (← fmtResults.toString)
-        IO.Process.exit 1
-      else
-        IO.println "-- Linting passed for {module}."
+  unsafe Lean.enableInitializersExecution
+  let env ← importModules #[module, lintModule] {} (trustLevel := 1024)
+  let ctx := { fileName := "", fileMap := default }
+  let state := { env }
+  Prod.fst <$> (CoreM.toIO · ctx state) do
+    let decls ← getDeclsInPackage module.getRoot
+    let linters ← getChecks (slow := true) (runAlways := none) (runOnly := none)
+    let results ← lintCore decls linters
+    if update then
+      writeJsonFile (α := NoLints) nolintsFile <|
+        .qsort (lt := fun (a, b) (c, d) => a.lt c || (a == c && b.lt d)) <|
+        .flatten <| results.map fun (linter, decls) =>
+        decls.fold (fun res decl _ => res.push (linter.name, decl)) #[]
+    let results := results.map fun (linter, decls) =>
+      .mk linter <| nolints.foldl (init := decls) fun decls (linter', decl') =>
+        if linter.name == linter' then decls.erase decl' else decls
+    let failed := results.any (!·.2.isEmpty)
+    if failed then
+      let fmtResults ←
+        formatLinterResults results decls (groupByFilename := true) (useErrorFormat := true)
+          s!"in {module}" (runSlowLinters := true) .medium linters.size
+      IO.print (← fmtResults.toString)
+      IO.Process.exit 1
+    else
+      IO.println s!"-- Linting passed for {module}."
 
 /--
 Usage: `runLinter [--update] [Batteries.Data.Nat.Basic]`
@@ -149,4 +150,3 @@ unsafe def main (args : List String) : IO Unit := do
   let modulesToLint ← determineModulesToLint specifiedModule
 
   modulesToLint.forM <| runLinterOnModule update
-