lean4: 4.18.0 -> 4.19.0

Release notes:
- https://github.com/leanprover/lean4/releases/tag/v4.19.0
- https://github.com/leanprover/lean4/releases/tag/v4.19.0-rc3
- https://github.com/leanprover/lean4/releases/tag/v4.19.0-rc2
- https://github.com/leanprover/lean4/releases/tag/v4.19.0-rc1

pkgs/by-name/le/lean4/mimalloc.patch

@@ -0,0 +1,16 @@
+--- a/CMakeLists.txt
++++ b/CMakeLists.txt
+@@ -77,12 +77,8 @@
+ if (USE_MIMALLOC)
+   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()
+ 

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

@@ -8,29 +8,51 @@
   cadical,
   pkg-config,
   libuv,
+  enableMimalloc ? true,
   perl,
   testers,
 }:
 
 stdenv.mkDerivation (finalAttrs: {
   pname = "lean4";
-  version = "4.18.0";
+  version = "4.19.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.
+  mimalloc-src = fetchFromGitHub {
+    owner = "microsoft";
+    repo = "mimalloc";
+    tag = "v2.2.3";
+    hash = "sha256-B0gngv16WFLBtrtG5NqA2m5e95bYVcQraeITcOX9A74=";
+  };
 
   src = fetchFromGitHub {
     owner = "leanprover";
     repo = "lean4";
     tag = "v${finalAttrs.version}";
-    hash = "sha256-1hVcRO9RbVUgoKTUTFXBqJZwt50/aw/P9dxUdI7RpCc=";
+    hash = "sha256-Iw5JSamrty9l6aJ2WwslAolSHfi2q0UO8P8HI1gp+j8=";
   };
 
-  postPatch = ''
-    substituteInPlace src/CMakeLists.txt \
-      --replace-fail 'set(GIT_SHA1 "")' 'set(GIT_SHA1 "${finalAttrs.src.tag}")'
+  postPatch =
+    let
+      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/
-  '';
+      # Remove tests that fails in sandbox.
+      # It expects `sourceRoot` to be a git repository.
+      rm -rf src/lake/examples/git/
+    ''
+    + (lib.optionalString enableMimalloc ''
+      substituteInPlace CMakeLists.txt \
+        --replace-fail 'MIMALLOC-SRC' '${finalAttrs.mimalloc-src}'
+      for file in src/CMakeLists.txt src/runtime/CMakeLists.txt; do
+        substituteInPlace "$file" \
+          --replace-fail '${pattern}' '${finalAttrs.mimalloc-src}'
+      done
+    '');
 
   preConfigure = ''
     patchShebangs stage0/src/bin/ src/bin/
@@ -52,9 +74,12 @@ stdenv.mkDerivation (finalAttrs: {
     perl
   ];
 
+  patches = [ ./mimalloc.patch ];
+
   cmakeFlags = [
     "-DUSE_GITHASH=OFF"
     "-DINSTALL_LICENSE=OFF"
+    "-DUSE_MIMALLOC=${if enableMimalloc then "ON" else "OFF"}"
   ];
 
   passthru.tests = {