aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 10 Pull Requests 2 Packages Projects Releases Wiki Activity

Merge pull request 'test: Update LSpec' (#182) from test/build into dev 

Reviewed-on: #182
This commit is contained in:
Leni Aniva 2025-03-29 15:44:28 -07:00
parent 3c07188cdf 2885671490
commit 18446f865e
3 changed files with 10 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
Test/Main.lean
View File

@ -17,9 +17,9 @@ def addPrefix (pref: String) (tests: List (String × α)): List (String × α)
tests.map (λ (name, x) => (pref ++ "/" ++ name, x)) tests.map (λ (name, x) => (pref ++ "/" ++ name, x))
/-- Runs test in parallel. Filters test name if given -/ /-- Runs test in parallel. Filters test name if given -/
def runTestGroup (filter: Option String) (tests: List (String × IO LSpec.TestSeq)): IO LSpec.TestSeq := do def runTestGroup (nameFilter?: Option String) (tests: List (String × IO LSpec.TestSeq)): IO LSpec.TestSeq := do
let tests: List (String × IO LSpec.TestSeq) := match filter with let tests: List (String × IO LSpec.TestSeq) := match nameFilter? with
| .some filter => tests.filter (λ (name, _) => filter.isPrefixOf name) | .some nameFilter => tests.filter (λ (name, _) => nameFilter.isPrefixOf name)
| .none => tests | .none => tests
let tasks: List (String × Task _) ← tests.mapM (λ (name, task) => do let tasks: List (String × Task _) ← tests.mapM (λ (name, task) => do
return (name, ← EIO.asTask task)) return (name, ← EIO.asTask task))
@ -37,7 +37,7 @@ open Pantograph.Test
/-- Main entry of tests; Provide an argument to filter tests by prefix -/ /-- Main entry of tests; Provide an argument to filter tests by prefix -/
def main (args: List String) := do def main (args: List String) := do
let name_filter := args.head? let nameFilter? := args.head?
Lean.initSearchPath (← Lean.findSysroot) Lean.initSearchPath (← Lean.findSysroot)
let env_default: Lean.Environment ← Lean.importModules let env_default: Lean.Environment ← Lean.importModules
(imports := #[`Init]) (imports := #[`Init])
@ -57,4 +57,4 @@ def main (args: List String) := do
("Tactic/Prograde", Tactic.Prograde.suite env_default), ("Tactic/Prograde", Tactic.Prograde.suite env_default),
] ]
let tests: List (String × IO LSpec.TestSeq) := suites.foldl (λ acc (name, suite) => acc ++ (addPrefix name suite)) [] 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)

8
lake-manifest.json
View File

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

2
lakefile.lean
View File

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