FFI用lakefile

最新版はドキュメントと差異が生じている模様なのでメモ。

import Lake

open System Lake DSL

package «myapp» where
  version := v!"0.1.0"
  moreLeancArgs := #["-g", "-O0"]

lean_lib «MyApp»

@[default_target]
lean_exe «myapp» where
  root := `Main
  moreLinkArgs := #["-L", s!"{__dir__}/.lake/build/lib", "-lnative"]

target «native.o» (pkg : NPackage __name__) : System.FilePath := do
  let outFile := pkg.buildDir / "out" / "native.o"
  let source ← inputFile (pkg.dir / "native" / "lib.c") true
  let built ← buildFileAfterDep outFile source λ srcFile => do
    let flags :=
      #[ "-I"
      , (← getLeanIncludeDir).toString
      , "-Wall"
      , "-Werror"
      , "-fPIC"
      , "-g"
      , "-O0"
      , "-std=c17"
      ]
    compileO outFile srcFile flags "clang"
  return built

extern_lib «native» (pkg : NPackage __name__) := do
  let name := nameToStaticLib "native"
  let bi := pkg.target `«native.o»
  let job ← bi.fetch
  buildStaticLib
    (pkg.buildDir / "lib" / name)
    #[job]