Reverse FFI with Lakefile

Stream: lean4

[fiforeach]

I am trying to create a lakefile.lean to work with reverse FFI.

What I would like to do is something along the lines of

import Lake
open Lake DSL System

package lakefile_for_exe

lean_lib SumOfTwo where
  srcDir := "lean"

input_file main.c where
  path := "c" / "main.c"
  text := true

target main.o pkg : FilePath := do
  let oFile := pkg.buildDir / "c" / "main.o"
  let srcJob ← main.c.fetch
  let weakArgs := #["-I", (← getLeanIncludeDir).toString]
  buildO oFile srcJob weakArgs #["-fPIC"] "cc"

@[default_target]
target exe pkg : FilePath := do
  let mainO ← main.o.fetch
  let exeName := pkg.binDir / "main"
  buildLeanExe exeName #[mainO] #[`@SumOfTwo:static]
--                                ^^^^^^^^^^^^^^^^^

That is, I would like to leverage the build infrastructure given by lean_lib, instead of defining all the targets manually myself. Is this possible or are there other options available that would avoid having to specify targets for all files I would like to generate? (If not an immediate follow-up question would be how to create the relevant static library in such a way that I can create the final executable using a lakefile.)

[fiforeach]

After gaining more experience with Lakefiles, I was able to reproduce the flags found in the Reverse FFI example and came up with the following

target exe pkg : System.FilePath := do
  let exeFile := pkg.binDir / "main"
  let mainO ← main.o.fetch
  let shared ← (← SumOfTwo.get).shared.fetch
  let weakArgs := #[
    "-I", (← getLeanIncludeDir).toString,
    "-L", (← getLeanLibDir).toString,
    "-lInit_shared",
    "-lleanshared_2",
    "-lleanshared_1",
    "-lleanshared",
    s!"-Wl,-rpath,{← getLeanLibDir}",
    s!"-Wl,-rpath,{pkg.buildDir}/lib",
  ]
  let leanArgs ← getLeanLinkSharedFlags
  buildLeanExe exeFile #[mainO] #[shared] weakArgs leanArgs

This produces a functioning binary.