From 590ccdb420036ed0ab6bffde991b13f98ec0fe14 Mon Sep 17 00:00:00 2001 From: Nadja Yang Date: Wed, 3 Jun 2026 14:01:07 -0400 Subject: [PATCH] leanPackages: partially revert https://github.com/NixOS/nixpkgs/pull/526718/commits/a26b66330f6fa572e7005ee2a1eb031093456e6e In favor of https://github.com/NixOS/nixpkgs/pull/511524 (https://github.com/NixOS/nixpkgs/pull/511524/commits/72b8bcfd8ef837cfddc1cacc0bd4c7b8b3998e59). Retains pkgs.lean4 at 4.30.0. --- pkgs/development/lean-modules/Cli/default.nix | 11 ++++------ .../lean-modules/LeanSearchClient/default.nix | 5 +---- pkgs/development/lean-modules/Qq/default.nix | 11 ++++------ .../lean-modules/aesop/default.nix | 11 ++++------ .../lean-modules/batteries/default.nix | 21 ++++--------------- .../lean-modules/importGraph/default.nix | 11 ++++------ .../lean-modules/lean4/default.nix | 16 +++++--------- .../lean-modules/mathlib/default.nix | 11 ++++------ .../lean-modules/plausible/default.nix | 11 ++++------ .../lean-modules/proofwidgets/default.nix | 5 +---- 10 files changed, 35 insertions(+), 78 deletions(-) diff --git a/pkgs/development/lean-modules/Cli/default.nix b/pkgs/development/lean-modules/Cli/default.nix index 07476219fea2..d3bc495ee9cf 100644 --- a/pkgs/development/lean-modules/Cli/default.nix +++ b/pkgs/development/lean-modules/Cli/default.nix @@ -6,13 +6,13 @@ buildLakePackage { pname = "lean4-cli"; - version = "4.30.0"; + version = "4.29.0"; src = fetchFromGitHub { owner = "leanprover"; repo = "lean4-cli"; - tag = "v4.30.0"; - hash = "sha256-oMaqHvWlEfk1601JfNKPvkGIWgMW6tiF7Mej7g63vh0="; + tag = "v4.29.0"; + hash = "sha256-jCUl4sXVmwtYPuQecEUFH6mwFzPaQY7au4624EOiWjk="; }; leanPackageName = "Cli"; @@ -31,9 +31,6 @@ buildLakePackage { description = "Command-line argument parser for Lean 4"; homepage = "https://github.com/leanprover/lean4-cli"; license = lib.licenses.mit; - maintainers = with lib.maintainers; [ - nadja-y - niklashh - ]; + maintainers = with lib.maintainers; [ nadja-y ]; }; } diff --git a/pkgs/development/lean-modules/LeanSearchClient/default.nix b/pkgs/development/lean-modules/LeanSearchClient/default.nix index da6eaf0263d0..b7e25b5ecbd0 100644 --- a/pkgs/development/lean-modules/LeanSearchClient/default.nix +++ b/pkgs/development/lean-modules/LeanSearchClient/default.nix @@ -22,9 +22,6 @@ buildLakePackage { description = "Lean 4 client for LeanSearch and Moogle proof search"; homepage = "https://github.com/leanprover-community/LeanSearchClient"; license = lib.licenses.asl20; - maintainers = with lib.maintainers; [ - nadja-y - niklashh - ]; + maintainers = with lib.maintainers; [ nadja-y ]; }; } diff --git a/pkgs/development/lean-modules/Qq/default.nix b/pkgs/development/lean-modules/Qq/default.nix index a91693775347..6feb6fa51916 100644 --- a/pkgs/development/lean-modules/Qq/default.nix +++ b/pkgs/development/lean-modules/Qq/default.nix @@ -6,13 +6,13 @@ buildLakePackage { pname = "lean4-Qq"; - version = "4.30.0"; + version = "4.29.0"; src = fetchFromGitHub { owner = "leanprover-community"; repo = "quote4"; - tag = "v4.30.0"; - hash = "sha256-jVsRw/R7D7HmsE7vQvVeDXcnVerlcDBOrhf9FJJiXkY="; + tag = "v4.29.0"; + hash = "sha256-pNY5hv1nJbreCfU4EewIHCpiryIBv1ghWibrUW8vnQ0="; }; leanPackageName = "Qq"; @@ -21,9 +21,6 @@ buildLakePackage { description = "Lean 4 compile-time quote and antiquote macros for metaprogramming"; homepage = "https://github.com/leanprover-community/quote4"; license = lib.licenses.asl20; - maintainers = with lib.maintainers; [ - nadja-y - niklashh - ]; + maintainers = with lib.maintainers; [ nadja-y ]; }; } diff --git a/pkgs/development/lean-modules/aesop/default.nix b/pkgs/development/lean-modules/aesop/default.nix index f71d9e7c9f47..7d8ad308741a 100644 --- a/pkgs/development/lean-modules/aesop/default.nix +++ b/pkgs/development/lean-modules/aesop/default.nix @@ -7,13 +7,13 @@ buildLakePackage { pname = "lean4-aesop"; - version = "4.30.0"; + version = "4.29.0"; src = fetchFromGitHub { owner = "leanprover-community"; repo = "aesop"; - tag = "v4.30.0"; - hash = "sha256-7PhQVMdiYImuzRYdf0Kgw3JYS4nBLfILXxyhFH8Zag0="; + tag = "v4.29.0"; + hash = "sha256-CNwxNig8OWjtfQRYyRnM/HGBn2oaNX5qP9CVT2eWNlg="; }; leanPackageName = "aesop"; @@ -23,9 +23,6 @@ buildLakePackage { description = "White-box automation for Lean 4"; homepage = "https://github.com/leanprover-community/aesop"; license = lib.licenses.asl20; - maintainers = with lib.maintainers; [ - nadja-y - niklashh - ]; + maintainers = with lib.maintainers; [ nadja-y ]; }; } diff --git a/pkgs/development/lean-modules/batteries/default.nix b/pkgs/development/lean-modules/batteries/default.nix index 3e06e945f9fa..9fdb1efd8686 100644 --- a/pkgs/development/lean-modules/batteries/default.nix +++ b/pkgs/development/lean-modules/batteries/default.nix @@ -6,34 +6,21 @@ buildLakePackage { pname = "lean4-batteries"; - version = "4.30.0"; + version = "4.29.0"; src = fetchFromGitHub { owner = "leanprover-community"; repo = "batteries"; - tag = "v4.30.0"; - hash = "sha256-OOcKCQEgnn9zkkwjHOovMb/IprNomTDufLOfEXs7hFU="; + tag = "v4.29.0"; + hash = "sha256-sEIDi2i2FaLTgKYWt/kzqPrjMdf+bFURfhw6ZZWBawQ="; }; leanPackageName = "batteries"; - # Pre-build static library for downstream executables. - # TODO: upstream this to batteries - postPatch = '' - substituteInPlace lakefile.toml \ - --replace-fail '[[lean_lib]] - name = "Batteries"' '[[lean_lib]] - name = "Batteries" - defaultFacets = ["static"]' - ''; - meta = { description = "The batteries-included extended library for Lean 4"; homepage = "https://github.com/leanprover-community/batteries"; license = lib.licenses.asl20; - maintainers = with lib.maintainers; [ - nadja-y - niklashh - ]; + maintainers = with lib.maintainers; [ nadja-y ]; }; } diff --git a/pkgs/development/lean-modules/importGraph/default.nix b/pkgs/development/lean-modules/importGraph/default.nix index 6692a5f99ec2..4da481fd5a16 100644 --- a/pkgs/development/lean-modules/importGraph/default.nix +++ b/pkgs/development/lean-modules/importGraph/default.nix @@ -7,13 +7,13 @@ buildLakePackage { pname = "lean4-importGraph"; - version = "4.30.0"; + version = "4.29.0"; src = fetchFromGitHub { owner = "leanprover-community"; repo = "import-graph"; - tag = "v4.30.0"; - hash = "sha256-V3bGQxTNs2G4MqaVxRb6WED1a7VaHfEo1HgBNqPipz8="; + tag = "v4.29.0"; + hash = "sha256-tqdO2qyWiJzEbK0yuu4+tiOXTEg9XJfGnI7z6Jh/abg="; }; leanPackageName = "importGraph"; @@ -23,9 +23,6 @@ buildLakePackage { description = "Tools to analyse and visualise Lean 4 import structures"; homepage = "https://github.com/leanprover-community/import-graph"; license = lib.licenses.asl20; - maintainers = with lib.maintainers; [ - nadja-y - niklashh - ]; + maintainers = with lib.maintainers; [ nadja-y ]; }; } diff --git a/pkgs/development/lean-modules/lean4/default.nix b/pkgs/development/lean-modules/lean4/default.nix index 2e1c9b2f3c02..7ba6dd5170f4 100644 --- a/pkgs/development/lean-modules/lean4/default.nix +++ b/pkgs/development/lean-modules/lean4/default.nix @@ -8,18 +8,16 @@ git, gmp, cadical, - leangz, pkg-config, libuv, perl, testers, }: -let - cadical' = cadical.override { version = "2.1.3"; }; +let lean4 = stdenv.mkDerivation (finalAttrs: { pname = "lean4"; - version = "4.30.0"; + version = "4.29.0"; mimalloc-src = fetchFromGitHub { owner = "microsoft"; @@ -32,7 +30,7 @@ let owner = "leanprover"; repo = "lean4"; tag = "v${finalAttrs.version}"; - hash = "sha256-YTsfIppd6km7wOjAxRH5KMPsW++ztFDCJT2up72J86Q="; + hash = "sha256-0v4OTrCLdHBbWJUq7hIjJonqget9SvsG3izGlOwhwyU="; }; # Vendor mimalloc. Upstream has since partially adopted FetchContent: @@ -72,13 +70,12 @@ let nativeBuildInputs = [ cmake pkg-config - leangz # Provides leantar ]; buildInputs = [ gmp libuv - cadical' + cadical ]; nativeCheckInputs = [ @@ -106,10 +103,7 @@ let changelog = "https://github.com/leanprover/lean4/blob/${finalAttrs.src.tag}/RELEASES.md"; license = lib.licenses.asl20; platforms = lib.platforms.all; - maintainers = with lib.maintainers; [ - nadja-y - niklashh - ]; + maintainers = with lib.maintainers; [ nadja-y ]; mainProgram = "lean"; }; }); diff --git a/pkgs/development/lean-modules/mathlib/default.nix b/pkgs/development/lean-modules/mathlib/default.nix index 60ae77331f02..70a34dd9f333 100644 --- a/pkgs/development/lean-modules/mathlib/default.nix +++ b/pkgs/development/lean-modules/mathlib/default.nix @@ -14,13 +14,13 @@ buildLakePackage { pname = "lean4-mathlib"; - version = "4.30.0"; + version = "4.29.0"; src = fetchFromGitHub { owner = "leanprover-community"; repo = "mathlib4"; - tag = "v4.30.0"; - hash = "sha256-RxOxdUiVUAxUbfVhxlkjmPX1V64EtmIIn1eW75TiJWA="; + tag = "v4.29.0"; + hash = "sha256-fe+qS7gNxdLnACX3/jqToa9m7r1gbskY6kDJbm1ZefE="; }; leanPackageName = "mathlib"; @@ -44,9 +44,6 @@ buildLakePackage { description = "Mathematical library for Lean 4"; homepage = "https://github.com/leanprover-community/mathlib4"; license = lib.licenses.asl20; - maintainers = with lib.maintainers; [ - nadja-y - niklashh - ]; + maintainers = with lib.maintainers; [ nadja-y ]; }; } diff --git a/pkgs/development/lean-modules/plausible/default.nix b/pkgs/development/lean-modules/plausible/default.nix index 6f4d08d0ee28..07b22b3ebe87 100644 --- a/pkgs/development/lean-modules/plausible/default.nix +++ b/pkgs/development/lean-modules/plausible/default.nix @@ -6,13 +6,13 @@ buildLakePackage { pname = "lean4-plausible"; - version = "4.30.0"; + version = "4.29.0"; src = fetchFromGitHub { owner = "leanprover-community"; repo = "plausible"; - tag = "v4.30.0"; - hash = "sha256-DSaS0W2cfCUh2N+7WyiM7aUv3trtRNON0PzCgCW2SKY="; + tag = "v4.29.0"; + hash = "sha256-08fNB2GK5AqDJ15n5Ol+HYqaSbsznyp4cerDo32bG50="; }; leanPackageName = "plausible"; @@ -21,9 +21,6 @@ buildLakePackage { description = "Property-based testing framework for Lean 4"; homepage = "https://github.com/leanprover-community/plausible"; license = lib.licenses.asl20; - maintainers = with lib.maintainers; [ - nadja-y - niklashh - ]; + maintainers = with lib.maintainers; [ nadja-y ]; }; } diff --git a/pkgs/development/lean-modules/proofwidgets/default.nix b/pkgs/development/lean-modules/proofwidgets/default.nix index 3a2793272012..54998125b500 100644 --- a/pkgs/development/lean-modules/proofwidgets/default.nix +++ b/pkgs/development/lean-modules/proofwidgets/default.nix @@ -62,9 +62,6 @@ buildLakePackage { description = "Interactive UI framework for Lean 4 proof assistants"; homepage = "https://github.com/leanprover-community/ProofWidgets4"; license = lib.licenses.asl20; - maintainers = with lib.maintainers; [ - nadja-y - niklashh - ]; + maintainers = with lib.maintainers; [ nadja-y ]; }; }