Compiling a CMAKE build as a Lake target

Stream: lean4

[Akhil Reddimalla]

My project structure is roughly as follows:

• projectName
  - Basic.lean
  - FFI.lean
• native
  - src
  - CMAKELISTS.txt
• projectName.lean
• lake-manifest.json
• lakefile.lean
• lean-toolchain
• Main.lean

Now, in lakefile.lean , I want lake to compile the library in the native folder (which is defined by cmake). In the ffi example I see how to do it for a single c/c++ file, but not how you could do it for a cmake project. How can make lean call cmake to build the library? If Lake can't do it is there a way to have lake run a bash script that can handle compiling the native library?

Thanks in advance

[Mac Malone]

Lake targets (e.g., extern_lib, target) can have arbitrary Lean code. For running external processes, Lake provides a helper called proc to hook the output into Lake's standard logging facilities. For example, you could run the CMake configuration step like so:

let cmakeBuildDir := pkg.buildDir / "native"
IO.FS.createDirAll cmakeBuildDir
proc {
  cmd := "cmake"
  args := #["-S", pkg.dir / "native" |>.toString, "-B", cmakeBuildDir.toString]
}

[Mac Malone]

With the configured directory you could then run the configured build system via another proc. For instance, if you are ouputting makefiles (e.g., -G "Unix Makefiles") the next step would be:

proc {
  cmd := "make"
  args := #["-C", cmakeBuildDir.toString, "-j", "4"]
}

[Mac Malone]

This could be wrapped in a target like the following and then lake build native would run the cmake build:

target native pkg : Unit := do
  let cmakeBuildDir := pkg.buildDir / "native"
  IO.FS.createDirAll cmakeBuildDir
  proc {
    cmd := "cmake"
    args := #["-S", pkg.dir / "native" |>.toString, "-B", cmakeBuildDir.toString]
  }
  proc {
    cmd := "make"
    args := #["-C", cmakeBuildDir.toString, "-j", "4"]
  }
  return .nil