lean4: update leanPackages and lean4 4.29.0/1 -> 4.30.0 (#526718)

pkgs/by-name/le/lean4/package.nix

@@ -6,6 +6,7 @@
   git,
   gmp,
   cadical,
+  leangz,
   makeWrapper,
   pkg-config,
   libuv,
@@ -13,13 +14,12 @@
   perl,
   testers,
 }:
-
 let
   cadical' = cadical.override { version = "2.1.3"; };
 in
 stdenv.mkDerivation (finalAttrs: {
   pname = "lean4";
-  version = "4.29.1";
+  version = "4.30.0";
 
   # Using a vendored version rather than nixpkgs' version to match the exact version required by
   # Lean.  Apparently, even a slight version change can impact greatly the final performance.
@@ -34,7 +34,7 @@ stdenv.mkDerivation (finalAttrs: {
     owner = "leanprover";
     repo = "lean4";
     tag = "v${finalAttrs.version}";
-    hash = "sha256-pdhRPjSic2H8zPJXLmyfN8umKDoafjmSo4OQSRxIbyE=";
+    hash = "sha256-YTsfIppd6km7wOjAxRH5KMPsW++ztFDCJT2up72J86Q=";
   };
 
   postPatch =
@@ -66,6 +66,7 @@ stdenv.mkDerivation (finalAttrs: {
     cmake
     pkg-config
     makeWrapper
+    leangz # Provides leantar
   ];
 
   buildInputs = [
@@ -110,6 +111,7 @@ stdenv.mkDerivation (finalAttrs: {
       danielbritten
       jthulhu
       nadja-y
+      niklashh
     ];
     mainProgram = "lean";
   };

pkgs/by-name/le/leangz/package.nix

@@ -0,0 +1,27 @@
+{
+  lib,
+  rustPlatform,
+  fetchFromGitHub,
+}:
+rustPlatform.buildRustPackage (finalAttrs: {
+  pname = "leangz";
+  version = "0.1.19"; # Should match LEANTAR_VERSION in leanprover/lean4/CMakeLists.txt
+
+  src = fetchFromGitHub {
+    owner = "digama0";
+    repo = "leangz";
+    rev = "v${finalAttrs.version}";
+    hash = "sha256-kDvaydStWiJYCmKjoU39tuOQHNw5Zo577GeAvlENO2o=";
+  };
+
+  cargoHash = "sha256-n3iqdRbXcSsCL+8/vDcdOXwnbU9k7DTSKR14gZ4Zlxg=";
+
+  __structuredAttrs = true;
+
+  meta = {
+    description = "Lean 4 .olean file (de)compressor";
+    homepage = "https://github.com/digama0/leangz";
+    license = lib.licenses.asl20;
+    maintainers = with lib.maintainers; [ niklashh ];
+  };
+})

pkgs/development/lean-modules/Cli/default.nix

@@ -6,13 +6,13 @@
 
 buildLakePackage {
   pname = "lean4-cli";
-  version = "4.29.0";
+  version = "4.30.0";
 
   src = fetchFromGitHub {
     owner = "leanprover";
     repo = "lean4-cli";
-    tag = "v4.29.0";
-    hash = "sha256-jCUl4sXVmwtYPuQecEUFH6mwFzPaQY7au4624EOiWjk=";
+    tag = "v4.30.0";
+    hash = "sha256-oMaqHvWlEfk1601JfNKPvkGIWgMW6tiF7Mej7g63vh0=";
   };
 
   leanPackageName = "Cli";
@@ -31,6 +31,9 @@ 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 ];
+    maintainers = with lib.maintainers; [
+      nadja-y
+      niklashh
+    ];
   };
 }

pkgs/development/lean-modules/LeanSearchClient/default.nix

@@ -22,6 +22,9 @@ 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 ];
+    maintainers = with lib.maintainers; [
+      nadja-y
+      niklashh
+    ];
   };
 }

pkgs/development/lean-modules/Qq/default.nix

@@ -6,13 +6,13 @@
 
 buildLakePackage {
   pname = "lean4-Qq";
-  version = "4.29.0";
+  version = "4.30.0";
 
   src = fetchFromGitHub {
     owner = "leanprover-community";
     repo = "quote4";
-    tag = "v4.29.0";
-    hash = "sha256-pNY5hv1nJbreCfU4EewIHCpiryIBv1ghWibrUW8vnQ0=";
+    tag = "v4.30.0";
+    hash = "sha256-jVsRw/R7D7HmsE7vQvVeDXcnVerlcDBOrhf9FJJiXkY=";
   };
 
   leanPackageName = "Qq";
@@ -21,6 +21,9 @@ 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 ];
+    maintainers = with lib.maintainers; [
+      nadja-y
+      niklashh
+    ];
   };
 }

pkgs/development/lean-modules/aesop/default.nix

@@ -7,13 +7,13 @@
 
 buildLakePackage {
   pname = "lean4-aesop";
-  version = "4.29.0";
+  version = "4.30.0";
 
   src = fetchFromGitHub {
     owner = "leanprover-community";
     repo = "aesop";
-    tag = "v4.29.0";
-    hash = "sha256-CNwxNig8OWjtfQRYyRnM/HGBn2oaNX5qP9CVT2eWNlg=";
+    tag = "v4.30.0";
+    hash = "sha256-7PhQVMdiYImuzRYdf0Kgw3JYS4nBLfILXxyhFH8Zag0=";
   };
 
   leanPackageName = "aesop";
@@ -23,6 +23,9 @@ 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 ];
+    maintainers = with lib.maintainers; [
+      nadja-y
+      niklashh
+    ];
   };
 }

pkgs/development/lean-modules/batteries/default.nix

@@ -6,21 +6,34 @@
 
 buildLakePackage {
   pname = "lean4-batteries";
-  version = "4.29.0";
+  version = "4.30.0";
 
   src = fetchFromGitHub {
     owner = "leanprover-community";
     repo = "batteries";
-    tag = "v4.29.0";
-    hash = "sha256-sEIDi2i2FaLTgKYWt/kzqPrjMdf+bFURfhw6ZZWBawQ=";
+    tag = "v4.30.0";
+    hash = "sha256-OOcKCQEgnn9zkkwjHOovMb/IprNomTDufLOfEXs7hFU=";
   };
 
   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 ];
+    maintainers = with lib.maintainers; [
+      nadja-y
+      niklashh
+    ];
   };
 }

pkgs/development/lean-modules/importGraph/default.nix

@@ -7,13 +7,13 @@
 
 buildLakePackage {
   pname = "lean4-importGraph";
-  version = "4.29.0";
+  version = "4.30.0";
 
   src = fetchFromGitHub {
     owner = "leanprover-community";
     repo = "import-graph";
-    tag = "v4.29.0";
-    hash = "sha256-tqdO2qyWiJzEbK0yuu4+tiOXTEg9XJfGnI7z6Jh/abg=";
+    tag = "v4.30.0";
+    hash = "sha256-V3bGQxTNs2G4MqaVxRb6WED1a7VaHfEo1HgBNqPipz8=";
   };
 
   leanPackageName = "importGraph";
@@ -23,6 +23,9 @@ 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 ];
+    maintainers = with lib.maintainers; [
+      nadja-y
+      niklashh
+    ];
   };
 }

pkgs/development/lean-modules/lean4/default.nix

@@ -8,16 +8,18 @@
   git,
   gmp,
   cadical,
+  leangz,
   pkg-config,
   libuv,
   perl,
   testers,
 }:
-
 let
+  cadical' = cadical.override { version = "2.1.3"; };
+
   lean4 = stdenv.mkDerivation (finalAttrs: {
     pname = "lean4";
-    version = "4.29.0";
+    version = "4.30.0";
 
     mimalloc-src = fetchFromGitHub {
       owner = "microsoft";
@@ -30,7 +32,7 @@ let
       owner = "leanprover";
       repo = "lean4";
       tag = "v${finalAttrs.version}";
-      hash = "sha256-0v4OTrCLdHBbWJUq7hIjJonqget9SvsG3izGlOwhwyU=";
+      hash = "sha256-YTsfIppd6km7wOjAxRH5KMPsW++ztFDCJT2up72J86Q=";
     };
 
     # Vendor mimalloc. Upstream has since partially adopted FetchContent:
@@ -70,12 +72,13 @@ let
     nativeBuildInputs = [
       cmake
       pkg-config
+      leangz # Provides leantar
     ];
 
     buildInputs = [
       gmp
       libuv
-      cadical
+      cadical'
     ];
 
     nativeCheckInputs = [
@@ -103,7 +106,10 @@ 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 ];
+      maintainers = with lib.maintainers; [
+        nadja-y
+        niklashh
+      ];
       mainProgram = "lean";
     };
   });

pkgs/development/lean-modules/mathlib/default.nix

@@ -14,13 +14,13 @@
 
 buildLakePackage {
   pname = "lean4-mathlib";
-  version = "4.29.0";
+  version = "4.30.0";
 
   src = fetchFromGitHub {
     owner = "leanprover-community";
     repo = "mathlib4";
-    tag = "v4.29.0";
-    hash = "sha256-fe+qS7gNxdLnACX3/jqToa9m7r1gbskY6kDJbm1ZefE=";
+    tag = "v4.30.0";
+    hash = "sha256-RxOxdUiVUAxUbfVhxlkjmPX1V64EtmIIn1eW75TiJWA=";
   };
 
   leanPackageName = "mathlib";
@@ -44,6 +44,9 @@ buildLakePackage {
     description = "Mathematical library for Lean 4";
     homepage = "https://github.com/leanprover-community/mathlib4";
     license = lib.licenses.asl20;
-    maintainers = with lib.maintainers; [ nadja-y ];
+    maintainers = with lib.maintainers; [
+      nadja-y
+      niklashh
+    ];
   };
 }

pkgs/development/lean-modules/plausible/default.nix

@@ -6,13 +6,13 @@
 
 buildLakePackage {
   pname = "lean4-plausible";
-  version = "4.29.0";
+  version = "4.30.0";
 
   src = fetchFromGitHub {
     owner = "leanprover-community";
     repo = "plausible";
-    tag = "v4.29.0";
-    hash = "sha256-08fNB2GK5AqDJ15n5Ol+HYqaSbsznyp4cerDo32bG50=";
+    tag = "v4.30.0";
+    hash = "sha256-DSaS0W2cfCUh2N+7WyiM7aUv3trtRNON0PzCgCW2SKY=";
   };
 
   leanPackageName = "plausible";
@@ -21,6 +21,9 @@ 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 ];
+    maintainers = with lib.maintainers; [
+      nadja-y
+      niklashh
+    ];
   };
 }

pkgs/development/lean-modules/proofwidgets/default.nix

@@ -62,6 +62,9 @@ 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 ];
+    maintainers = with lib.maintainers; [
+      nadja-y
+      niklashh
+    ];
   };
 }