gador/nixpkgs
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

leanPackages: partially revert https://github.com/NixOS/nixpkgs/pull/526718/commits/a26b66330f6fa572e7005ee2a1eb031093456e6e

Browse Source 
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.
This commit is contained in:
Nadja Yang
2026-06-04 16:48:52 -04:00
parent 49b3a82b8b
commit 590ccdb420
10 changed files with 35 additions and 78 deletions
Download Patch File Download Diff File Expand all files Collapse all files
pkgs/development/lean-modules/Cli/default.nix
+4 -7
View File
@@ -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 ];
};
}
pkgs/development/lean-modules/LeanSearchClient/default.nix
+1 -4
View File
@@ -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 ];
};
}
pkgs/development/lean-modules/Qq/default.nix
+4 -7
View File
@@ -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 ];
};
}
pkgs/development/lean-modules/aesop/default.nix
+4 -7
View File
@@ -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 ];
};
}
pkgs/development/lean-modules/batteries/default.nix
+4 -17
View File
@@ -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 ];
};
}
pkgs/development/lean-modules/importGraph/default.nix
+4 -7
View File
@@ -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 ];
};
}
pkgs/development/lean-modules/lean4/default.nix
+5 -11
View File
@@ -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";
};
});
pkgs/development/lean-modules/mathlib/default.nix
+4 -7
View File
@@ -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 ];
};
}
pkgs/development/lean-modules/plausible/default.nix
+4 -7
View File
@@ -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 ];
};
}
pkgs/development/lean-modules/proofwidgets/default.nix
+1 -4
View File
@@ -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 ];
};
}