leanPackages: 4.29.1 -> 4.30.0
Add leangz (leantar) as a new build and runtime dependency. https://github.com/leanprover/lean4/releases/tag/v4.30.0 https://github.com/leanprover-community/mathlib4/blob/v4.30.0/lake-manifest.json
This commit is contained in:
@@ -7,13 +7,13 @@
|
||||
buildLakePackage (finalAttrs: {
|
||||
pname = "lean4-cli";
|
||||
# nixpkgs-update: no auto update
|
||||
version = "4.29.0";
|
||||
version = "4.30.0";
|
||||
|
||||
src = fetchFromGitHub {
|
||||
owner = "leanprover";
|
||||
repo = "lean4-cli";
|
||||
tag = "v${finalAttrs.version}";
|
||||
hash = "sha256-jCUl4sXVmwtYPuQecEUFH6mwFzPaQY7au4624EOiWjk=";
|
||||
hash = "sha256-oMaqHvWlEfk1601JfNKPvkGIWgMW6tiF7Mej7g63vh0=";
|
||||
};
|
||||
|
||||
leanPackageName = "Cli";
|
||||
|
||||
@@ -7,13 +7,13 @@
|
||||
buildLakePackage {
|
||||
pname = "lean4-Qq";
|
||||
# nixpkgs-update: no auto update
|
||||
version = "4.29.0-unstable-2026-03-28";
|
||||
version = "4.30.0";
|
||||
|
||||
src = fetchFromGitHub {
|
||||
owner = "leanprover-community";
|
||||
repo = "quote4";
|
||||
rev = "707efb56d0696634e9e965523a1bbe9ac6ce141d";
|
||||
hash = "sha256-pNY5hv1nJbreCfU4EewIHCpiryIBv1ghWibrUW8vnQ0=";
|
||||
tag = "v4.30.0";
|
||||
hash = "sha256-jVsRw/R7D7HmsE7vQvVeDXcnVerlcDBOrhf9FJJiXkY=";
|
||||
};
|
||||
|
||||
leanPackageName = "Qq";
|
||||
|
||||
@@ -8,13 +8,13 @@
|
||||
buildLakePackage {
|
||||
pname = "lean4-aesop";
|
||||
# nixpkgs-update: no auto update
|
||||
version = "4.29.0-unstable-2026-03-28";
|
||||
version = "4.30.0";
|
||||
|
||||
src = fetchFromGitHub {
|
||||
owner = "leanprover-community";
|
||||
repo = "aesop";
|
||||
rev = "7152850e7b216a0d409701617721b6e469d34bf6";
|
||||
hash = "sha256-CNwxNig8OWjtfQRYyRnM/HGBn2oaNX5qP9CVT2eWNlg=";
|
||||
tag = "v4.30.0";
|
||||
hash = "sha256-7PhQVMdiYImuzRYdf0Kgw3JYS4nBLfILXxyhFH8Zag0=";
|
||||
};
|
||||
|
||||
leanPackageName = "aesop";
|
||||
|
||||
@@ -7,13 +7,13 @@
|
||||
buildLakePackage {
|
||||
pname = "lean4-batteries";
|
||||
# nixpkgs-update: no auto update
|
||||
version = "4.29.0-unstable-2026-03-27";
|
||||
version = "4.30.0-unstable-2026-05-26";
|
||||
|
||||
src = fetchFromGitHub {
|
||||
owner = "leanprover-community";
|
||||
repo = "batteries";
|
||||
rev = "756e3321fd3b02a85ffda19fef789916223e578c";
|
||||
hash = "sha256-sEIDi2i2FaLTgKYWt/kzqPrjMdf+bFURfhw6ZZWBawQ=";
|
||||
rev = "32dc18cde3684679f3c003de608743b57498c56f";
|
||||
hash = "sha256-OOcKCQEgnn9zkkwjHOovMb/IprNomTDufLOfEXs7hFU=";
|
||||
};
|
||||
|
||||
leanPackageName = "batteries";
|
||||
|
||||
@@ -8,13 +8,13 @@
|
||||
buildLakePackage {
|
||||
pname = "lean4-importGraph";
|
||||
# nixpkgs-update: no auto update
|
||||
version = "4.29.0-unstable-2026-03-28";
|
||||
version = "4.30.0-unstable-2026-05-26";
|
||||
|
||||
src = fetchFromGitHub {
|
||||
owner = "leanprover-community";
|
||||
repo = "import-graph";
|
||||
rev = "48d5698bc464786347c1b0d859b18f938420f060";
|
||||
hash = "sha256-tqdO2qyWiJzEbK0yuu4+tiOXTEg9XJfGnI7z6Jh/abg=";
|
||||
rev = "515cf9d0c00ece5e661f6de4326a53dedc1e8ea1";
|
||||
hash = "sha256-V3bGQxTNs2G4MqaVxRb6WED1a7VaHfEo1HgBNqPipz8=";
|
||||
};
|
||||
|
||||
leanPackageName = "importGraph";
|
||||
|
||||
@@ -9,6 +9,7 @@
|
||||
gmp,
|
||||
cadical,
|
||||
cadical' ? cadical.override { version = "2.1.3"; },
|
||||
leangz,
|
||||
pkg-config,
|
||||
libuv,
|
||||
perl,
|
||||
@@ -20,7 +21,7 @@
|
||||
let
|
||||
lean4 = stdenv.mkDerivation (finalAttrs: {
|
||||
pname = "lean4";
|
||||
version = "4.29.1";
|
||||
version = "4.30.0";
|
||||
|
||||
mimalloc-src = fetchFromGitHub {
|
||||
owner = "microsoft";
|
||||
@@ -33,7 +34,7 @@ let
|
||||
owner = "leanprover";
|
||||
repo = "lean4";
|
||||
tag = "v${finalAttrs.version}";
|
||||
hash = "sha256-pdhRPjSic2H8zPJXLmyfN8umKDoafjmSo4OQSRxIbyE=";
|
||||
hash = "sha256-YTsfIppd6km7wOjAxRH5KMPsW++ztFDCJT2up72J86Q=";
|
||||
};
|
||||
|
||||
# Vendor mimalloc. Upstream has since partially adopted FetchContent:
|
||||
@@ -72,6 +73,7 @@ let
|
||||
|
||||
nativeBuildInputs = [
|
||||
cmake
|
||||
leangz
|
||||
pkg-config
|
||||
];
|
||||
|
||||
@@ -90,6 +92,7 @@ let
|
||||
"-DUSE_GITHASH=OFF"
|
||||
"-DINSTALL_LICENSE=OFF"
|
||||
"-DINSTALL_CADICAL=OFF"
|
||||
"-DINSTALL_LEANTAR=OFF"
|
||||
"-DUSE_MIMALLOC=ON"
|
||||
];
|
||||
|
||||
@@ -119,6 +122,7 @@ let
|
||||
paths = [
|
||||
lean4
|
||||
cadical'
|
||||
leangz
|
||||
];
|
||||
nativeBuildInputs = [ perl ];
|
||||
postBuild = ''
|
||||
|
||||
@@ -18,13 +18,13 @@ let
|
||||
mathlib__archive = buildLakePackage (finalAttrs: {
|
||||
pname = "lean4-mathlib";
|
||||
# nixpkgs-update: no auto update
|
||||
version = "4.29.1";
|
||||
version = "4.30.0";
|
||||
|
||||
src = fetchFromGitHub {
|
||||
owner = "leanprover-community";
|
||||
repo = "mathlib4";
|
||||
tag = "v${finalAttrs.version}";
|
||||
hash = "sha256-K/QPTOytsV+OX25xyKlspeB9G0a28IjmJxcUAKXFP9U=";
|
||||
hash = "sha256-RxOxdUiVUAxUbfVhxlkjmPX1V64EtmIIn1eW75TiJWA=";
|
||||
};
|
||||
|
||||
leanPackageName = "mathlib";
|
||||
|
||||
@@ -7,13 +7,13 @@
|
||||
buildLakePackage {
|
||||
pname = "lean4-plausible";
|
||||
# nixpkgs-update: no auto update
|
||||
version = "4.29.0-unstable-2026-03-28";
|
||||
version = "4.30.0-unstable-2026-05-26";
|
||||
|
||||
src = fetchFromGitHub {
|
||||
owner = "leanprover-community";
|
||||
repo = "plausible";
|
||||
rev = "83e90935a17ca19ebe4b7893c7f7066e266f50d3";
|
||||
hash = "sha256-08fNB2GK5AqDJ15n5Ol+HYqaSbsznyp4cerDo32bG50=";
|
||||
rev = "a456461b368b71d2accd95234832cd9c174b5437";
|
||||
hash = "sha256-DSaS0W2cfCUh2N+7WyiM7aUv3trtRNON0PzCgCW2SKY=";
|
||||
};
|
||||
|
||||
leanPackageName = "plausible";
|
||||
|
||||
@@ -10,13 +10,13 @@
|
||||
buildLakePackage (finalAttrs: {
|
||||
pname = "lean4-proofwidgets";
|
||||
# nixpkgs-update: no auto update
|
||||
version = "0.0.95+lean-v4.29.1";
|
||||
version = "0.0.99";
|
||||
|
||||
src = fetchFromGitHub {
|
||||
owner = "leanprover-community";
|
||||
repo = "ProofWidgets4";
|
||||
tag = "v${finalAttrs.version}";
|
||||
hash = "sha256-D1fTsV8W29S1C53ky66sFgIoA5cLx/ilKa98czScV+s=";
|
||||
hash = "sha256-kGoEkKGrucNUWFYkHW2LsS1gI4C0J8bAHQL2MiE4Pzc=";
|
||||
};
|
||||
|
||||
leanPackageName = "proofwidgets";
|
||||
@@ -32,7 +32,7 @@ buildLakePackage (finalAttrs: {
|
||||
name = "lean4-proofwidgets-npm-deps";
|
||||
src = finalAttrs.src;
|
||||
sourceRoot = "source/widget";
|
||||
hash = "sha256-ShH6MDr76wzWQrJvhMWCnklaox/uRsfoe+aYVSo/eNA=";
|
||||
hash = "sha256-ssWSr2qfsIbX25DidiVPm0tsLGjrhQhQ6YKPL0rfc1k=";
|
||||
};
|
||||
npmRoot = "widget";
|
||||
|
||||
|
||||
Reference in New Issue
Block a user