update

.github/workflows/build.yml

@@ -5,23 +5,13 @@ jobs:
   build:
     runs-on: ubuntu-latest
     steps:
-      - name: install elan
-        run: |
-          set -o pipefail
-          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
-          ./elan-init -y
-          echo "$HOME/.elan/bin" >> $GITHUB_PATH
       - uses: actions/checkout@v4
-      - name: print lean and lake versions
-        run: |
-          lean --version
-          lake --version
-      - run: lake build
+
+      - uses: leanprover/lean-action@v1-beta
+        with:
+          check-reservoir-eligibility: true
+      # use setup from lean-action to perform the following steps
       - name: verify `lake exe graph` works
         run: |
           lake exe graph
           rm import_graph.dot
-      - name: run tests
-        id: test
-        run: |
-          find test/*.lean -exec lake env lean {} \;

ImportGraph/Cli.lean

@@ -1,11 +1,11 @@
 /-
-Copyright (c) 2023 Scott Morrison. All rights reserved.
+Copyright (c) 2023 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 import Cli.Basic
-import Std.Lean.IO.Process
-import Std.Lean.Util.Path
+import Batteries.Lean.IO.Process
+import Batteries.Lean.Util.Path
 import ImportGraph.CurrentModule
 import ImportGraph.Imports
 import ImportGraph.Lean.Name

ImportGraph/Imports.lean

@@ -1,10 +1,10 @@
 /-
-Copyright (c) 2023 Scott Morrison. All rights reserved.
+Copyright (c) 2023 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 import Lean
-import Std.Lean.NameMap
+import Batteries.Lean.NameMap
 import ImportGraph.RequiredModules
 
 /-!

ImportGraph/Lean/Name.lean

@@ -5,19 +5,17 @@ Authors: Jon Eugster
 -/
 import Lean.Data.Name
 import Lean.CoreM
-import Std.Data.HashMap.Basic
-import Std.Lean.Name
-import Std.Lean.SMap
+import Batteries.Data.HashMap.Basic
+import Batteries.Lean.SMap
 import Lean.Meta.Match.MatcherInfo
 
 /-!
 TODO: Some declarations in this file are duplicated from mathlib, but especially `isBlacklisted`
-is deemed to specific for upstreaming to Std.
+is deemed to specific for upstreaming to Batteries.
 -/
 namespace Lean.Name
 
 open Lean Meta Elab
-open Std
 
 namespace ImportGraph
 
@@ -48,11 +46,11 @@ gathered together into a `HashMap` according to the module they are defined in.
 
 Note: copied from `Mathlib.Lean.Name`
 -/
-def allNamesByModule (p : Name → Bool) : CoreM (Std.HashMap Name (Array Name)) := do
-  (← getEnv).constants.foldM (init := Std.HashMap.empty) fun names n _ => do
+def allNamesByModule (p : Name → Bool) : CoreM (Batteries.HashMap Name (Array Name)) := do
+  (← getEnv).constants.foldM (init := Batteries.HashMap.empty) fun names n _ => do
     if p n && !(← isBlackListed n) then
       let some m ← findModuleOf? n | return names
-      -- TODO use `Std.HashMap.modify` when we bump Std4 (or `alter` if that is written).
+      -- TODO use `Batteries.HashMap.modify` when we bump `batteries` (or `alter` if that is written).
       match names.find? m with
       | some others => return names.insert m (others.push n)
       | none => return names.insert m #[n]

ImportGraph/RequiredModules.lean

@@ -1,7 +1,7 @@
 /-
-Copyright (c) 2023 Scott Morrison. All rights reserved.
+Copyright (c) 2023 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 import Lean
 

README.md

@@ -36,4 +36,8 @@ There are a few commands implemented, which help you analysing the imports of a
 
 ## Credits
 
-This code has been extracted from [mathlib](https://github.com/leanprover-community/mathlib4) and has mainly been written by Scott Morrison and a few other mathlib contributors.
+This code has been extracted from [mathlib](https://github.com/leanprover-community/mathlib4) and has mainly been written by Kim Morrison and a few other mathlib contributors.
+
+### Maintainers
+
+For issues, questions, or feature requests, please reach out to [Jon Eugster](https://leanprover.zulipchat.com/#narrow/dm/385895-Jon-Eugster).

lake-manifest.json

@@ -1,22 +1,22 @@
-{"version": 7,
+{"version": "1.0.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
+   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/std4",
+  {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "0af134abc3d7433de13467d9dc4281e155c1fbfd",
-   "name": "std",
+   "rev": "2506c85498141bc8ab3ee745bcb06021c3ed9a80",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing",
+   "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "importGraph",

lakefile.toml

@@ -0,0 +1,29 @@
+name = "importGraph"
+defaultTargets = ["ImportGraph", "graph"]
+testRunner = "test"
+
+[[require]]
+name = "Cli"
+git = "https://github.com/leanprover/lean4-cli"
+rev = "main"
+
+[[require]]
+name = "batteries"
+git = "https://github.com/leanprover-community/batteries"
+rev = "main"
+
+[[lean_lib]]
+name = "ImportGraph"
+
+# `lake exe graph` constructs import graphs in `.dot` or graphical formats.
+[[lean_exe]]
+name = "graph"
+root = "Main"
+# Enables the use of the Lean interpreter by the executable (e.g., `runFrontend`) 
+# at the expense of increased binary size on Linux.
+# Remove this line if you do not need such functionality.
+supportInterpreter = true
+
+[[lean_exe]]
+name = "test"
+srcDir = "scripts"

lean-toolchain

@@ -1 +1,2 @@
-leanprover/lean4:nightly-2024-04-02
+leanprover/lean4:nightly-2024-06-15
+

scripts/test.lean

@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2024 Kim Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+open IO.Process
+open System
+
+/-
+This is a copy-paste from Batteries test runner.
+If https://github.com/leanprover/lean4/pull/4121 is resolved, use Batteries' script directly.
+-/
+
+/--
+Run tests.
+
+If no arguments are provided, run everything in the `test/` directory.
+
+If arguments are provided, assume they are names of files in the `test/` directory,
+and just run those.
+-/
+def main (args : List String) : IO Unit := do
+  -- We first run `lake build`, to ensure oleans are available.
+  -- Alternatively, we could use `lake lean` below instead of `lake env lean`,
+  -- but currently with parallelism this results in build jobs interfering with each other.
+  _ ← (← IO.Process.spawn { cmd := "lake", args := #["build"] }).wait
+  -- Collect test targets, either from the command line or by walking the `test/` directory.
+  let targets ← match args with
+  | [] => System.FilePath.walkDir "./test"
+  | _ => pure <| (args.map fun t => mkFilePath [".", "test", t] |>.withExtension "lean") |>.toArray
+  let existing ← targets.filterM fun t => do pure <| (← t.pathExists) && !(← t.isDir)
+  -- Generate a `lake env lean` task for each test target.
+  let tasks ← existing.mapM fun t => do
+    IO.asTask do
+      let out ← IO.Process.output
+        { cmd := "lake",
+          args := #["env", "lean", t.toString],
+          env := #[("LEAN_ABORT_ON_PANIC", "1")] }
+      if out.exitCode = 0 then
+        IO.println s!"Test succeeded: {t}"
+      else
+        IO.eprintln s!"Test failed: `lake env lean {t}` produced:"
+        unless out.stdout.isEmpty do IO.eprintln out.stdout
+        unless out.stderr.isEmpty do IO.eprintln out.stderr
+      pure out.exitCode
+  -- Wait on all the jobs and exit with 1 if any failed.
+  let mut exitCode : UInt8 := 0
+  for t in tasks do
+    let e ← IO.wait t
+    match e with
+    | .ok 0 => pure ()
+    | _ => exitCode := 1
+  exit exitCode

test/Imports.lean

@@ -7,23 +7,19 @@ def importTest : CoreM Unit := do
   let x ← redundantImports
   logInfo s!"{x.toArray}"
 
-/-
-info:
-Found the following transitively redundant imports:
+/--
+info: Found the following transitively redundant imports:
 ImportGraph.RequiredModules
 -/
+#guard_msgs in
 #redundant_imports
 
-/-
-info:
-import ImportGraph.Imports
--/
+/-- info: import ImportGraph.Imports -/
+#guard_msgs in
 #minimize_imports
 
-/-
-info:
-[ImportGraph.Imports]
--/
+/-- info: [ImportGraph.Imports] -/
+#guard_msgs in
 #find_home importTest
 
 
@@ -50,8 +46,6 @@ elab "#my_test" : command => do
   logInfo s!"{mi.toArray}"
   pure ()
 
-/-
-info:
-#[ImportGraph.RequiredModules]
--/
+/-- info: #[ImportGraph.Imports] -/
+#guard_msgs in
 #my_test