ffi_test/lakefile.lean

24 lines
642 B
Text

import Lake
open Lake DSL
package "ffi_test" where
version := v!"0.1.0"
lean_lib «FfiTest» where
-- add library configuration options here
@[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]