Pantograph/Test/Main.lean

59 lines
2.2 KiB
Plaintext
Raw Permalink Normal View History

2023-05-22 11:47:46 -07:00
import LSpec
import Test.Environment
2023-08-13 21:19:06 -07:00
import Test.Integration
2024-03-31 16:43:30 -07:00
import Test.Library
import Test.Metavar
import Test.Proofs
import Test.Serial
2024-04-20 13:09:41 -07:00
import Test.Tactic
2023-05-22 11:47:46 -07:00
-- 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
2023-05-22 11:47:46 -07:00
/-- Main entry of tests; Provide an argument to filter tests by prefix -/
2024-04-06 14:07:13 -07:00
def main (args: List String) := do
let name_filter := args.head?
Lean.initSearchPath (← Lean.findSysroot)
2024-04-06 14:07:13 -07:00
let env_default: Lean.Environment ← Lean.importModules
(imports := #[`Init])
(opts := {})
(trustLevel := 1)
2024-04-06 14:07:13 -07:00
let suites: List (String × List (String × IO LSpec.TestSeq)) := [
("Environment", Environment.suite),
("Integration", Integration.suite env_default),
2024-04-06 14:07:13 -07:00
("Library", Library.suite env_default),
("Metavar", Metavar.suite env_default),
("Proofs", Proofs.suite env_default),
("Serial", Serial.suite env_default),
2024-05-20 11:51:35 -07:00
("Tactic/Congruence", Tactic.Congruence.suite env_default),
2024-04-20 13:09:41 -07:00
("Tactic/Motivated Apply", Tactic.MotivatedApply.suite env_default),
2024-05-05 13:24:29 -07:00
("Tactic/No Confuse", Tactic.NoConfuse.suite env_default),
2024-06-25 08:03:08 -07:00
("Tactic/Prograde", Tactic.Prograde.suite env_default),
]
2024-04-06 14:07:13 -07:00
let tests: List (String × IO LSpec.TestSeq) := suites.foldl (λ acc (name, suite) => acc ++ (addPrefix name suite)) []
LSpec.lspecIO (← runTestGroup name_filter tests)