feat: Add Nix flake

.github/workflows/ci.yml

@@ -0,0 +1,31 @@
+name: CI Tests
+
+on:
+  push:
+    branches: main
+  pull_request:
+  workflow_dispatch:
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }}
+  cancel-in-progress: true
+
+jobs:
+  lean:
+    name: Lean Build
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: leanprover/lean-action@v1
+
+  nix:
+    name: Nix Flake Check
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: DeterminateSystems/nix-installer-action@main
+      - uses: cachix/cachix-action@v14
+        with:
+          name: argumentcomputer
+          authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
+      - run: nix flake check

.gitignore

@@ -1,3 +1,4 @@
 /build
 /lake-packages
 .lake/
+/result*

flake.nix

@@ -0,0 +1,58 @@
+{
+  description = "Lean 4 Example Project";
+
+  inputs = {
+    nixpkgs.url = "github:nixos/nixpkgs/nixos-24.11";
+    flake-parts.url = "github:hercules-ci/flake-parts";
+    lean4-nix = {
+      url = "github:argumentcomputer/lean4-nix";
+      inputs.nixpkgs.follows = "nixpkgs";
+      #rev = "";
+    };
+  };
+
+  outputs = inputs @ {
+    nixpkgs,
+    flake-parts,
+    lean4-nix,
+    ...
+  }:
+    flake-parts.lib.mkFlake {inherit inputs;} {
+      systems = [
+        "aarch64-darwin"
+        "aarch64-linux"
+        "x86_64-darwin"
+        "x86_64-linux"
+      ];
+
+      flake = {
+        lib = import ./lspec.nix;
+      };
+
+      perSystem = {
+        system,
+        pkgs,
+        self',
+        config,
+        ...
+      }:
+        let
+          lib = (import ./lspec.nix { inherit pkgs lean4-nix; }).lib;
+          lspecBin = lib.lspecLib.executable;
+        in
+      {
+        _module.args.pkgs = import nixpkgs {
+          inherit system;
+          overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)];
+        };
+        # TODO: Replace with a Nix-compatible binary
+        # Running `lspecBin` will cause an error due to calling `lake` explicitly and only parsing `lakefile.lean` files
+        # It is included for completeness only
+        #packages.default = lspecBin;
+
+        devShells.default = pkgs.mkShell {
+          packages = with pkgs.lean; [lean lean-all];
+        };
+    };
+  };
+}

lspec.nix

@@ -0,0 +1,78 @@
+{pkgs, lean4-nix}:
+let
+  # Creates a Lean package for LSpec
+  lspecLib = ((lean4-nix.lake {inherit pkgs;}).mkPackage {
+    name = "LSpec";
+    src = ./.;
+    roots = ["Main" "LSpec"];
+  });
+
+  # Extracts test names from the lakefile
+  extractTestNames = src: pkgs.runCommand "extract-test-names" {
+    buildInputs = [ pkgs.gnused pkgs.gnugrep ];
+  } ''
+    if [ ! -f ${src}/lakefile.lean ]; then
+      echo "Error: lakefile.lean not found" >&2
+      exit 1
+    fi
+
+    grep -o "lean_exe Tests\.[^ ]*" ${src}/lakefile.lean | \
+      sed 's/lean_exe Tests\.//' > $out
+  '';
+
+  # Reads the test names into a Nix list
+  testNames = src:
+    let
+      content = builtins.readFile (extractTestNames src);
+      # Split the content by newlines
+      splitResult = builtins.split "\n" content;
+      # Filter to only keep the string elements
+      isString = x: builtins.typeOf x == "string";
+      # Keep only non-empty strings
+      nonEmptyStrings = builtins.filter (x: isString x && x != "") splitResult;
+    in
+      nonEmptyStrings;
+
+  # Generates test packages for each test in the lakefile
+  mkTests = src: pkgs.lib.genAttrs (testNames src) (name: ((lean4-nix.lake {inherit pkgs;}).mkPackage {
+    inherit name src;
+    roots = ["Tests.${name}"];
+    deps = [ lspecLib ];
+  }).executable);
+
+  # Runs each test package, replicating `lake exe lspec`
+  allTests = src:
+    let
+      tests = mkTests src;
+      testNames = pkgs.lib.attrNames tests;
+    in
+    pkgs.writeShellApplication {
+      name = "all-tests";
+      runtimeInputs = pkgs.lib.attrValues tests;
+      text = ''
+        #!/usr/bin/env bash
+        set -euo pipefail
+
+        echo "Running all tests:"
+
+        ${pkgs.lib.concatMapStringsSep "\n" (string: ''
+          echo "Running ${string}..."
+          ${tests.${string}}/bin/${pkgs.lib.toLower string}
+        '') testNames }
+
+        echo "All tests executed successfully"
+      '';
+    };
+
+  lib = {
+    inherit
+      lspecLib
+      extractTestNames
+      testNames
+      mkTests
+      allTests;
+  };
+in
+{
+  inherit lib;
+}