diff --git a/Test/Main.lean b/Test/Main.lean index e5cf285..8d9a87d 100644 --- a/Test/Main.lean +++ b/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) diff --git a/lake-manifest.json b/lake-manifest.json index e1545af..a585fc9 100644 --- a/lake-manifest.json +++ b/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"} diff --git a/lakefile.lean b/lakefile.lean index 2aa3986..ddf721a 100644 --- a/lakefile.lean +++ b/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]