forked from leanprover/cslib
-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathRunTests.lean
More file actions
41 lines (34 loc) · 980 Bytes
/
RunTests.lean
File metadata and controls
41 lines (34 loc) · 980 Bytes
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
/-
Copyright (c) 2025 Jesse Alama. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jesse Alama
-/
/-!
# Test Runner
This script runs all CSLib tests including:
- Building the CslibTests library
- Running init imports validation
-/
def main (_ : List String) : IO UInt32 := do
-- build CslibTests
IO.println "building CslibTests..."
let CslibTestsResult ← IO.Process.spawn {
cmd := "lake"
args := #["build", "CslibTests"]
} >>= (·.wait)
if CslibTestsResult != 0 then
IO.eprintln "\n✗ CslibTests build failed"
return CslibTestsResult
else
println! ""
-- Run init imports check
IO.println "\nChecking init imports..."
let checkResult ← IO.Process.spawn {
cmd := "lake"
args := #["exe", "checkInitImports"]
} >>= (·.wait)
if checkResult != 0 then
IO.eprintln "\n✗ Init imports check failed"
return checkResult
IO.println "\n✓ All tests passed"
return 0