From d1a18a3b1562e7f6a45e972ffe612d088a2979ee Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Mon, 20 Oct 2025 11:00:14 -0400
Subject: [PATCH] chore: Use pre-built Lean binary in Nix build

---
 .github/workflows/ci.yml | 11 -----------
 flake.lock               | 12 ++++++------
 flake.nix                | 21 ++++++---------------
 3 files changed, 12 insertions(+), 32 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 3755179..41dd32f 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -19,14 +19,3 @@ jobs:
       - uses: leanprover/lean-action@v1
         with:
           build-args: "--wfail"
-
-  nix:
-    name: Nix Flake Check
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v5
-      - uses: cachix/install-nix-action@v31
-        with:
-          nix_path: nixpkgs=channel:nixos-unstable
-          github_access_token: ${{ secrets.GITHUB_TOKEN }}
-      - run: nix build --accept-flake-config
diff --git a/flake.lock b/flake.lock
index 387f8af..bee047c 100644
--- a/flake.lock
+++ b/flake.lock
@@ -5,11 +5,11 @@
         "nixpkgs-lib": "nixpkgs-lib"
       },
       "locked": {
-        "lastModified": 1756770412,
-        "narHash": "sha256-+uWLQZccFHwqpGqr2Yt5VsW/PbeJVTn9Dk6SHWhNRPw=",
+        "lastModified": 1760948891,
+        "narHash": "sha256-TmWcdiUUaWk8J4lpjzu4gCGxWY6/Ok7mOK4fIFfBuU4=",
         "owner": "hercules-ci",
         "repo": "flake-parts",
-        "rev": "4524271976b625a4a605beefd893f270620fd751",
+        "rev": "864599284fc7c0ba6357ed89ed5e2cd5040f0c04",
         "type": "github"
       },
       "original": {
@@ -42,11 +42,11 @@
         "nixpkgs": "nixpkgs"
       },
       "locked": {
-        "lastModified": 1758037834,
-        "narHash": "sha256-P2rBelR9lgFJPE8kEV1wwX1LHK6xWlVcQqEez84ss6E=",
+        "lastModified": 1760753731,
+        "narHash": "sha256-RJCrWSH1Iz8WPVL2hB2U/kBXuct4+tKo/aiPCaOYPzM=",
         "owner": "lenianiva",
         "repo": "lean4-nix",
-        "rev": "d87ff09bad00ca4addd471a68a968f2aa29c7c36",
+        "rev": "ae7abc9f97a26da2ecf5233b9edfe3ba0af1b9a9",
         "type": "github"
       },
       "original": {
diff --git a/flake.nix b/flake.nix
index 514d5d0..c6e2690 100644
--- a/flake.nix
+++ b/flake.nix
@@ -1,15 +1,6 @@
 {
   description = "LSpec Nix Flake";
 
-  nixConfig = {
-    extra-substituters = [
-      "https://cache.garnix.io"
-    ];
-    extra-trusted-public-keys = [
-      "cache.garnix.io:CTFPyKSLcx5RMJKfLo5EEPUObbA78b0YQ2DTCJXqr9g="
-    ];
-  };
-
   inputs = {
     nixpkgs.follows = "lean4-nix/nixpkgs";
     flake-parts.url = "github:hercules-ci/flake-parts";
@@ -36,22 +27,22 @@
         self',
         config,
         ...
-      }:
-      {
+      }: {
         _module.args.pkgs = import nixpkgs {
           inherit system;
           overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)];
         };
 
         # Build the library with `nix build`
-        packages.default = ((lean4-nix.lake {inherit pkgs;}).mkPackage {
+        packages.default =
+          ((lean4-nix.lake {inherit pkgs;}).mkPackage {
             src = ./.;
             roots = ["LSpec"];
-        }).modRoot;
+          }).modRoot;
 
         devShells.default = pkgs.mkShell {
-          packages = with pkgs.lean; [lean lean-all];
+          packages = with pkgs.lean; [lean];
         };
+      };
     };
-  };
 }