FFI dynamic linking

Stream: lean4

[Philip Zucker]

I'm trying to use Lean as a replacement for the way I use jupyter notebooks. A lot of things I do in jupyter notebooks are very hacky and involve printing files and running bash commands. One thing in particular I like to do is interactively dynamically link into libraries to explore them or explore compiling snippets of assembly or C. After a good couple days, I can't figure out how to do this in Lean. This is my best attempt.

def compile_C (code : String) : IO Unit := do
  IO.FS.writeFile "/tmp/leany.c" code
  let stdout <- IO.Process.run {
    cmd := "gcc",
    args := #["-c", "-fPIC", "-o", "/tmp/leany.o", "/tmp/leany.c"],
  }
  IO.println stdout
  let stdout2 <- IO.Process.run {
    cmd := "gcc",
    args := #["-shared", "-o", "/tmp/leany.so", "/tmp/leany.o"],
  }
  --let dylib <- Lean.Dynlib.load "/tmp/leany.so"
  Lean.loadDynlib "/tmp/leany.so" -- This will load the shared library



#eval compile_C r#"
#include <stdint.h>
uint64_t l_myadd(uint64_t a, uint64_t b) {
return a + b;
}"#

@[extern "myadd"]
opaque myadd (a b : UInt64) : UInt64

#eval myadd 5 7 -- segafaults

Suggestions? Maybe I need to split into multiple files? Or just impossible with the way lean compilation is set up? Super hacky segfault skirting solutions are fine for my purposes. This isn't and never will be production code. The hackier, the better really.

[Philip Zucker]

For future reference, my best understanding of the issue is that lean generates unboxing code when this is done in a separate file. Copying over such unboxing C code combined with supportInterpreter = true in my lakefile.toml seems to work. I'd guess this is using possibly unstable parts of C / linking mechanisms.

def bash (cmd : String) (_ : Unit) : IO Unit := do
  let output <- IO.Process.output {
    cmd := "bash",
    args := #["-c", cmd],
  }
  IO.println output.stdout
  IO.println output.stderr

-- LEAN_EXPORTING is at least one way to make symbols global.
def compile_C (code : String) : IO Unit := do
  IO.FS.writeFile "/tmp/leany.c" code
  bash "leanc -c -DLEAN_EXPORTING -fPIC -o /tmp/leany.o /tmp/leany.c" ()
  bash "leanc -shared -o /tmp/leany.so /tmp/leany.o" ()
  Lean.loadDynlib "/tmp/leany.so" -- This will load the shared library

-- https://proofassistants.stackexchange.com/questions/4801/how-to-eval-a-ffi-function-in-vscode-in-lean-4
#eval compile_C r#"
#include <stdint.h>
#include <lean/lean.h>
LEAN_EXPORT uint64_t myadd(uint64_t a, uint64_t b) {
return a + b;
}

LEAN_EXPORT lean_object* l_myadd___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint64_t x_3; uint64_t x_4; uint64_t x_5; lean_object* x_6;
x_3 = lean_unbox_uint64(x_1);
lean_dec(x_1);
x_4 = lean_unbox_uint64(x_2);
lean_dec(x_2);
x_5 = myadd(x_3, x_4);
x_6 = lean_box_uint64(x_5);
return x_6;
}
}
"#

@[extern "myadd"]
opaque myadd (a b : UInt64) : UInt64

#eval myadd 5 7 -- Infoview returns 12