From d23f99fd44802ad688ba89b357a64cf8098345cc Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 14 Oct 2024 21:16:41 -0700 Subject: [PATCH 1/3] feat: Update Lean4 upstream to unofficial flake --- flake.lock | 98 +++++++++++++++++++++++++++--------------------------- flake.nix | 9 ++--- 2 files changed, 52 insertions(+), 55 deletions(-) diff --git a/flake.lock b/flake.lock index dc83369..5bd2d47 100644 --- a/flake.lock +++ b/flake.lock @@ -19,12 +19,15 @@ } }, "flake-utils": { + "inputs": { + "systems": "systems" + }, "locked": { - "lastModified": 1656928814, - "narHash": "sha256-RIFfgBuKz6Hp89yRr7+NR5tzIAbn52h8vT6vXkYjZoM=", + "lastModified": 1726560853, + "narHash": "sha256-X6rJYSESBVr3hBoH0WbKE5KvhPU5bloyZ2L4K60/fPQ=", "owner": "numtide", "repo": "flake-utils", - "rev": "7e2a3b3dfd9af950a856d66b0a7d01e3c18aa249", + "rev": "c1dfcf08411b08f6b8615f7d8971a2bfa81d5e8a", "type": "github" }, "original": { @@ -34,12 +37,7 @@ } }, "lean": { - "inputs": { - "flake-utils": "flake-utils", - "nixpkgs": "nixpkgs", - "nixpkgs-cadical": "nixpkgs-cadical", - "nixpkgs-old": "nixpkgs-old" - }, + "flake": false, "locked": { "lastModified": 1727749878, "narHash": "sha256-O2Egyh2D0TfQWzQKfHUeAh7qAjMfeLVwXwGUw5QqcvE=", @@ -55,6 +53,26 @@ "type": "github" } }, + "lean4-nix": { + "inputs": { + "flake-utils": "flake-utils", + "lean": "lean", + "nixpkgs": "nixpkgs" + }, + "locked": { + "lastModified": 1728965016, + "narHash": "sha256-DB1k6zpRp6KMuSQm/JcuyherqJ2n39CaGhfiEbA8VNI=", + "owner": "lenianiva", + "repo": "lean4-nix", + "rev": "e18ea1c5035e35db56e080ad4311a40fd1a75eea", + "type": "github" + }, + "original": { + "owner": "lenianiva", + "repo": "lean4-nix", + "type": "github" + } + }, "lspec": { "flake": false, "locked": { @@ -74,36 +92,20 @@ }, "nixpkgs": { "locked": { - "lastModified": 1686089707, - "narHash": "sha256-LTNlJcru2qJ0XhlhG9Acp5KyjB774Pza3tRH0pKIb3o=", - "owner": "NixOS", + "lastModified": 1728500571, + "narHash": "sha256-dOymOQ3AfNI4Z337yEwHGohrVQb4yPODCW9MDUyAc4w=", + "owner": "nixos", "repo": "nixpkgs", - "rev": "af21c31b2a1ec5d361ed8050edd0303c31306397", + "rev": "d51c28603def282a24fa034bcb007e2bcb5b5dd0", "type": "github" }, "original": { - "owner": "NixOS", - "ref": "nixpkgs-unstable", + "owner": "nixos", + "ref": "nixos-24.05", "repo": "nixpkgs", "type": "github" } }, - "nixpkgs-cadical": { - "locked": { - "lastModified": 1722221733, - "narHash": "sha256-sga9SrrPb+pQJxG1ttJfMPheZvDOxApFfwXCFO0H9xw=", - "owner": "NixOS", - "repo": "nixpkgs", - "rev": "12bf09802d77264e441f48e25459c10c93eada2e", - "type": "github" - }, - "original": { - "owner": "NixOS", - "repo": "nixpkgs", - "rev": "12bf09802d77264e441f48e25459c10c93eada2e", - "type": "github" - } - }, "nixpkgs-lib": { "locked": { "dir": "lib", @@ -122,23 +124,6 @@ "type": "github" } }, - "nixpkgs-old": { - "flake": false, - "locked": { - "lastModified": 1581379743, - "narHash": "sha256-i1XCn9rKuLjvCdu2UeXKzGLF6IuQePQKFt4hEKRU5oc=", - "owner": "NixOS", - "repo": "nixpkgs", - "rev": "34c7eb7545d155cc5b6f499b23a7cb1c96ab4d59", - "type": "github" - }, - "original": { - "owner": "NixOS", - "ref": "nixos-19.03", - "repo": "nixpkgs", - "type": "github" - } - }, "nixpkgs_2": { "locked": { "lastModified": 1711703276, @@ -158,10 +143,25 @@ "root": { "inputs": { "flake-parts": "flake-parts", - "lean": "lean", + "lean4-nix": "lean4-nix", "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 d4c903f..a573368 100644 --- a/flake.nix +++ b/flake.nix @@ -4,10 +4,7 @@ inputs = { nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable"; flake-parts.url = "github:hercules-ci/flake-parts"; - lean = { - # Do not follow input's nixpkgs since it could cause build failures - url = "github:leanprover/lean4?ref=v4.12.0"; - }; + lean4-nix.url = "github:lenianiva/lean4-nix"; lspec = { url = "github:argumentcomputer/LSpec?ref=504a8cecf8da601b9466ac727aebb6b511aae4ab"; flake = false; @@ -18,7 +15,7 @@ self, nixpkgs, flake-parts, - lean, + lean4-nix, lspec, ... } : flake-parts.lib.mkFlake { inherit inputs; } { @@ -29,7 +26,7 @@ "x86_64-darwin" ]; perSystem = { system, pkgs, ... }: let - leanPkgs = lean.packages.${system}.deprecated; + leanPkgs = lean4-nix.packages.${system}; lspecLib = leanPkgs.buildLeanPackage { name = "LSpec"; roots = [ "Main" "LSpec" ]; -- 2.44.1 From 23efed960b890ad2c8bc8e87ad30c6f539e05c40 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 26 Oct 2024 13:49:03 -0700 Subject: [PATCH 2/3] 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 ]; }; }; }; -- 2.44.1 From b99fecdb504ca6b4ea3bfb26674cd22a6b927906 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 26 Oct 2024 17:52:37 -0700 Subject: [PATCH 3/3] chore: Update `lean4-nix` --- flake.lock | 6 +++--- flake.nix | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/flake.lock b/flake.lock index 7617c3a..6bf8405 100644 --- a/flake.lock +++ b/flake.lock @@ -42,11 +42,11 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1729966280, - "narHash": "sha256-8G0n9POJW2zITB1m2h9+0GHA6lNlfsd2kssEqYLfK/U=", + "lastModified": 1729990097, + "narHash": "sha256-3RUciZy/VMbyp9v1f8oba/oQ8bWWVh2+1wsuUah3ryE=", "owner": "lenianiva", "repo": "lean4-nix", - "rev": "169dfe5e5db6038801ecfdbe4391cb14c5e8d454", + "rev": "6919763f186c7b0d39907203a649078ff3a4eb71", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index a2d0263..2c1a76e 100644 --- a/flake.nix +++ b/flake.nix @@ -28,7 +28,7 @@ perSystem = { system, pkgs, ... }: let pkgs = import nixpkgs { inherit system; - overlays = [ lean4-nix.tags."v4.12.0" ]; + overlays = [ (lean4-nix.readToolchainFile ./lean-toolchain) ]; }; lspecLib = pkgs.lean.buildLeanPackage { name = "LSpec"; -- 2.44.1