feat: initial ffi setup

Changes

16 changed files (+107/-0)

• .envrc (new)
  • @@ -0,0 +1,1 @@
    + use nix
• .gitignore (new)
  • @@ -0,0 +1,2 @@
    + /.lake + /.direnv
• Flean.lean (new)
  • @@ -0,0 +1,6 @@
    + import FFI + + def a := myAdd 2 3 + #check a + #eval a +
• Flean/.gitkeep (new)
• Main.lean (new)
  • @@ -0,0 +1,7 @@
    + import FFI + + def double (f : Nat -> Nat) n := f (f n) + def inc := fun n => n + 1 + + def main : IO Unit := + IO.println s!"Hello, {double inc 100} {myAdd 1 1} {myAdd 1 1} {myAdd 1 1}"
• README.md (new)
  • @@ -0,0 +1,2 @@
    + # flean +
• ffi/.gitignore (new)
  • @@ -0,0 +1,1 @@
    + /.flake
• ffi/c/ffi.cpp (new)
  • @@ -0,0 +1,9 @@
    + #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/lake-manifest.json (new)
  • @@ -0,0 +1,5 @@
    + {"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "ffi", + "lakeDir": ".lake"}
• ffi/lakefile.lean (new)
  • @@ -0,0 +1,22 @@
    + import Lake + open System Lake DSL + + package ffi where + srcDir := "lean" + + lean_lib FFI + + @[default_target] + lean_exe test where + root := `Main + + target ffi.o pkg : FilePath := do + let oFile := pkg.buildDir / "c" / "ffi.o" + let srcJob ← inputTextFile <| pkg.dir / "c" / "ffi.cpp" + let weakArgs := #["-I", (← getLeanIncludeDir).toString] + buildO oFile srcJob weakArgs #["-fPIC"] "clang++" getLeanTrace + + extern_lib libleanffi pkg := do + let ffiO ← ffi.o.fetch + let name := nameToStaticLib "leanffi" + buildStaticLib (pkg.nativeLibDir / name) #[ffiO]
• ffi/lean/FFI.lean (new)
  • @@ -0,0 +1,3 @@
    + @[extern "myAdd"] + opaque myAdd : UInt32 → UInt32 → UInt32 +
• ffi/lean/Main.lean (new)
  • @@ -0,0 +1,9 @@
    + import FFI + + open IO + + def main : IO Unit := do + println $ myAdd 1 2 + println $ myAdd 0 0 + + #check myAdd 1 2
• lake-manifest.json (new)
  • @@ -0,0 +1,22 @@
    + {"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": + [{"type": "path", + "scope": "", + "name": "ffi", + "manifestFile": "lake-manifest.json", + "inherited": false, + "dir": "./ffi", + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "", + "rev": "80520e5834d0d9a2446cb88ea3d2a38a94d2e143", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": false, + "configFile": "lakefile.toml"}], + "name": "flean", + "lakeDir": ".lake"}
• lakefile.lean (new)
  • @@ -0,0 +1,13 @@
    + import Lake + open Lake DSL + + package flean + + lean_lib Flean + + @[default_target] + lean_exe flean where + root := `Main + + require ffi from "ffi" + require batteries from git "https://github.com/leanprover-community/batteries" @ "main"
• lean-toolchain (new)
  • @@ -0,0 +1,1 @@
    + leanprover/lean4:4.9.0
• shell.nix (new)
  • @@ -0,0 +1,4 @@
    + { pkgs ? import <nixpkgs> { } }: + with pkgs; mkShell { + buildInputs = [ lean4 clang ]; + }