docs: Add FFI template

templates/ffi/FFI.lean

@@ -0,0 +1,3 @@
+-- This module serves as the root of the `FFI` library.
+-- Import modules here that should be built as part of the library.
+import FFI.Basic

templates/ffi/FFI/Basic.lean

@@ -0,0 +1,5 @@
+import Blake3
+
+abbrev input : ByteArray := ⟨#[0]⟩
+
+def myHash := (Blake3.hash input).val.data

templates/ffi/Main.lean

@@ -0,0 +1,5 @@
+import FFI
+
+def main : IO Unit :=
+  IO.println s!"Hash of [0]: {myHash}"
+

templates/ffi/flake.nix

@@ -0,0 +1,63 @@
+{
+  description = "Lean 4 Example Project";
+
+  inputs = {
+    nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
+    flake-parts.url = "github:hercules-ci/flake-parts";
+    lean4-nix = {
+      url = "github:argumentcomputer/lean4-nix";
+      inputs.nixpkgs.follows = "nixpkgs";
+    };
+    blake3-lean = {
+      url = "github:argumentcomputer/Blake3.lean?rev=29018d578b043f6638907f3425af839eec345361";
+      inputs.nixpkgs.follows = "nixpkgs";
+    };
+  };
+
+  outputs = inputs @ {
+    nixpkgs,
+    flake-parts,
+    lean4-nix,
+    blake3-lean,
+    ...
+  }:
+    flake-parts.lib.mkFlake {inherit inputs;} {
+      systems = [
+        "aarch64-darwin"
+        "aarch64-linux"
+        "x86_64-darwin"
+        "x86_64-linux"
+      ];
+
+      perSystem = {
+        system,
+        pkgs,
+        ...
+      }: 
+      let
+        blake3 = blake3-lean.inputs.blake3;
+        blake3Mod = (blake3-lean.lib { inherit pkgs lean4-nix blake3; }).lib;
+        blake3Lib = blake3Mod.blake3-lib;
+        blake3C = blake3Mod.blake3-c;
+      in
+      {
+        _module.args.pkgs = import nixpkgs {
+          inherit system;
+          overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)];
+        };
+
+        packages.default = (pkgs.lean.buildLeanPackage {
+          name = "ffi";
+          src = ./.;
+          roots = ["FFI" "Main"];
+          deps = [ blake3Lib ];
+          staticLibDeps = [ blake3C ];
+          linkFlags = [ "-L${blake3C}/lib" "-lblake3" ];
+        }).executable;
+
+        devShells.default = pkgs.mkShell {
+          packages = with pkgs.lean; [lean lean-all];
+        };
+      };
+    };
+}

templates/ffi/lake-manifest.json

@@ -0,0 +1,15 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/argumentcomputer/Blake3.lean",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "29018d578b043f6638907f3425af839eec345361",
+   "name": "Blake3",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "29018d578b043f6638907f3425af839eec345361",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "ffi",
+ "lakeDir": ".lake"}

templates/ffi/lakefile.lean

@@ -0,0 +1,15 @@
+import Lake
+open Lake DSL
+
+require Blake3 from git
+  "https://github.com/argumentcomputer/Blake3.lean" @ "29018d578b043f6638907f3425af839eec345361"
+
+package "ffi" where
+  version := v!"0.1.0"
+
+lean_lib «FFI» where
+  -- add library configuration options here
+
+@[default_target]
+lean_exe "ffi" where
+  root := `Main

templates/ffi/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.17.0