fix: Nix devShell & light refactor

.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"

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|

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
           ];
         };
       };

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

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