From 6865086944689c421785f3b7397a5e5d3498ea23 Mon Sep 17 00:00:00 2001
From: Samuel Burnham <45365069+samuelburnham@users.noreply.github.com>
Date: Tue, 18 Mar 2025 09:51:50 -0400
Subject: [PATCH] fix: Nix devShell & light refactor

---
 .github/workflows/nix.yml |  9 ++++++---
 Ix/Cli/HashCmd.lean       | 20 ++++++++++----------
 flake.nix                 | 25 +++++++++----------------
 ix.nix                    | 38 ++++++++++++++++++++++++++------------
 ix_test/IxTest.lean       |  4 +---
 5 files changed, 52 insertions(+), 44 deletions(-)

diff --git a/.github/workflows/nix.yml b/.github/workflows/nix.yml
index 50acb80f..cfb6a91e 100644
--- a/.github/workflows/nix.yml
+++ b/.github/workflows/nix.yml
@@ -38,6 +38,9 @@ jobs:
         with:
           nix_path: nixpkgs=channel:nixos-unstable
           github_access_token: ${{ secrets.GITHUB_TOKEN }}
-      # Installs `elan` and `lake` via Nix, which then downloads the Lean toolchain binary
-      # from https://github.com/leanprover/lean4/releases
-      - run: nix develop .#ci --command bash -c "lake build && lake test"
+      - uses: cachix/cachix-action@v15
+        with:
+          name: argumentcomputer
+          authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
+      # Builds and runs tests using Lake as a Nix package
+      - run: nix develop --command bash -c "lake build && lake test"
diff --git a/Ix/Cli/HashCmd.lean b/Ix/Cli/HashCmd.lean
index e941c011..31c784a3 100644
--- a/Ix/Cli/HashCmd.lean
+++ b/Ix/Cli/HashCmd.lean
@@ -23,17 +23,17 @@ def runHash (p : Cli.Parsed) : IO UInt32 := do
      IO.println <| s!"constant'' {x.name}"
   --cronos ← cronos.clock "Run Lean frontend"
 
-  IO.println <| "content-address"
-  -- Start content-addressing
-  cronos ← cronos.clock "Content-address"
-  let stt ← match ← Ix.CanonM.canon constMap delta with
-    | .error err => IO.eprintln err; return 1
-    | .ok stt => pure stt
-  cronos ← cronos.clock "Content-address"
-  stt.store.forM fun adr _ => do
-     IO.println <| s!"{adr}"
+ -- IO.println <| "content-address"
+ -- -- Start content-addressing
+ -- cronos ← cronos.clock "Content-address"
+ -- let stt ← match ← Ix.CanonM.canon constMap delta with
+ --   | .error err => IO.eprintln err; return 1
+ --   | .ok stt => pure stt
+ -- cronos ← cronos.clock "Content-address"
+ -- stt.store.forM fun adr _ => do
+ --    IO.println <| s!"{adr}"
 
-  IO.println cronos.summary
+ -- IO.println cronos.summary
   return 0
 
 def hashCmd : Cli.Cmd := `[Cli|
diff --git a/flake.nix b/flake.nix
index c382c58a..7822f90b 100644
--- a/flake.nix
+++ b/flake.nix
@@ -45,15 +45,6 @@
       perSystem = { system, pkgs, ... }:
       let
         lib = (import ./ix.nix { inherit system pkgs fenix crane lean4-nix blake3-lean; }).lib;
-
-        devShellPkgs = with pkgs; [
-          pkg-config
-          openssl
-          ocl-icd
-          gcc
-          clang
-          lib.rustToolchain
-        ];
       in {
         # Lean overlay
         _module.args.pkgs = import nixpkgs {
@@ -68,15 +59,17 @@
 
         # Provide a unified dev shell with Lean + Rust
         devShells.default = pkgs.mkShell {
-          packages = with pkgs; devShellPkgs ++ [
+          LEAN_SYSROOT="${pkgs.lean.lean-all}";
+          packages = with pkgs; [
+            pkg-config
+            openssl
+            ocl-icd
+            gcc
+            clang
+            lib.rustToolchain
+            rust-analyzer
             lean.lean         # Lean compiler
             lean.lean-all     # Includes Lake, stdlib, etc.
-            pkgs.rust-analyzer
-          ];
-        };
-        devShells.ci = pkgs.mkShell {
-          packages = with pkgs; devShellPkgs ++ [
-            elan
           ];
         };
       };
diff --git a/ix.nix b/ix.nix
index 6cef6aa5..4c4a10c6 100644
--- a/ix.nix
+++ b/ix.nix
@@ -28,23 +28,37 @@ let
   });
 
   # C Package
-  cPkg = pkgs.stdenv.mkDerivation {
+  cPkg = let
+    # Function to get all files in `./c` ending with given extension
+    getFiles = ext: builtins.filter (file: builtins.match (".*" + ext) file != null) (builtins.attrNames (builtins.readDir "${toString ./c}"));
+    # Gets all C files in `./c`, without the extension
+    cFiles = let ext = ".c"; in builtins.map (file: builtins.replaceStrings [ext] [""] file) (getFiles ext);
+    # Creates `gcc -c` command for each C file
+    buildCmd = builtins.map (file: "gcc -Wall -Werror -Wextra -c ${file}.c -o ${file}.o") cFiles;
+    # Final `buildPhase` instructions
+    buildSteps = buildCmd ++
+    [
+      "ar rcs libix_c.a ${builtins.concatStringsSep " " (builtins.map (file: "-o ${file}.o") cFiles)}"
+    ];
+    # Gets all header files in `./c`
+    hFiles = getFiles ".h";
+    # Final `installPhase` instructions
+    installSteps =
+    [
+      "mkdir -p $out/lib $out/include"
+      "cp libix_c.a $out/lib/"
+      "cp ${builtins.concatStringsSep " " hFiles} $out/include/"
+    ];
+  in
+  pkgs.stdenv.mkDerivation {
     pname = "ix_c";
     version = "0.1.0";
     src = ./c;
     buildInputs = [ pkgs.gcc pkgs.lean.lean-all rustPkg ];
-    # Builds the C file
-    buildPhase = ''
-      gcc -Wall -Werror -Wextra -c binius.c -o binius.o
-      gcc -Wall -Werror -Wextra -c unsigned.c -o unsigned.o
-      ar rcs libix_c.a binius.o unsigned.o
-    '';
+    # Builds the C files
+    buildPhase = builtins.concatStringsSep "\n" buildSteps;
     # Installs the library files
-    installPhase = ''
-      mkdir -p $out/lib $out/include
-      cp libix_c.a $out/lib/
-      cp rust.h linear.h common.h $out/include/
-    '';
+    installPhase = builtins.concatStringsSep "\n" installSteps;
   };
 
   # Blake3.lean C FFI dependency, needed for explicit static lib linking
diff --git a/ix_test/IxTest.lean b/ix_test/IxTest.lean
index 94be327c..795208bd 100644
--- a/ix_test/IxTest.lean
+++ b/ix_test/IxTest.lean
@@ -7,6 +7,4 @@ import Std
 def id' (A: Type) (x: A) := x
 --def ref (A: Type) (x y: A) := hello
 
---def one : Nat := 1
-
-
+def one : Nat := 1