lean4: 4.30.0 -> 4.34.1

Release notes: - https://lean-lang.org/doc/reference/latest/releases/v4.34.1 - https://lean-lang.org/doc/reference/latest/releases/v4.34.0 - https://lean-lang.org/doc/reference/latest/releases/v4.33.1 - https://lean-lang.org/doc/reference/latest/releases/v4.33.0 - https://lean-lang.org/doc/reference/latest/releases/v4.32.2 - https://lean-lang.org/doc/reference/latest/releases/v4.32.1 - https://lean-lang.org/doc/reference/latest/releases/v4.32.0 - https://lean-lang.org/doc/reference/latest/releases/v4.31.0 Co-authored-by: Niklas Halonen <niklas.2.halonen@aalto.fi> Co-authored-by: jthulhu <jthulhu@posteo.net> Co-authored-by: Gaetan Lepage <gaetan@glepage.com>
2026-10-04 14:00:04 +00:00 · 2026-09-24 20:08:24 -04:00
parent 8768f5db58
commit edac0312cb
13 changed files with 119 additions and 130 deletions
--- a/pkgs/build-support/lake/default.nix
+++ b/pkgs/build-support/lake/default.nix
@@ -13,6 +13,7 @@
  gitMinimal,
  cacert,
  jq,
+  writableTmpDirAsHomeHook,
  writeText,
  stdenvNoCC,
 }:
@@ -113,48 +114,58 @@ lib.extendMkDerivation {
        lean4
        gitMinimal
        jq
+        writableTmpDirAsHomeHook
      ];

      propagatedBuildInputs = lib.optionals isLibrary leanDeps;
      buildInputs = lib.optionals (!isLibrary) leanDeps;

      configurePhase =
-        args.configurePhase or ''
-          runHook preConfigure
-
-          export HOME="$TMPDIR"
-
+        args.configurePhase or (
+          ''
+            runHook preConfigure
+          ''
          # Disable cloud caching and Reservoir lookups.
-          export LAKE_NO_CACHE=1
-          export RESERVOIR_API_URL=""
-          export LEAN_CC="${stdenv.cc}/bin/cc"
+          + ''
+            export LAKE_NO_CACHE=1
+            export RESERVOIR_API_URL=""
+            export LEAN_CC="${stdenv.cc}/bin/cc"
+          ''
+          # `lake` has no `-j`: it schedules build jobs on Lean's task manager, which otherwise
+          # sizes itself from `hardware_concurrency()` and ignores the builder's core budget.
+          + ''
+            export LEAN_NUM_THREADS="$NIX_BUILD_CORES"

-          if [ -n "''${LEAN_PATH:-}" ]; then
-            echo "buildLakePackage: LEAN_PATH=$LEAN_PATH"
-          fi
+            if [ -n "''${LEAN_PATH:-}" ]; then
+              echo "buildLakePackage: LEAN_PATH=$LEAN_PATH"
+            fi

-          ${lib.optionalString (computedLakeDeps != null) ''
-            mkdir -p .lake/packages
-            for dep in ${computedLakeDeps}/*; do
-              depName="$(basename "$dep")"
-              cp -r "$dep" ".lake/packages/$depName"
-              chmod -R u+w ".lake/packages/$depName"
-            done
+            ${lib.optionalString (computedLakeDeps != null) (
+              ''
+                mkdir -p .lake/packages
+                for dep in ${computedLakeDeps}/*; do
+                  depName="$(basename "$dep")"
+                  cp -r "$dep" ".lake/packages/$depName"
+                  chmod -R u+w ".lake/packages/$depName"
+                done
+              ''
+              # FOD deps use package-overrides.json (the on-disk mechanism).
+              # Nix-managed deps use --packages (the CLI mechanism, takes precedence).
+              + ''
+                jq -n --argjson pkgs "$(
+                  for dep in .lake/packages/*/; do
+                    [ -d "$dep" ] || continue
+                    depName="$(basename "$dep")"
+                    jq -n --arg name "$depName" --arg dir ".lake/packages/$depName" \
+                      '{type: "path", name: $name, inherited: false, dir: $dir}'
+                  done | jq -s '.'
+                )" '{schemaVersion: "1.2.0", packages: $pkgs}' > .lake/package-overrides.json
+              ''
+            )}

-            # FOD deps use package-overrides.json (the on-disk mechanism).
-            # Nix-managed deps use --packages (the CLI mechanism, takes precedence).
-            jq -n --argjson pkgs "$(
-              for dep in .lake/packages/*/; do
-                [ -d "$dep" ] || continue
-                depName="$(basename "$dep")"
-                jq -n --arg name "$depName" --arg dir ".lake/packages/$depName" \
-                  '{type: "path", name: $name, inherited: false, dir: $dir}'
-              done | jq -s '.'
-            )" '{schemaVersion: "1.2.0", packages: $pkgs}' > .lake/package-overrides.json
-          ''}
-
-          runHook postConfigure
-        '';
+            runHook postConfigure
+          ''
+        );

      buildPhase =
        args.buildPhase or ''
--- a/pkgs/by-name/le/lean4/mimalloc.patch
+++ b/pkgs/by-name/le/lean4/mimalloc.patch
@@ -1,17 +0,0 @@
--- a/CMakeLists.txt
-+++ b/CMakeLists.txt
-@@ -80,11 +80,7 @@
-   ExternalProject_add(
-     mimalloc
-     PREFIX mimalloc
-    GIT_REPOSITORY https://github.com/microsoft/mimalloc
-    GIT_TAG v2.2.3
-    # just download, we compile it as part of each stage as it is small
-    CONFIGURE_COMMAND ""
-    BUILD_COMMAND ""
-+    SOURCE_DIR "MIMALLOC-SRC"
-     INSTALL_COMMAND ""
-   )
-   list(APPEND EXTRA_DEPENDS mimalloc)
- endif()
- 
--- a/pkgs/by-name/le/lean4/package.nix
+++ b/pkgs/by-name/le/lean4/package.nix
@@ -4,38 +4,34 @@
  cmake,
  cctools,
  fetchFromGitHub,
-  git,
+  fetchpatch,
+  gitMinimal,
  gmp,
  cadical,
  leangz,
  makeWrapper,
+  openssl,
  pkg-config,
  libuv,
  enableMimalloc ? true,
  perl,
-  testers,
+  versionCheckHook,
 }:
 let
  cadical' = cadical.override { version = "2.1.3"; };
 in
 stdenv.mkDerivation (finalAttrs: {
  pname = "lean4";
-  version = "4.30.0";
+  version = "4.34.1";

-  # 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.
-  mimalloc-src = fetchFromGitHub {
-    owner = "microsoft";
-    repo = "mimalloc";
-    tag = "v2.2.3";
-    hash = "sha256-B0gngv16WFLBtrtG5NqA2m5e95bYVcQraeITcOX9A74=";
-  };
+  __structuredAttrs = true;
+  strictDeps = true;

  src = fetchFromGitHub {
    owner = "leanprover";
    repo = "lean4";
    tag = "v${finalAttrs.version}";
-    hash = "sha256-YTsfIppd6km7wOjAxRH5KMPsW++ztFDCJT2up72J86Q=";
+    hash = "sha256-JO1pCqWeotC4zjiIQZccEPXfVHnuDQC0DugyuJvIMRs=";
  };

  postPatch =
@@ -43,38 +39,38 @@ stdenv.mkDerivation (finalAttrs: {
      pattern = "\${LEAN_BINARY_DIR}/../mimalloc/src/mimalloc";
    in
    ''
-      substituteInPlace src/CMakeLists.txt \
-        --replace-fail 'set(GIT_SHA1 "")' 'set(GIT_SHA1 "${finalAttrs.src.tag}")'
-
-      # Remove tests that fails in sandbox.
-      # It expects `sourceRoot` to be a git repository.
-      rm -rf src/lake/examples/git/
+      substituteInPlace \
+        src/CMakeLists.txt \
+        src/runtime/CMakeLists.txt \
+        stage0/src/CMakeLists.txt \
+        stage0/src/runtime/CMakeLists.txt \
+        --replace-fail '${pattern}' '${finalAttrs.mimalloc-src}'
    ''
-    + (lib.optionalString enableMimalloc ''
-      substituteInPlace CMakeLists.txt \
-        --replace-fail 'MIMALLOC-SRC' '${finalAttrs.mimalloc-src}'
-      for file in stage0/src/CMakeLists.txt stage0/src/runtime/CMakeLists.txt src/CMakeLists.txt src/runtime/CMakeLists.txt; do
-        substituteInPlace "$file" \
-          --replace-fail '${pattern}' '${finalAttrs.mimalloc-src}'
-      done
-    '');
+    # Remove tests that fails in sandbox.
+    # It expects `sourceRoot` to be a git repository.
+    + ''
+      rm -rf src/lake/examples/git/
+    '';

  preConfigure = ''
    patchShebangs stage0/src/bin/ src/bin/
  '';

  nativeBuildInputs = [
+    cadical'
    cmake
    pkg-config
    makeWrapper
    leangz # Provides leantar
  ]
-  ++ lib.optionals stdenv.hostPlatform.isDarwin [ cctools.libtool ];
+  ++ lib.optionals stdenv.hostPlatform.isDarwin [
+    cctools.libtool
+  ];

  buildInputs = [
    gmp
    libuv
-    cadical'
+    openssl
  ];

  postInstall = ''
@@ -83,26 +79,31 @@ stdenv.mkDerivation (finalAttrs: {
  '';

  nativeCheckInputs = [
-    git
+    gitMinimal
    perl
  ];

-  patches = [ ./mimalloc.patch ];
+  # 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.
+  mimalloc-src = fetchFromGitHub {
+    owner = "microsoft";
+    repo = "mimalloc";
+    tag = "v3.4.5";
+    hash = "sha256-vNVZw2YsDkf0GcdFTNb/fXMQLQYvoc8P425LupPShpo=";
+  };

  cmakeFlags = [
-    "-DUSE_GITHASH=OFF"
-    "-DINSTALL_LICENSE=OFF"
-    "-DINSTALL_CADICAL=OFF"
-    "-DSTAGE1_CMAKE_INSTALL_PREFIX=${placeholder "out"}"
-    "-DUSE_MIMALLOC=${if enableMimalloc then "ON" else "OFF"}"
+    (lib.cmakeBool "USE_GITHASH" false)
+    (lib.cmakeBool "INSTALL_LICENSE" false)
+    (lib.cmakeBool "INSTALL_CADICAL" false)
+    (lib.cmakeBool "USE_MIMALLOC" enableMimalloc)
+    (lib.cmakeFeature "FETCHCONTENT_SOURCE_DIR_MIMALLOC" finalAttrs.mimalloc-src.outPath)
  ];

-  passthru.tests = {
-    version = testers.testVersion {
-      package = finalAttrs.finalPackage;
-      version = "v${finalAttrs.version}";
-    };
-  };
+  nativeInstallCheckInputs = [
+    versionCheckHook
+  ];
+  doInstallCheck = true;

  meta = {
    description = "Automatic and interactive theorem prover";
--- a/pkgs/development/lean-modules/Cli/default.nix
+++ b/pkgs/development/lean-modules/Cli/default.nix
@@ -7,13 +7,13 @@
 buildLakePackage (finalAttrs: {
  pname = "lean4-cli";
  # nixpkgs-update: no auto update
-  version = "4.30.0";
+  version = "4.34.0";

  src = fetchFromGitHub {
    owner = "leanprover";
    repo = "lean4-cli";
    tag = "v${finalAttrs.version}";
-    hash = "sha256-oMaqHvWlEfk1601JfNKPvkGIWgMW6tiF7Mej7g63vh0=";
+    hash = "sha256-3HLYlycvm4Ho98pB7eF+u8RN1GQJ7Ve6COqMSZr4Hic=";
  };

  leanPackageName = "Cli";
--- a/pkgs/development/lean-modules/LeanSearchClient/default.nix
+++ b/pkgs/development/lean-modules/LeanSearchClient/default.nix
@@ -7,13 +7,13 @@
 buildLakePackage {
  pname = "lean4-LeanSearchClient";
  # nixpkgs-update: no auto update
-  version = "4.12.0-unstable-2026-02-12";
+  version = "4.34.0-unstable-2026-09-14";

  src = fetchFromGitHub {
    owner = "leanprover-community";
    repo = "LeanSearchClient";
-    rev = "c5d5b8fe6e5158def25cd28eb94e4141ad97c843";
-    hash = "sha256-L2aAwn3OeRLVt/VccLdBS0ogqmIIKAwnz94PpAOhaRc=";
+    rev = "ddf04cf3949fa556442341e87d47f9f6e6074707";
+    hash = "sha256-S2dp1E3Xv9b+U+r+b/MKGHviOg7ySE8QAX7EoB6Jbl8=";
  };

  leanPackageName = "LeanSearchClient";
--- a/pkgs/development/lean-modules/Qq/default.nix
+++ b/pkgs/development/lean-modules/Qq/default.nix
@@ -7,13 +7,13 @@
 buildLakePackage {
  pname = "lean4-Qq";
  # nixpkgs-update: no auto update
-  version = "4.30.0";
+  version = "4.34.0-unstable-2026-09-14";

  src = fetchFromGitHub {
    owner = "leanprover-community";
    repo = "quote4";
-    tag = "v4.30.0";
-    hash = "sha256-jVsRw/R7D7HmsE7vQvVeDXcnVerlcDBOrhf9FJJiXkY=";
+    rev = "6a489d9af5d0c47e5b259e2e8bcdfc1811b5a259";
+    hash = "sha256-fRsOiIgpS0YYWUsL/TwYn+orRC4rgNz7NSQ4+XCHCHQ=";
  };

  leanPackageName = "Qq";
--- a/pkgs/development/lean-modules/aesop/default.nix
+++ b/pkgs/development/lean-modules/aesop/default.nix
@@ -8,13 +8,13 @@
 buildLakePackage {
  pname = "lean4-aesop";
  # nixpkgs-update: no auto update
-  version = "4.30.0";
+  version = "4.34.0-unstable-2026-09-14";

  src = fetchFromGitHub {
    owner = "leanprover-community";
    repo = "aesop";
-    tag = "v4.30.0";
-    hash = "sha256-7PhQVMdiYImuzRYdf0Kgw3JYS4nBLfILXxyhFH8Zag0=";
+    rev = "355695d523e41d0554926416cba2a2b3544fbbc9";
+    hash = "sha256-yF2+P7H0B3546zopncnH2APEynRRJjTy+17OEAFovkE=";
  };

  leanPackageName = "aesop";
--- a/pkgs/development/lean-modules/batteries/default.nix
+++ b/pkgs/development/lean-modules/batteries/default.nix
@@ -7,13 +7,13 @@
 buildLakePackage {
  pname = "lean4-batteries";
  # nixpkgs-update: no auto update
-  version = "4.30.0-unstable-2026-05-26";
+  version = "4.34.0-unstable-2026-09-14";

  src = fetchFromGitHub {
    owner = "leanprover-community";
    repo = "batteries";
-    rev = "32dc18cde3684679f3c003de608743b57498c56f";
-    hash = "sha256-OOcKCQEgnn9zkkwjHOovMb/IprNomTDufLOfEXs7hFU=";
+    rev = "f2effa3d803fda822b1f97b806c47cf2adfbcbc2";
+    hash = "sha256-Y/Vfr3gVFfik2Rfshgu0iIn0IQYYCb6ShDt5nZe4RBc=";
  };

  leanPackageName = "batteries";
--- a/pkgs/development/lean-modules/importGraph/default.nix
+++ b/pkgs/development/lean-modules/importGraph/default.nix
@@ -8,13 +8,13 @@
 buildLakePackage {
  pname = "lean4-importGraph";
  # nixpkgs-update: no auto update
-  version = "4.30.0-unstable-2026-05-26";
+  version = "4.34.0-unstable-2026-09-14";

  src = fetchFromGitHub {
    owner = "leanprover-community";
    repo = "import-graph";
-    rev = "515cf9d0c00ece5e661f6de4326a53dedc1e8ea1";
-    hash = "sha256-V3bGQxTNs2G4MqaVxRb6WED1a7VaHfEo1HgBNqPipz8=";
+    rev = "e928b72544873815af278d38681b31c0293588e3";
+    hash = "sha256-U3eskYuk2vJ35IJqBsIgOHKL03UHtlEriyssNkBxwjM=";
  };

  leanPackageName = "importGraph";
--- a/pkgs/development/lean-modules/lean4/default.nix
+++ b/pkgs/development/lean-modules/lean4/default.nix
@@ -6,11 +6,13 @@
  cmake,
  cctools,
  fetchFromGitHub,
+  fetchpatch,
  git,
  gmp,
  cadical,
  cadical' ? cadical.override { version = "2.1.3"; },
  leangz,
+  openssl,
  pkg-config,
  libuv,
  perl,
@@ -22,20 +24,20 @@
 let
  lean4 = stdenv.mkDerivation (finalAttrs: {
    pname = "lean4";
-    version = "4.30.0";
+    version = "4.34.1";

    mimalloc-src = fetchFromGitHub {
      owner = "microsoft";
      repo = "mimalloc";
-      tag = "v2.2.3";
-      hash = "sha256-B0gngv16WFLBtrtG5NqA2m5e95bYVcQraeITcOX9A74=";
+      tag = "v3.4.5";
+      hash = "sha256-vNVZw2YsDkf0GcdFTNb/fXMQLQYvoc8P425LupPShpo=";
    };

    src = fetchFromGitHub {
      owner = "leanprover";
      repo = "lean4";
      tag = "v${finalAttrs.version}";
-      hash = "sha256-YTsfIppd6km7wOjAxRH5KMPsW++ztFDCJT2up72J86Q=";
+      hash = "sha256-JO1pCqWeotC4zjiIQZccEPXfVHnuDQC0DugyuJvIMRs=";
    };

    # Vendor mimalloc. Upstream has since partially adopted FetchContent:
@@ -48,15 +50,6 @@ let
        pattern = "\${LEAN_BINARY_DIR}/../mimalloc/src/mimalloc";
      in
      ''
-        substituteInPlace src/CMakeLists.txt \
-          --replace-fail 'set(GIT_SHA1 "")' 'set(GIT_SHA1 "${finalAttrs.src.tag}")'
-
-        rm -rf src/lake/examples/git/
-
-        substituteInPlace CMakeLists.txt \
-          --replace-fail 'GIT_REPOSITORY https://github.com/microsoft/mimalloc' \
-                         'SOURCE_DIR "${finalAttrs.mimalloc-src}"' \
-          --replace-fail 'GIT_TAG ${finalAttrs.mimalloc-src.tag}' ""
        for file in stage0/src/CMakeLists.txt stage0/src/runtime/CMakeLists.txt src/CMakeLists.txt src/runtime/CMakeLists.txt; do
          substituteInPlace "$file" \
            --replace-fail '${pattern}' '${finalAttrs.mimalloc-src}'
@@ -83,6 +76,7 @@ let
      gmp
      libuv
      cadical'
+      openssl
    ];

    nativeCheckInputs = [
@@ -95,8 +89,8 @@ let
      "-DINSTALL_LICENSE=OFF"
      "-DINSTALL_CADICAL=OFF"
      "-DINSTALL_LEANTAR=OFF"
-      "-DSTAGE1_CMAKE_INSTALL_PREFIX=${placeholder "out"}"
      "-DUSE_MIMALLOC=ON"
+      "-DFETCHCONTENT_SOURCE_DIR_MIMALLOC=${finalAttrs.mimalloc-src}"
    ];

    passthru.tests = {
--- a/pkgs/development/lean-modules/mathlib/default.nix
+++ b/pkgs/development/lean-modules/mathlib/default.nix
@@ -21,13 +21,13 @@ let
  mathlib__archive = buildLakePackage (finalAttrs: {
    pname = "lean4-mathlib";
    # nixpkgs-update: no auto update
-    version = "4.30.0";
+    version = "4.34.1";

    src = fetchFromGitHub {
      owner = "leanprover-community";
      repo = "mathlib4";
      tag = "v${finalAttrs.version}";
-      hash = "sha256-RxOxdUiVUAxUbfVhxlkjmPX1V64EtmIIn1eW75TiJWA=";
+      hash = "sha256-y3ql35O/z5fC9PSmMxqYAXZn63yByp3Z8LD00y9D2og=";
    };

    leanPackageName = "mathlib";
--- a/pkgs/development/lean-modules/plausible/default.nix
+++ b/pkgs/development/lean-modules/plausible/default.nix
@@ -7,13 +7,13 @@
 buildLakePackage {
  pname = "lean4-plausible";
  # nixpkgs-update: no auto update
-  version = "4.30.0-unstable-2026-05-26";
+  version = "4.34.0-unstable-2026-09-14";

  src = fetchFromGitHub {
    owner = "leanprover-community";
    repo = "plausible";
-    rev = "a456461b368b71d2accd95234832cd9c174b5437";
-    hash = "sha256-DSaS0W2cfCUh2N+7WyiM7aUv3trtRNON0PzCgCW2SKY=";
+    rev = "118aa17ee84656b8bd727fef7c458ee8c833385c";
+    hash = "sha256-/ianaKsruF30J5tqK4vtbXsFd3mu4Xt8Ppj4ibHDEvg=";
  };

  leanPackageName = "plausible";
--- a/pkgs/development/lean-modules/proofwidgets/default.nix
+++ b/pkgs/development/lean-modules/proofwidgets/default.nix
@@ -10,13 +10,13 @@
 buildLakePackage (finalAttrs: {
  pname = "lean4-proofwidgets";
  # nixpkgs-update: no auto update
-  version = "0.0.99";
+  version = "0.0.111-unstable-2026-09-14";

  src = fetchFromGitHub {
    owner = "leanprover-community";
    repo = "ProofWidgets4";
-    tag = "v${finalAttrs.version}";
-    hash = "sha256-kGoEkKGrucNUWFYkHW2LsS1gI4C0J8bAHQL2MiE4Pzc=";
+    rev = "106ff4fafc74ef4ac99d81dbf3ab399118f497a5";
+    hash = "sha256-xjd3p+637F5q7xGTpDpy3/UCewpO8ArCfSAMAnAAjgs=";
  };

  leanPackageName = "proofwidgets";
@@ -32,7 +32,7 @@ buildLakePackage (finalAttrs: {
    name = "lean4-proofwidgets-npm-deps";
    src = finalAttrs.src;
    sourceRoot = "source/widget";
-    hash = "sha256-ssWSr2qfsIbX25DidiVPm0tsLGjrhQhQ6YKPL0rfc1k=";
+    hash = "sha256-z3LCBPmowLlkn5w/z72J1l8WnY60F8I7r48HMM/Lnns=";
  };
  npmRoot = "widget";