File size: 2,510 Bytes
0115dcf | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 | import Test.Delate
import Test.Environment
import Test.Frontend
import Test.Integration
import Test.Library
import Test.Metavar
import Test.Parser
import Test.Proofs
import Test.Serial
import Test.Tactic
import LSpec
-- Test running infrastructure
namespace Pantograph.Test
def addPrefix (pref: String) (tests: List (String × α)): List (String × α) :=
tests.map (λ (name, x) => (pref ++ "/" ++ name, x))
abbrev TestTask := Task (Except IO.Error LSpec.TestSeq)
def filterTestGroup (tests : List (String × IO LSpec.TestSeq)) (nameFilter? : Option String)
: IO (List (String × TestTask)) := do
let tests : List (String × IO LSpec.TestSeq) := match nameFilter? with
| .some nameFilter => tests.filter (λ (name, _) => nameFilter.isPrefixOf name)
| .none => tests
tests.mapM λ (name, t) => return (name, ← IO.asTask t)
/-- Runs test in parallel. Filters test name if given -/
def runTestTask (t : (String × TestTask)) : IO LSpec.TestSeq := do
let (name, task) := t
let v: Except IO.Error LSpec.TestSeq := task.get
return match v with
| .ok case => LSpec.group name case
| .error e => expectationFailure name e.toString
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 nameFilter? := args.head?
Lean.initSearchPath (← Lean.findSysroot)
let env_default : Lean.Environment ← Lean.importModules
(imports := #[`Init])
(opts := {})
(trustLevel := 1)
(loadExts := true)
let suites: List (String × (Lean.Environment → List (String × IO LSpec.TestSeq))) := [
("Environment", Environment.suite),
("Frontend/Collect", Frontend.Collect.suite),
("Frontend/Distil", Frontend.Distil.suite),
("Frontend/Refactor", Frontend.Refactor.suite),
("Integration", Integration.suite),
("Library", Library.suite),
("Metavar", Metavar.suite),
("Parser", Parser.suite),
("Proofs", Proofs.suite),
("Delate", Delate.suite),
("Serial", Serial.suite),
("Tactic/Assign", Tactic.Assign.suite),
("Tactic/Fragment", Tactic.Fragment.suite),
("Tactic/Prograde", Tactic.Prograde.suite),
]
let suiterunner (f : Lean.Environment → List (String × IO LSpec.TestSeq)) :=
f env_default
let tests : List (String × IO LSpec.TestSeq) := suites.foldl (init := []) λ acc (name, suite) =>
acc ++ (addPrefix name $ suiterunner suite)
LSpec.lspecEachIO (← filterTestGroup tests nameFilter?) runTestTask
|