forked from ufmg-smite/lean-smt
-
Notifications
You must be signed in to change notification settings - Fork 0
/
lakefile.lean
73 lines (65 loc) · 1.97 KB
/
lakefile.lean
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
73
import Lake
open Lake DSL
package smt where
precompileModules := true
@[defaultTarget]
lean_lib Smt
open Std
open System
partial def readAllFiles (dir : FilePath) : IO (Array FilePath) := do
let mut files := #[]
for entry in (← FilePath.readDir dir) do
if ← entry.path.isDir then
files := (← readAllFiles entry.path) ++ files
else
files := files.push entry.path
return files
/--
Run tests.
USAGE:
lake script run test
Run tests.
-/
script test do
let lean := match (← Lake.findLeanInstall?) with
| none => panic! "Error: could not find lean executable."
| some i => i.lean
let files ← readAllFiles (FilePath.mk "Test")
let mut tests : Array FilePath := #[]
let mut expected : Array FilePath := #[]
for file in files do
if file.extension = some "lean" then
tests := tests.push file
else if file.extension = some "expected" then
expected := expected.push file
let mut tasks := []
for t in tests do
let e := t.withExtension "expected"
if (expected.contains e) then
tasks := (← IO.asTask (runTest lean t e)) :: tasks
else
IO.println s!"Error: Could not find {e}"
return 1
for task in tasks do
let code ← IO.ofExcept task.get
if code ≠ 0 then
return code
return 0
where
runTest (lean : FilePath) (test : FilePath) (expected : FilePath) : IO UInt32 := do
let path := Lake.defaultBuildDir.join Lake.defaultOleanDir.toString
IO.println s!"Start : {test}"
let out ← IO.Process.output {
cmd := lean.toString
args := #[test.toString],
env := #[("LEAN_PATH", path.toString)]
}
let expected ← IO.FS.readFile expected
if ¬out.stderr.isEmpty ∨ out.stdout ≠ expected then
IO.println s!"Failed: {test}"
IO.println s!"Stderr:\n{out.stderr}"
IO.println s!"Stdout:\n{out.stdout}"
IO.println s!"Expect:\n{expected}"
return 2
IO.println s!"Passed: {test}"
return 0