Changes

7 changed files (+22/-13)

• .clangd (new)
  • @@ -0,0 +1,6 @@
    + CompileFlags: + Add: + - "-I/nix/store/wlavaybjbzgllhq11lib6qgr7rm8imgp-glibc-2.39-52-dev/include/" + - "-I/nix/store/8r55amvr43sm771rgm0sszd05rm8j1cr-sqlite-3.46.0-dev/include/" + - "-I/nix/store/4rz4z2bkb68vwbdxcwq0jxh2fyhhiqkh-clang-wrapper-18.1.8/resource-root/include/" + - "-I/nix/store/10clq066aqh4ajyzn4layvybzvmigx7s-lean4-4.10.0/include/"
• .gitignore
  • @@ -1,2 +1,3 @@
    + /ffi/.lake /.lake /.direnv
• ffi/.gitignore (deleted)
  • @@ -1,1 +0,0 @@
    - /.flake
• ffi/c/ffi.c (new)
  • @@ -0,0 +1,12 @@
    + #include <lean/lean.h> + #include <sqlite3.h> + #include <stdio.h> + + uint32_t myAdd(uint32_t a, uint32_t b) { + printf("a = %d, b = %d\n", a, b); + return a + b; + } + + lean_obj_res myLeanFun() { + return lean_io_result_mk_ok(lean_box(0)); + }
• ffi/c/ffi.cpp (deleted)
  • @@ -1,9 +0,0 @@
    - #include <lean/lean.h> - - extern "C" uint32_t myAdd(uint32_t a, uint32_t b) { - return a + b + something; - } - - extern "C" lean_obj_res myLeanFun() { - return lean_io_result_mk_ok(lean_box(0)); - }
• ffi/lakefile.lean
  • @@ -12,9 +12,9 @@ root := `Main
    target ffi.o pkg : FilePath := do let oFile := pkg.buildDir / "c" / "ffi.o" - let srcJob ← inputTextFile <| pkg.dir / "c" / "ffi.cpp" + let srcJob ← inputTextFile <| pkg.dir / "c" / "ffi.c" let weakArgs := #["-I", (← getLeanIncludeDir).toString] - buildO oFile srcJob weakArgs #["-fPIC"] "clang++" getLeanTrace + buildO oFile srcJob weakArgs #["-fPIC"] "clang" getLeanTrace extern_lib libleanffi pkg := do let ffiO ← ffi.o.fetch
• shell.nix
  • @@ -1,4 +1,4 @@
    { pkgs ? import <nixpkgs> { } }: with pkgs; mkShell { - buildInputs = [ lean4 clang ]; + buildInputs = [ sqlite lean4 clang ]; }