From fb3d36584fe7f5155669ab3227fc5213b8f3c3e6 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 5 Dec 2024 18:59:14 -0800
Subject: [PATCH] chore: Add formatter, update lean4-nix

---
 flake.lock |   7 ++-
 flake.nix  | 157 ++++++++++++++++++++++++++++-------------------------
 2 files changed, 87 insertions(+), 77 deletions(-)

diff --git a/flake.lock b/flake.lock
index f40dde9..9f54bbe 100644
--- a/flake.lock
+++ b/flake.lock
@@ -42,15 +42,16 @@
         "nixpkgs": "nixpkgs"
       },
       "locked": {
-        "lastModified": 1731711316,
-        "narHash": "sha256-s5u+A2/Ea9gPveB5wwVM5dWW0NST6kamDsTeovGuLEs=",
+        "lastModified": 1733351931,
+        "narHash": "sha256-ngMjY/ci6490G2gofaS9CODtpnmFoYzfaI13U14TkFM=",
         "owner": "lenianiva",
         "repo": "lean4-nix",
-        "rev": "136fc6057c48de970579e960b62421e9c295b67d",
+        "rev": "157c85903f668fadeb79f330961b7bbe5ee596de",
         "type": "github"
       },
       "original": {
         "owner": "lenianiva",
+        "ref": "157c85903f668fadeb79f330961b7bbe5ee596de",
         "repo": "lean4-nix",
         "type": "github"
       }
diff --git a/flake.nix b/flake.nix
index 91901d8..d8ce698 100644
--- a/flake.nix
+++ b/flake.nix
@@ -4,7 +4,7 @@
   inputs = {
     nixpkgs.url = "github:nixos/nixpkgs/nixos-24.05";
     flake-parts.url = "github:hercules-ci/flake-parts";
-    lean4-nix.url = "github:lenianiva/lean4-nix";
+    lean4-nix.url = "github:lenianiva/lean4-nix?ref=157c85903f668fadeb79f330961b7bbe5ee596de";
     lspec = {
       url = "github:argumentcomputer/LSpec?ref=504a8cecf8da601b9466ac727aebb6b511aae4ab";
       flake = false;
@@ -18,80 +18,89 @@
     lean4-nix,
     lspec,
     ...
-  } : flake-parts.lib.mkFlake { inherit inputs; } {
-    flake = {
-    };
-    systems = [
-      "x86_64-linux"
-      "x86_64-darwin"
-    ];
-    perSystem = { system, pkgs, ... }: let
-      pkgs = import nixpkgs {
-        inherit system;
-        overlays = [ (lean4-nix.readToolchainFile ./lean-toolchain) ];
+  }:
+    flake-parts.lib.mkFlake {inherit inputs;} {
+      flake = {
       };
-      lspecLib = pkgs.lean.buildLeanPackage {
-        name = "LSpec";
-        roots = [ "Main" "LSpec" ];
-        src = "${lspec}";
-      };
-      project = pkgs.lean.buildLeanPackage {
-        name = "Pantograph";
-        roots = [ "Pantograph" ];
-        src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
-          src = ./.;
-          filter = path: type:
-            !(pkgs.lib.hasInfix "/Test/" path) &&
-            !(pkgs.lib.hasSuffix ".md" path) &&
-            !(pkgs.lib.hasSuffix "Repl.lean" path);
-        });
-      };
-      repl = pkgs.lean.buildLeanPackage {
-        name = "Repl";
-        roots = [ "Main" "Repl" ];
-        deps = [ project ];
-        src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
-          src = ./.;
-          filter = path: type:
-            !(pkgs.lib.hasInfix "/Test/" path) &&
-            !(pkgs.lib.hasSuffix ".md" path);
-        });
-      };
-      test = pkgs.lean.buildLeanPackage {
-        name = "Test";
-        # NOTE: The src directory must be ./. since that is where the import
-        # root begins (e.g. `import Test.Environment` and not `import
-        # Environment`) and thats where `lakefile.lean` resides.
-        roots = [ "Test.Main" ];
-        deps = [ lspecLib repl ];
-        src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
-          src = ./.;
-          filter = path: type:
-            !(pkgs.lib.hasInfix "Pantograph" path);
-        });
-      };
-    in rec {
-      packages = {
-        inherit (pkgs.lean) lean lean-all;
-        inherit (project) sharedLib iTree;
-        inherit (repl) executable;
-        default = repl.executable;
-      };
-      legacyPackages = {
-        inherit project;
-        leanPkgs = pkgs.lean;
-      };
-      checks = {
-        test = pkgs.runCommand "test" {
-          buildInputs = [ test.executable pkgs.lean.lean-all ];
-        } ''
-          #export LEAN_SRC_PATH="${./.}"
-          ${test.executable}/bin/test > $out
-        '';
-      };
-      devShells.default = pkgs.mkShell {
-        buildInputs = [ pkgs.lean.lean-all pkgs.lean.lean ];
+      systems = [
+        "aarch64-linux"
+        "aarch64-darwin"
+        "x86_64-linux"
+        "x86_64-darwin"
+      ];
+      perSystem = {
+        system,
+        pkgs,
+        ...
+      }: let
+        pkgs = import nixpkgs {
+          inherit system;
+          overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)];
+        };
+        lspecLib = pkgs.lean.buildLeanPackage {
+          name = "LSpec";
+          roots = ["Main" "LSpec"];
+          src = "${lspec}";
+        };
+        project = pkgs.lean.buildLeanPackage {
+          name = "Pantograph";
+          roots = ["Pantograph"];
+          src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
+            src = ./.;
+            filter = path: type:
+              !(pkgs.lib.hasInfix "/Test/" path)
+              && !(pkgs.lib.hasSuffix ".md" path)
+              && !(pkgs.lib.hasSuffix "Repl.lean" path);
+          });
+        };
+        repl = pkgs.lean.buildLeanPackage {
+          name = "Repl";
+          roots = ["Main" "Repl"];
+          deps = [project];
+          src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
+            src = ./.;
+            filter = path: type:
+              !(pkgs.lib.hasInfix "/Test/" path)
+              && !(pkgs.lib.hasSuffix ".md" path);
+          });
+        };
+        test = pkgs.lean.buildLeanPackage {
+          name = "Test";
+          # NOTE: The src directory must be ./. since that is where the import
+          # root begins (e.g. `import Test.Environment` and not `import
+          # Environment`) and thats where `lakefile.lean` resides.
+          roots = ["Test.Main"];
+          deps = [lspecLib repl];
+          src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
+            src = ./.;
+            filter = path: type:
+              !(pkgs.lib.hasInfix "Pantograph" path);
+          });
+        };
+      in rec {
+        packages = {
+          inherit (pkgs.lean) lean lean-all;
+          inherit (project) sharedLib iTree;
+          inherit (repl) executable;
+          default = repl.executable;
+        };
+        formatter = pkgs.alejandra;
+        legacyPackages = {
+          inherit project;
+          leanPkgs = pkgs.lean;
+        };
+        checks = {
+          test =
+            pkgs.runCommand "test" {
+              buildInputs = [test.executable pkgs.lean.lean-all];
+            } ''
+              #export LEAN_SRC_PATH="${./.}"
+              ${test.executable}/bin/test > $out
+            '';
+        };
+        devShells.default = pkgs.mkShell {
+          buildInputs = [pkgs.lean.lean-all pkgs.lean.lean];
+        };
       };
     };
-  };
 }