README.md

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

Test/Common.lean

@@ -41,6 +41,28 @@ 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

Test/Main.lean

@@ -6,33 +6,8 @@ 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)