Strata/lakefile.toml at main · strata-org/Strata · GitHub

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
name = "Strata"
version = "0.1.0"
defaultTargets = ["Strata", "strata", "StrataMain", "StrataToCBMC", "StrataCoreToGoto"]
testDriver = "StrataTestMain"
lintDriver = "CheckImports"

[[require]]
name = "plausible"
git = "https://github.com/leanprover-community/plausible.git"
rev = "bump_to_v4.29.0-rc8"

[[lean_lib]]
name = "Strata"

[[lean_exe]]
name = "strata"
root = "StrataMain"

[[lean_lib]]
name = "StrataExamples"
globs = ["Examples.Lean.+"]

[[lean_lib]]
name = "StrataTest"
globs = ["StrataTest.+"]

[[lean_exe]]
name = "StrataTestMain"
root = "Scripts.StrataTestMain"
needs = ["StrataTest"]

[[lean_exe]]
name = "StrataToCBMC"

[[lean_exe]]
name = "StrataCoreToGoto"

[[lean_exe]]
name = "CheckImports"
root = "Scripts.CheckImports"

[[lean_exe]]
name = "ImportStats"
root = "Scripts.ImportStats"

[[lean_exe]]
name = "DiffTestCore"