forked from argumentcomputer/OpenSSL.lean
-
Notifications
You must be signed in to change notification settings - Fork 0
/
lakefile.lean
35 lines (29 loc) · 900 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
import Lake
open Lake DSL
package OpenSSL {
precompileModules := false
moreLinkArgs := #["-L", "./build/lib", "-lssl", "-lcrypto", "-lffi"]
extraDepTargets := #["ffi"]
}
@[defaultTarget]
lean_lib OpenSSL {
srcDir := "src"
}
def cDir := "native"
def ffiSrc := "native.c"
def ffiO := "ffi.o"
def ffiLib := "ffi"
target ffi.o (pkg : Package) : FilePath := do
let oFile := pkg.buildDir / ffiO
let srcJob ← inputFile <| pkg.dir / cDir / ffiSrc
buildFileAfterDep oFile srcJob fun srcFile => do
let flags := #["-I", (← getLeanIncludeDir).toString,
"-I", (<- IO.getEnv "C_INCLUDE_PATH").getD "", "-fPIC", "-g"]
compileO ffiSrc oFile srcFile flags
target ffi (pkg : Package) : FilePath := do
let name := nameToStaticLib ffiLib
let ffiO ← fetch <| pkg.target ``ffi.o
buildStaticLib (pkg.buildDir / "lib" / name) #[ffiO]
lean_exe test {
root := `test.Tests
}