feat: Add Nix build

.github/workflows/ci.yml

@@ -1,15 +1,38 @@
 name: "CI"
+
 on:
   pull_request:
   push:
     branches:
       - main
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }}
+  cancel-in-progress: true
+
 jobs:
-  build:
+  lean-test:
+    name: Lean Tests
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4
       - uses: leanprover/lean-action@v1
         with:
           build-args: "--wfail"
           test: true
+
+  nix-test:
+    name: Nix Tests
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: cachix/install-nix-action@v30
+        with:
+          nix_path: nixpkgs=channel:nixos-unstable
+          github_access_token: ${{ secrets.GITHUB_TOKEN }}
+      - uses: cachix/cachix-action@v15
+        with:
+          name: argumentcomputer
+          authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
+      - run: nix build .#test
+      - run: nix run .#test

.gitignore

@@ -1,2 +1,3 @@
 /.lake
 /blake3
+result*

blake3.nix

@@ -0,0 +1,61 @@
+{
+  pkgs,
+  lean4-nix,
+  blake3,
+}: let
+  blake3Flags = pkgs.lib.concatStringsSep " " [
+    "-DBLAKE3_NO_SSE2"
+    "-DBLAKE3_NO_SSE41"
+    "-DBLAKE3_NO_AVX2"
+    "-DBLAKE3_NO_AVX512"
+    "-DBLAKE3_USE_NEON=0"
+  ];
+  blake3Files = [
+    "blake3"
+    "blake3_dispatch"
+    "blake3_portable"
+  ];
+  buildSteps =
+    builtins.map (file: "gcc -O3 -Wall -c ${blake3}/c/${file}.c -o ${file}.o ${blake3Flags}") blake3Files
+    ++ [
+      "gcc -O3 -Wall -c ffi.c -o ffi.o -I ${pkgs.lean4}/include -I ${blake3}/c"
+      "ar rcs libblake3.a ${(builtins.concatStringsSep " " (builtins.map (str: "${str}.o") blake3Files))} ffi.o"
+    ];
+  blake3-c = pkgs.stdenv.mkDerivation {
+    name = "blake3-c";
+    src = ./.;
+    buildInputs = [pkgs.gcc pkgs.lean.lean-all];
+    buildPhase = builtins.concatStringsSep "\n" buildSteps;
+    installPhase = ''
+      mkdir -p $out/lib $out/include
+      cp libblake3.a $out/lib/
+      cp ${blake3}/c/blake3.h $out/include/
+    '';
+  };
+  blake3-lib = pkgs.lean.buildLeanPackage {
+    name = "blake3-lib";
+    src = ./.;
+    roots = ["Blake3"];
+    linkFlags = ["-L${blake3-c}/lib" "-lblake3"];
+    groupStaticLibs = true;
+  };
+
+  blake3-test = pkgs.lean.buildLeanPackage {
+    name = "blake3-test";
+    src = ./.;
+    roots = ["Blake3Test"];
+    deps = [blake3-lib];
+    linkFlags = ["-L${blake3-c}/lib" "-lblake3"];
+    groupStaticLibs = true;
+  };
+
+  lib = {
+    inherit
+      blake3-c
+      blake3-lib
+      blake3-test
+      ;
+  };
+in {
+  inherit lib;
+}

flake.nix

@@ -0,0 +1,61 @@
+{
+  description = "Blake3 Nix Flake";
+
+  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 = {
+      url = "github:BLAKE3-team/BLAKE3";
+      flake = false;
+    };
+  };
+
+  outputs = inputs @ {
+    nixpkgs,
+    flake-parts,
+    lean4-nix,
+    blake3,
+    ...
+  }:
+    flake-parts.lib.mkFlake {inherit inputs;} {
+      systems = [
+        "aarch64-darwin"
+        "aarch64-linux"
+        "x86_64-darwin"
+        "x86_64-linux"
+      ];
+
+      # Flake output for use downstream
+      flake = {
+        lib = import ./blake3.nix;
+        inputs.blake3 = blake3;
+      };
+
+      perSystem = {
+        system,
+        pkgs,
+        ...
+      }: let
+        lib = (import ./blake3.nix {inherit pkgs lean4-nix blake3;}).lib;
+      in {
+        _module.args.pkgs = import nixpkgs {
+          inherit system;
+          overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)];
+        };
+
+        packages = {
+          test = lib.blake3-test.executable;
+        };
+
+        devShells.default = pkgs.mkShell {
+          packages = with pkgs.lean; [lean lean-all pkgs.gcc pkgs.clang];
+        };
+
+        formatter = pkgs.alejandra;
+      };
+    };
+}