From 4cbfc4529294fcf3395f3d96b06c045827cd44c1 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sat, 6 Apr 2024 14:07:13 -0700
Subject: [PATCH 1/3] test: Parallel testing infrastructure

---
 Test/Common.lean      | 29 +++++++++++++++++++++++++++--
 Test/Environment.lean | 11 ++++++-----
 Test/Integration.lean | 16 ++++++++--------
 Test/Library.lean     | 14 +++++---------
 Test/Main.lean        | 25 +++++++++++++++----------
 Test/Metavar.lean     | 13 ++-----------
 Test/Proofs.lean      | 14 ++------------
 Test/Serial.lean      | 20 ++++++++------------
 8 files changed, 73 insertions(+), 69 deletions(-)

diff --git a/Test/Common.lean b/Test/Common.lean
index 378dce8..2711ff2 100644
--- a/Test/Common.lean
+++ b/Test/Common.lean
@@ -8,6 +8,7 @@ open Lean
 
 namespace Pantograph
 
+-- Auxiliary functions
 namespace Protocol
 /-- Set internal names to "" -/
 def Goal.devolatilize (goal: Goal): Goal :=
@@ -37,9 +38,32 @@ def TacticResult.toString : TacticResult → String
   | .parseError error => s!".parseError {error}"
   | .indexError index => s!".indexError {index}"
 
-def assertUnreachable (message: String): LSpec.TestSeq := LSpec.check message false
+namespace Test
 
-open Lean
+def expectationFailure (desc: String) (error: String): LSpec.TestSeq := LSpec.test desc (LSpec.ExpectationFailure "ok _" error)
+
+-- Test running infrastructure
+
+def addPrefix (pref: String) (tests: List (String × α)): List (String  × α) :=
+  tests.map (λ (name, x) => (pref ++ "/" ++ name, x))
+
+/-- Runs test in parallel. Filters test name if given -/
+def runTestGroup (filter: Option String) (tests: List (String × IO LSpec.TestSeq)): IO LSpec.TestSeq := do
+  let tests: List (String × IO LSpec.TestSeq) := match filter with
+    | .some filter => tests.filter (λ (name, _) => filter.isPrefixOf name)
+    | .none => tests
+  let tasks: List (String × Task _) ← tests.mapM (λ (name, task) => do
+    return (name, ← EIO.asTask task))
+  let all := tasks.foldl (λ acc (name, task) =>
+    let v: Except IO.Error LSpec.TestSeq := Task.get task
+    match v with
+    | .ok case => acc ++ (LSpec.group name case)
+    | .error e => acc ++ (expectationFailure name e.toString)
+    ) LSpec.TestSeq.done
+  return all
+
+
+def assertUnreachable (message: String): LSpec.TestSeq := LSpec.check message false
 
 def runCoreMSeq (env: Environment) (coreM: CoreM LSpec.TestSeq) (options: Array String := #[]): IO LSpec.TestSeq := do
   let coreContext: Core.Context ← createCoreContext options
@@ -59,5 +83,6 @@ def defaultTermElabMContext: Lean.Elab.Term.Context := {
     declName? := some "_pantograph".toName,
     errToSorry := false
   }
+end Test
 
 end Pantograph
diff --git a/Test/Environment.lean b/Test/Environment.lean
index 7a398da..927793d 100644
--- a/Test/Environment.lean
+++ b/Test/Environment.lean
@@ -94,10 +94,11 @@ def test_inspect: IO LSpec.TestSeq := do
     ) LSpec.TestSeq.done
   runCoreMSeq env inner
 
-def suite: IO LSpec.TestSeq := do
-  return LSpec.group "Environment" $
-    (LSpec.group "Catalog" (← test_catalog)) ++
-    (LSpec.group "Symbol visibility" (← test_symbol_visibility)) ++
-    (LSpec.group "Inspect" (← test_inspect))
+def suite: List (String × IO LSpec.TestSeq) :=
+  [
+    ("Catalog", test_catalog),
+    ("Symbol Visibility", test_symbol_visibility),
+    ("Inspect", test_inspect),
+  ]
 
 end Pantograph.Test.Environment
diff --git a/Test/Integration.lean b/Test/Integration.lean
index 5f2523b..4f3bcba 100644
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@@ -112,7 +112,7 @@ def test_tactic : IO LSpec.TestSeq :=
       Protocol.GoalTacticResult))
   ]
 
-def test_env : IO LSpec.TestSeq :=
+def test_env_add_inspect : IO LSpec.TestSeq :=
   let name1 := "Pantograph.mystery"
   let name2 := "Pantograph.mystery2"
   subroutine_runner [
@@ -148,13 +148,13 @@ def test_env : IO LSpec.TestSeq :=
       Protocol.EnvInspectResult))
   ]
 
-def suite: IO LSpec.TestSeq := do
-
-  return LSpec.group "Integration" $
-    (LSpec.group "Option modify" (← test_option_modify)) ++
-    (LSpec.group "Malformed command" (← test_malformed_command)) ++
-    (LSpec.group "Tactic" (← test_tactic)) ++
-    (LSpec.group "Env" (← test_env))
+def suite: List (String × IO LSpec.TestSeq) :=
+  [
+    ("Option modify", test_option_modify),
+    ("Malformed command", test_malformed_command),
+    ("Tactic", test_tactic),
+    ("env.add env.inspect", test_env_add_inspect),
+  ]
 
 
 end Pantograph.Test.Integration
diff --git a/Test/Library.lean b/Test/Library.lean
index 8c935ee..d995374 100644
--- a/Test/Library.lean
+++ b/Test/Library.lean
@@ -8,11 +8,7 @@ open Pantograph
 
 namespace Pantograph.Test.Library
 
-def test_expr_echo: IO LSpec.TestSeq := do
-  let env: Environment ← importModules
-    (imports := #[`Init])
-    (opts := {})
-    (trustLevel := 1)
+def test_expr_echo (env: Environment): IO LSpec.TestSeq := do
   let inner: CoreM LSpec.TestSeq := do
     let prop_and_proof := "⟨∀ (x: Prop), x → x, λ (x: Prop) (h: x) => h⟩"
     let tests := LSpec.TestSeq.done
@@ -34,9 +30,9 @@ def test_expr_echo: IO LSpec.TestSeq := do
     return tests
   runCoreMSeq env (options := #["pp.proofs.threshold=100"]) inner
 
-def suite: IO LSpec.TestSeq := do
-
-  return LSpec.group "Library" $
-    (LSpec.group "ExprEcho" (← test_expr_echo))
+def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
+  [
+    ("expr_echo", test_expr_echo env),
+  ]
 
 end Pantograph.Test.Library
diff --git a/Test/Main.lean b/Test/Main.lean
index 6baffad..42b9d5e 100644
--- a/Test/Main.lean
+++ b/Test/Main.lean
@@ -8,16 +8,21 @@ import Test.Serial
 
 open Pantograph.Test
 
-def main := do
+def main (args: List String) := do
+  let name_filter := args.head?
   Lean.initSearchPath (← Lean.findSysroot)
+  let env_default: Lean.Environment ← Lean.importModules
+    (imports := #[`Init])
+    (opts := {})
+    (trustLevel := 1)
 
-  let suites := [
-    Environment.suite,
-    Integration.suite,
-    Library.suite,
-    Metavar.suite,
-    Proofs.suite,
-    Serial.suite,
+  let suites: List (String × List (String × IO LSpec.TestSeq)) := [
+    ("Environment", Environment.suite),
+    ("Integration", Integration.suite),
+    ("Library", Library.suite env_default),
+    ("Metavar", Metavar.suite env_default),
+    ("Proofs", Proofs.suite env_default),
+    ("Serial", Serial.suite env_default),
   ]
-  let all ← suites.foldlM (λ acc m => do pure $ acc ++ (← m)) LSpec.TestSeq.done
-  LSpec.lspecIO $ all
+  let tests: List (String × IO LSpec.TestSeq) := suites.foldl (λ acc (name, suite) => acc ++ (addPrefix name suite)) []
+  LSpec.lspecIO (← runTestGroup name_filter tests)
diff --git a/Test/Metavar.lean b/Test/Metavar.lean
index 9595b35..433326d 100644
--- a/Test/Metavar.lean
+++ b/Test/Metavar.lean
@@ -268,11 +268,7 @@ def test_partial_continuation: TestM Unit := do
   return ()
 
 
-def suite: IO LSpec.TestSeq := do
-  let env: Lean.Environment ← Lean.importModules
-    (imports := #["Init"].map (λ str => { module := str.toName, runtimeOnly := false }))
-    (opts := {})
-    (trustLevel := 1)
+def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [
     ("Instantiate", test_instantiate_mvar),
     ("2 < 5", test_m_couple),
@@ -280,11 +276,6 @@ def suite: IO LSpec.TestSeq := do
     ("Proposition Generation", test_proposition_generation),
     ("Partial Continuation", test_partial_continuation)
   ]
-  let tests ← tests.foldlM (fun acc tests => do
-    let (name, tests) := tests
-    let tests ← proofRunner env tests
-    return acc ++ (LSpec.group name tests)) LSpec.TestSeq.done
-
-  return LSpec.group "Metavar" tests
+  tests.map (fun (name, test) => (name, proofRunner env test))
 
 end Pantograph.Test.Metavar
diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index 133eee0..a4a1927 100644
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@@ -293,12 +293,7 @@ def proof_or_comm: TestM Unit := do
       ]
     }
 
-
-def suite: IO LSpec.TestSeq := do
-  let env: Lean.Environment ← Lean.importModules
-    (imports := #[{ module := "Init".toName, runtimeOnly := false}])
-    (opts := {})
-    (trustLevel := 1)
+def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [
     ("Nat.add_comm", proof_nat_add_comm false),
     ("Nat.add_comm manual", proof_nat_add_comm true),
@@ -306,11 +301,6 @@ def suite: IO LSpec.TestSeq := do
     ("arithmetic", proof_arith),
     ("Or.comm", proof_or_comm)
   ]
-  let tests ← tests.foldlM (fun acc tests => do
-    let (name, tests) := tests
-    let tests ← proofRunner env tests
-    return acc ++ (LSpec.group name tests)) LSpec.TestSeq.done
-
-  return LSpec.group "Proofs" tests
+  tests.map (fun (name, test) => (name, proofRunner env test))
 
 end Pantograph.Test.Proofs
diff --git a/Test/Serial.lean b/Test/Serial.lean
index f186bbb..0a46acc 100644
--- a/Test/Serial.lean
+++ b/Test/Serial.lean
@@ -72,17 +72,13 @@ def test_instance (env: Environment): IO LSpec.TestSeq := do
     return LSpec.TestSeq.done
   runMetaMSeq env metaM
 
-def suite: IO LSpec.TestSeq := do
-  let env: Environment ← importModules
-    (imports := #["Init"].map (λ str => { module := str.toName, runtimeOnly := false }))
-    (opts := {})
-    (trustLevel := 1)
-
-  return LSpec.group "Serialization" $
-    (LSpec.group "name_to_ast" test_name_to_ast) ++
-    (LSpec.group "Expression binder" (← test_expr_to_binder env)) ++
-    (LSpec.group "Sexp from symbol" (← test_sexp_of_symbol env)) ++
-    (LSpec.group "Sexp from expr" (← test_sexp_of_expr env)) ++
-    (LSpec.group "Instance" (← test_instance env))
+def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
+  [
+    ("name_to_ast", do pure test_name_to_ast),
+    ("Expression binder", test_expr_to_binder env),
+    ("Sexp from symbol", test_sexp_of_symbol env),
+    ("Sexp from expr", test_sexp_of_expr env),
+    ("Instance", test_instance env),
+  ]
 
 end Pantograph.Test.Serial
-- 
2.44.1


From fd47711e1f090dd527e1f26bf872b95cc7a80f80 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sat, 6 Apr 2024 14:14:30 -0700
Subject: [PATCH 2/3] test: Move parallelism to Test/Main.lean

---
 Test/Common.lean | 22 ----------------------
 Test/Main.lean   | 25 +++++++++++++++++++++++++
 2 files changed, 25 insertions(+), 22 deletions(-)

diff --git a/Test/Common.lean b/Test/Common.lean
index 2711ff2..9c13a6d 100644
--- a/Test/Common.lean
+++ b/Test/Common.lean
@@ -41,28 +41,6 @@ def TacticResult.toString : TacticResult → String
 namespace Test
 
 def expectationFailure (desc: String) (error: String): LSpec.TestSeq := LSpec.test desc (LSpec.ExpectationFailure "ok _" error)
-
--- Test running infrastructure
-
-def addPrefix (pref: String) (tests: List (String × α)): List (String  × α) :=
-  tests.map (λ (name, x) => (pref ++ "/" ++ name, x))
-
-/-- Runs test in parallel. Filters test name if given -/
-def runTestGroup (filter: Option String) (tests: List (String × IO LSpec.TestSeq)): IO LSpec.TestSeq := do
-  let tests: List (String × IO LSpec.TestSeq) := match filter with
-    | .some filter => tests.filter (λ (name, _) => filter.isPrefixOf name)
-    | .none => tests
-  let tasks: List (String × Task _) ← tests.mapM (λ (name, task) => do
-    return (name, ← EIO.asTask task))
-  let all := tasks.foldl (λ acc (name, task) =>
-    let v: Except IO.Error LSpec.TestSeq := Task.get task
-    match v with
-    | .ok case => acc ++ (LSpec.group name case)
-    | .error e => acc ++ (expectationFailure name e.toString)
-    ) LSpec.TestSeq.done
-  return all
-
-
 def assertUnreachable (message: String): LSpec.TestSeq := LSpec.check message false
 
 def runCoreMSeq (env: Environment) (coreM: CoreM LSpec.TestSeq) (options: Array String := #[]): IO LSpec.TestSeq := do
diff --git a/Test/Main.lean b/Test/Main.lean
index 42b9d5e..1aa1d3d 100644
--- a/Test/Main.lean
+++ b/Test/Main.lean
@@ -6,8 +6,33 @@ import Test.Metavar
 import Test.Proofs
 import Test.Serial
 
+-- Test running infrastructure
+
+namespace Pantograph.Test
+
+def addPrefix (pref: String) (tests: List (String × α)): List (String  × α) :=
+  tests.map (λ (name, x) => (pref ++ "/" ++ name, x))
+
+/-- Runs test in parallel. Filters test name if given -/
+def runTestGroup (filter: Option String) (tests: List (String × IO LSpec.TestSeq)): IO LSpec.TestSeq := do
+  let tests: List (String × IO LSpec.TestSeq) := match filter with
+    | .some filter => tests.filter (λ (name, _) => filter.isPrefixOf name)
+    | .none => tests
+  let tasks: List (String × Task _) ← tests.mapM (λ (name, task) => do
+    return (name, ← EIO.asTask task))
+  let all := tasks.foldl (λ acc (name, task) =>
+    let v: Except IO.Error LSpec.TestSeq := Task.get task
+    match v with
+    | .ok case => acc ++ (LSpec.group name case)
+    | .error e => acc ++ (expectationFailure name e.toString)
+    ) LSpec.TestSeq.done
+  return all
+
+end Pantograph.Test
+
 open Pantograph.Test
 
+/-- Main entry of tests; Provide an argument to filter tests by prefix -/
 def main (args: List String) := do
   let name_filter := args.head?
   Lean.initSearchPath (← Lean.findSysroot)
-- 
2.44.1


From d44693e548062145f530fdc7ea6c832c56528208 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sat, 6 Apr 2024 14:15:58 -0700
Subject: [PATCH 3/3] doc: Documentation for `nix flake check`

---
 README.md | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/README.md b/README.md
index 26bf788..f60ee22 100644
--- a/README.md
+++ b/README.md
@@ -132,8 +132,5 @@ requires the presence of `lean-all`.
 
 To run tests:
 ``` sh
-nix build .#checks.${system}.test
+nix flake check
 ```
-
-For example, `${system}` could be `x86_64-linux`. Using `nix develop` drops the
-current session into a development shell with fixed Lean version.
-- 
2.44.1