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]