Merge branch 'dev' into bug/env-add-level

Test/Main.lean

@@ -17,9 +17,9 @@ 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)
+def runTestGroup (nameFilter?: Option String) (tests: List (String × IO LSpec.TestSeq)): IO LSpec.TestSeq := do
+  let tests: List (String × IO LSpec.TestSeq) := match nameFilter? with
+    | .some nameFilter => tests.filter (λ (name, _) => nameFilter.isPrefixOf name)
     | .none => tests
   let tasks: List (String × Task _) ← tests.mapM (λ (name, task) => do
     return (name, ← EIO.asTask task))
@@ -37,7 +37,7 @@ 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?
+  let nameFilter? := args.head?
   Lean.initSearchPath (← Lean.findSysroot)
   let env_default: Lean.Environment ← Lean.importModules
     (imports := #[`Init])
@@ -57,4 +57,4 @@ def main (args: List String) := do
     ("Tactic/Prograde", Tactic.Prograde.suite env_default),
   ]
   let tests: List (String × IO LSpec.TestSeq) := suites.foldl (λ acc (name, suite) => acc ++ (addPrefix name suite)) []
-  LSpec.lspecIO (← runTestGroup name_filter tests)
+  LSpec.lspecEachIO [()] (λ () => runTestGroup nameFilter? tests)

lake-manifest.json

@@ -1,15 +1,15 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/lenianiva/LSpec.git",
+ [{"url": "https://github.com/argumentcomputer/LSpec.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "c492cecd0bc473e2f9c8b94d545d02cc0056034f",
+   "rev": "a6652a48b5c67b0d8dd3930fad6390a97d127e8d",
    "name": "LSpec",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "c492cecd0bc473e2f9c8b94d545d02cc0056034f",
+   "inputRev": "a6652a48b5c67b0d8dd3930fad6390a97d127e8d",
    "inherited": false,
-   "configFile": "lakefile.lean"}],
+   "configFile": "lakefile.toml"}],
  "name": "pantograph",
  "lakeDir": ".lake"}

lakefile.lean

@@ -18,7 +18,7 @@ lean_exe repl {
 }
 
 require LSpec from git
-  "https://github.com/lenianiva/LSpec.git" @ "c492cecd0bc473e2f9c8b94d545d02cc0056034f"
+  "https://github.com/argumentcomputer/LSpec.git" @ "a6652a48b5c67b0d8dd3930fad6390a97d127e8d"
 lean_lib Test {
 }
 @[test_driver]