-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathlakefile.lean
41 lines (34 loc) · 1.13 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
import Lake
open Lake DSL
package c0deine {
-- add package configuration options here
}
lean_lib C0deine {
-- add library configuration options here
}
@[default_target]
lean_exe c0deine {
root := `Main
}
-- use argument "web" for non-local execution
lean_exe wasm_builder {
root := `BuildWasm
}
script js (args : List String) do
let out ← IO.Process.output {
stdin := .piped
stdout := .piped
stderr := .piped
cmd := "node"
args := (".lake/build/wasm/c0deine.js" :: args).toArray
}
IO.print out.stdout
IO.print out.stderr
return out.exitCode
-- require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.8.0"
require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.8.0"
require Cli from git "https://github.com/mhuisi/lean4-cli" @ "nightly"
require numbers from git "https://github.com/T-Brick/Numbers" @ "main"
require controlflow from git "https://github.com/T-Brick/ControlFlow" @ "main"
require wasm from git "https://github.com/T-Brick/lean-wasm" @ "main"
require importGraph from git "https://github.com/leanprover-community/import-graph" @ "v4.8.0"