diff --git a/pkgs/by-name/le/lean4/package.nix b/pkgs/by-name/le/lean4/package.nix index dbf5e3b0d7d7..a1016a1b437a 100644 --- a/pkgs/by-name/le/lean4/package.nix +++ b/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"; }; diff --git a/pkgs/by-name/le/leangz/package.nix b/pkgs/by-name/le/leangz/package.nix new file mode 100644 index 000000000000..5af5edd28e53 --- /dev/null +++ b/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 ]; + }; +}) diff --git a/pkgs/development/lean-modules/Cli/default.nix b/pkgs/development/lean-modules/Cli/default.nix index d3bc495ee9cf..07476219fea2 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.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 + ]; }; } diff --git a/pkgs/development/lean-modules/LeanSearchClient/default.nix b/pkgs/development/lean-modules/LeanSearchClient/default.nix index b7e25b5ecbd0..da6eaf0263d0 100644 --- a/pkgs/development/lean-modules/LeanSearchClient/default.nix +++ b/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 + ]; }; } diff --git a/pkgs/development/lean-modules/Qq/default.nix b/pkgs/development/lean-modules/Qq/default.nix index 6feb6fa51916..a91693775347 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.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 + ]; }; } diff --git a/pkgs/development/lean-modules/aesop/default.nix b/pkgs/development/lean-modules/aesop/default.nix index 7d8ad308741a..f71d9e7c9f47 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.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 + ]; }; } diff --git a/pkgs/development/lean-modules/batteries/default.nix b/pkgs/development/lean-modules/batteries/default.nix index 9fdb1efd8686..3e06e945f9fa 100644 --- a/pkgs/development/lean-modules/batteries/default.nix +++ b/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 + ]; }; } diff --git a/pkgs/development/lean-modules/importGraph/default.nix b/pkgs/development/lean-modules/importGraph/default.nix index 4da481fd5a16..6692a5f99ec2 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.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 + ]; }; } diff --git a/pkgs/development/lean-modules/lean4/default.nix b/pkgs/development/lean-modules/lean4/default.nix index 7ba6dd5170f4..2e1c9b2f3c02 100644 --- a/pkgs/development/lean-modules/lean4/default.nix +++ b/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"; }; }); diff --git a/pkgs/development/lean-modules/mathlib/default.nix b/pkgs/development/lean-modules/mathlib/default.nix index 70a34dd9f333..60ae77331f02 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.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 + ]; }; } diff --git a/pkgs/development/lean-modules/plausible/default.nix b/pkgs/development/lean-modules/plausible/default.nix index 07b22b3ebe87..6f4d08d0ee28 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.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 + ]; }; } diff --git a/pkgs/development/lean-modules/proofwidgets/default.nix b/pkgs/development/lean-modules/proofwidgets/default.nix index 54998125b500..3a2793272012 100644 --- a/pkgs/development/lean-modules/proofwidgets/default.nix +++ b/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 + ]; }; }