From 23efed960b890ad2c8bc8e87ad30c6f539e05c40 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 26 Oct 2024 13:49:03 -0700 Subject: [PATCH] chore: Update `lean4-nix` --- flake.lock | 103 ++++++++++++++++++++--------------------------------- flake.nix | 24 +++++++------ 2 files changed, 52 insertions(+), 75 deletions(-) diff --git a/flake.lock b/flake.lock index 5bd2d47..7617c3a 100644 --- a/flake.lock +++ b/flake.lock @@ -5,11 +5,11 @@ "nixpkgs-lib": "nixpkgs-lib" }, "locked": { - "lastModified": 1709336216, - "narHash": "sha256-Dt/wOWeW6Sqm11Yh+2+t0dfEWxoMxGBvv3JpIocFl9E=", + "lastModified": 1727826117, + "narHash": "sha256-K5ZLCyfO/Zj9mPFldf3iwS6oZStJcU4tSpiXTMYaaL0=", "owner": "hercules-ci", "repo": "flake-parts", - "rev": "f7b3c975cf067e56e7cda6cb098ebe3fb4d74ca2", + "rev": "3d04084d54bedc3d6b8b736c70ef449225c361b1", "type": "github" }, "original": { @@ -18,53 +18,35 @@ "type": "github" } }, - "flake-utils": { + "flake-parts_2": { "inputs": { - "systems": "systems" + "nixpkgs-lib": "nixpkgs-lib_2" }, "locked": { - "lastModified": 1726560853, - "narHash": "sha256-X6rJYSESBVr3hBoH0WbKE5KvhPU5bloyZ2L4K60/fPQ=", - "owner": "numtide", - "repo": "flake-utils", - "rev": "c1dfcf08411b08f6b8615f7d8971a2bfa81d5e8a", + "lastModified": 1727826117, + "narHash": "sha256-K5ZLCyfO/Zj9mPFldf3iwS6oZStJcU4tSpiXTMYaaL0=", + "owner": "hercules-ci", + "repo": "flake-parts", + "rev": "3d04084d54bedc3d6b8b736c70ef449225c361b1", "type": "github" }, "original": { - "owner": "numtide", - "repo": "flake-utils", - "type": "github" - } - }, - "lean": { - "flake": false, - "locked": { - "lastModified": 1727749878, - "narHash": "sha256-O2Egyh2D0TfQWzQKfHUeAh7qAjMfeLVwXwGUw5QqcvE=", - "owner": "leanprover", - "repo": "lean4", - "rev": "dc2533473114eb8656439ff2b9335209784aa640", - "type": "github" - }, - "original": { - "owner": "leanprover", - "ref": "v4.12.0", - "repo": "lean4", + "owner": "hercules-ci", + "repo": "flake-parts", "type": "github" } }, "lean4-nix": { "inputs": { - "flake-utils": "flake-utils", - "lean": "lean", + "flake-parts": "flake-parts_2", "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1728965016, - "narHash": "sha256-DB1k6zpRp6KMuSQm/JcuyherqJ2n39CaGhfiEbA8VNI=", + "lastModified": 1729966280, + "narHash": "sha256-8G0n9POJW2zITB1m2h9+0GHA6lNlfsd2kssEqYLfK/U=", "owner": "lenianiva", "repo": "lean4-nix", - "rev": "e18ea1c5035e35db56e080ad4311a40fd1a75eea", + "rev": "169dfe5e5db6038801ecfdbe4391cb14c5e8d454", "type": "github" }, "original": { @@ -108,34 +90,40 @@ }, "nixpkgs-lib": { "locked": { - "dir": "lib", - "lastModified": 1709237383, - "narHash": "sha256-cy6ArO4k5qTx+l5o+0mL9f5fa86tYUX3ozE1S+Txlds=", - "owner": "NixOS", - "repo": "nixpkgs", - "rev": "1536926ef5621b09bba54035ae2bb6d806d72ac8", - "type": "github" + "lastModified": 1727825735, + "narHash": "sha256-0xHYkMkeLVQAMa7gvkddbPqpxph+hDzdu1XdGPJR+Os=", + "type": "tarball", + "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz" }, "original": { - "dir": "lib", - "owner": "NixOS", - "ref": "nixos-unstable", - "repo": "nixpkgs", - "type": "github" + "type": "tarball", + "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz" + } + }, + "nixpkgs-lib_2": { + "locked": { + "lastModified": 1727825735, + "narHash": "sha256-0xHYkMkeLVQAMa7gvkddbPqpxph+hDzdu1XdGPJR+Os=", + "type": "tarball", + "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz" + }, + "original": { + "type": "tarball", + "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz" } }, "nixpkgs_2": { "locked": { - "lastModified": 1711703276, - "narHash": "sha256-iMUFArF0WCatKK6RzfUJknjem0H9m4KgorO/p3Dopkk=", + "lastModified": 1729691686, + "narHash": "sha256-BAuPWW+9fa1moZTU+jFh+1cUtmsuF8asgzFwejM4wac=", "owner": "nixos", "repo": "nixpkgs", - "rev": "d8fe5e6c92d0d190646fb9f1056741a229980089", + "rev": "32e940c7c420600ef0d1ef396dc63b04ee9cad37", "type": "github" }, "original": { "owner": "nixos", - "ref": "nixos-unstable", + "ref": "nixos-24.05", "repo": "nixpkgs", "type": "github" } @@ -147,21 +135,6 @@ "lspec": "lspec", "nixpkgs": "nixpkgs_2" } - }, - "systems": { - "locked": { - "lastModified": 1681028828, - "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", - "owner": "nix-systems", - "repo": "default", - "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", - "type": "github" - }, - "original": { - "owner": "nix-systems", - "repo": "default", - "type": "github" - } } }, "root": "root", diff --git a/flake.nix b/flake.nix index a573368..a2d0263 100644 --- a/flake.nix +++ b/flake.nix @@ -2,7 +2,7 @@ description = "Pantograph"; inputs = { - nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable"; + nixpkgs.url = "github:nixos/nixpkgs/nixos-24.05"; flake-parts.url = "github:hercules-ci/flake-parts"; lean4-nix.url = "github:lenianiva/lean4-nix"; lspec = { @@ -26,13 +26,16 @@ "x86_64-darwin" ]; perSystem = { system, pkgs, ... }: let - leanPkgs = lean4-nix.packages.${system}; - lspecLib = leanPkgs.buildLeanPackage { + pkgs = import nixpkgs { + inherit system; + overlays = [ lean4-nix.tags."v4.12.0" ]; + }; + lspecLib = pkgs.lean.buildLeanPackage { name = "LSpec"; roots = [ "Main" "LSpec" ]; src = "${lspec}"; }; - project = leanPkgs.buildLeanPackage { + project = pkgs.lean.buildLeanPackage { name = "Pantograph"; roots = [ "Pantograph" ]; src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith { @@ -43,7 +46,7 @@ !(pkgs.lib.hasSuffix "Repl.lean" path); }); }; - repl = leanPkgs.buildLeanPackage { + repl = pkgs.lean.buildLeanPackage { name = "Repl"; roots = [ "Main" "Repl" ]; deps = [ project ]; @@ -54,7 +57,7 @@ !(pkgs.lib.hasSuffix ".md" path); }); }; - test = leanPkgs.buildLeanPackage { + 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 @@ -69,24 +72,25 @@ }; in rec { packages = { - inherit (leanPkgs) lean lean-all; + inherit (pkgs.lean) lean lean-all; inherit (project) sharedLib; inherit (repl) executable; default = repl.executable; }; legacyPackages = { - inherit project leanPkgs; + inherit project; + leanPkgs = pkgs.lean; }; checks = { test = pkgs.runCommand "test" { - buildInputs = [ test.executable leanPkgs.lean-all ]; + buildInputs = [ test.executable pkgs.lean.lean-all ]; } '' #export LEAN_SRC_PATH="${./.}" ${test.executable}/bin/test > $out ''; }; devShells.default = pkgs.mkShell { - buildInputs = [ leanPkgs.lean-all leanPkgs.lean ]; + buildInputs = [ pkgs.lean.lean-all pkgs.lean.lean ]; }; }; };