2024-10-23 16:03:06 +09:00
|
|
|
import Lake
|
|
|
|
|
open Lake DSL
|
|
|
|
|
|
|
|
|
|
package "ffi_test" where
|
|
|
|
|
version := v!"0.1.0"
|
|
|
|
|
|
|
|
|
|
lean_lib «FfiTest» where
|
|
|
|
|
-- add library configuration options here
|
2024-10-25 16:47:35 +09:00
|
|
|
|
|
|
|
|
@[default_target]
|
|
|
|
|
lean_exe test where
|
|
|
|
|
root := `Main
|
|
|
|
|
|
|
|
|
|
target ffi.o pkg : FilePath := do
|
|
|
|
|
let oFile := pkg.buildDir / "c" / "ffi.o"
|
|
|
|
|
let srcJob ← inputTextFile <| pkg.dir / "c" / "ffi.cpp"
|
|
|
|
|
let weakArgs := #["-I", (← getLeanIncludeDir).toString]
|
|
|
|
|
buildO oFile srcJob weakArgs #["-fPIC"] "c++" getLeanTrace
|
|
|
|
|
|
|
|
|
|
extern_lib libleanffi pkg := do
|
|
|
|
|
let ffiO ← ffi.o.fetch
|
|
|
|
|
let name := nameToStaticLib "leanffi"
|
|
|
|
|
IO.println s!"{repr name}"
|
|
|
|
|
buildStaticLib (pkg.nativeLibDir / name) #[ffiO]
|
