From b8e28fc11417ef6081e93048d5a303d9fcf3aa72 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Mon, 13 May 2024 09:59:25 +1000
Subject: [PATCH 1/3] feat: switch to using 'lake test' for testing

---
 .github/workflows/build.yml |  2 +-
 lakefile.toml               |  5 ++++
 scripts/test.lean           | 53 +++++++++++++++++++++++++++++++++++++
 3 files changed, 59 insertions(+), 1 deletion(-)
 create mode 100644 scripts/test.lean

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 3d63f57..fd860fa 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -24,4 +24,4 @@ jobs:
       - name: run tests
         id: test
         run: |
-          find test/*.lean -exec lake env lean {} \;
+          lake test
diff --git a/lakefile.toml b/lakefile.toml
index 3af684d..f8404dc 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -1,5 +1,6 @@
 name = "importGraph"
 defaultTargets = ["ImportGraph", "graph"]
+testRunner = "test"
 
 [[require]]
 name = "Cli"
@@ -22,3 +23,7 @@ root = "Main"
 # 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"
diff --git a/scripts/test.lean b/scripts/test.lean
new file mode 100644
index 0000000..fcc6f5f
--- /dev/null
+++ b/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

From 923d1d09a484b8e58dfbdcd69851f3008c8018b8 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Mon, 13 May 2024 10:00:55 +1000
Subject: [PATCH 2/3] break test, for testing

---
 test/Imports.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/Imports.lean b/test/Imports.lean
index 6b7ae01..e116169 100644
--- a/test/Imports.lean
+++ b/test/Imports.lean
@@ -14,7 +14,7 @@ ImportGraph.RequiredModules
 #guard_msgs in
 #redundant_imports
 
-/-- info: import ImportGraph.Imports -/
+/-- info: import ImportGraph.Iports -/
 #guard_msgs in
 #minimize_imports
 

From 15298f2012e6adea70a5fc6a8b32343b27d0ce54 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Mon, 13 May 2024 10:01:57 +1000
Subject: [PATCH 3/3] and restore test

---
 test/Imports.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/Imports.lean b/test/Imports.lean
index e116169..6b7ae01 100644
--- a/test/Imports.lean
+++ b/test/Imports.lean
@@ -14,7 +14,7 @@ ImportGraph.RequiredModules
 #guard_msgs in
 #redundant_imports
 
-/-- info: import ImportGraph.Iports -/
+/-- info: import ImportGraph.Imports -/
 #guard_msgs in
 #minimize_imports