-
Notifications
You must be signed in to change notification settings - Fork 5
/
lakefile.lean
41 lines (31 loc) · 993 Bytes
/
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
import Lake
open Lake DSL
package «SSA» where
@[default_target]
lean_lib SSA {
roots := #[`SSA]
}
lean_exe mlirnatural {
root := `SSA.MLIRNatural
}
lean_exe opt {
root := `SSA.Projects.InstCombine.LLVM.Opt
-- `supportInterpreter` flag needed to link executable with the Lean frontend
supportInterpreter := true
}
lean_exe ssaLLVMEnumerator {
root := `SSA.Projects.InstCombine.LLVM.Enumerator
}
-- PROJECTS
-- ========
/-- Separate lib since it takes quite a while to compile -/
lean_lib AliveExamples {
roots := #[`SSA.Projects.InstCombine.AliveAutoGenerated]
}
lean_lib AliveScaling {
roots := #[`SSA.Projects.InstCombine.ScalingTest]
}
require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "master"
require Cli from git "https://github.com/mhuisi/lean4-cli.git" @ "nightly"
meta if get_config? doc = some "on" then -- dev is so not everyone has to build it
require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"