Configuring Lakefile for multiple c files over the FFI

Stream: lean4

[z battleman]

Hi! I'm wondering if it's possible to configure a lakefile such that different lean files look to different c files when externing their functions (Apologies if my vernacular isn't right). It would be nice to have seperate files Foo.c and Bar.c which correspond to different lean files Foo.lean and Bar.lean`. Looking on Github, it seems most projects use one c file, so I'm wondering if it's possible to do such a thing. Thank you so much!

[z battleman]

In case anyone comes across this in the future, while I didn't manage to figure out how to do exactly what I described, what you can do is #include your other c files in a main c file which is referenced by your lakefile. Then, the only change to your lakefile is adding adding the new lean files to the libRoots in the declaration of the package

[Mac]

The target used in an extern_lib declaration is generally a static library (i.e., a staticLibTarget). You can pass as many different .o file targets as want to such a library and they will all be available to Lean files. To demonstration, here is an adaption of Lake's ffi example with multiple .c file inputs (i.e., a.c, b.c, c.c from the directory c):

def pkgDir := __dir__
def cSrcDir := pkgDir / "c"
def cBuildDir := pkgDir / _package.buildDir / "c"

def oTarget (fileName : String) : FileTarget :=
  let oFile := cBuildDir / s!"{fileName}.o"
  let srcTarget := inputFileTarget <| cSrcDir / s!"{fileName}.c"
  fileTargetWithDep oFile srcTarget fun srcFile => do
    compileO oFile srcFile #["-I", (← getLeanIncludeDir).toString] "cc"

extern_lib cLib :=
  let libFile := cBuildDir / "libffi.a"
  staticLibTarget libFile #[oTarget "a.c", oTarget "b.c", oTarget "c.c"]

[z battleman]

oh thank you so much!

[Xubai Wang]

I find it very difficult to express platform specific extern_lib when I'm updating socket package to new lakefile format: moreLibTargets := if Platform.isWindows then #[cLibTarget, inputFileTarget "C:\\Windows\\System32\\ws2_32.dll"] else #[cLibTarget]
Shall we now have conditional elaboration as Lean's builtin feature? For example with section-like format:

section if Platform.isWindows  -- only elaborate when if condition satisfies
extern_lib ws2 :=
  inputFileTarget "C:\\Windows\\System32\\ws2_32.dll"
end

[Mac]

Oof, yeah that is use case I forgot about. As a stop gap solution this should work:

import Lean.Elab.Command
import Lake.Util.EvalTerm
open Lake Lean Elab Command

elab "meta " "if " x:term " then " cmd:command : command => do
  if (← runTermElabM none <| fun _ => evalTerm Bool x) then elabCommand cmd

meta if System.Platform.isWindows then
extern_lib ws2 := inputFileTarget "C:\\Windows\\System32\\ws2_32.dll"

However, I will add a more long term solution later. My idea is to add a when block to specify the condition under which the extern_lib should be use. For example:

extern_lib ws2 :=
  inputFileTarget "C:\\Windows\\System32\\ws2_32.dll"
when
  System.Platform.isWindows

I lean towards this approach as it allows the target to still exist on other platforms (e.g., for potential cross-compilation) but just not be used by default.

I may still add meta utilities like the one above to the DSL, though.

[Xubai Wang]

Great!