build directly

Author: Kha

Diff for: CMakeLists.txt

@@ -1,4 +1,7 @@
 cmake_minimum_required(VERSION 3.11)
+
+option(USE_MIMALLOC "use mimalloc" ON)
+
 # store all variables passed on the command line into CL_ARGS so we can pass them to the stage builds
 # https://stackoverflow.com/a/48555098/161659
 # MUST be done before call to 'project'
@@ -14,8 +17,7 @@ foreach(var ${vars})
     if("${var}" MATCHES "USE_GMP|CHECK_OLEAN_VERSION")
       # must forward options that generate incompatible .olean format
       list(APPEND STAGE0_ARGS "-D${var}=${${var}}")
-    endif()
-    if("${var}" MATCHES "LLVM*|PKG_CONFIG|USE_LAKE")
+    elseif("${var}" MATCHES "LLVM*|PKG_CONFIG|USE_LAKE|USE_MIMALLOC")
       list(APPEND STAGE0_ARGS "-D${var}=${${var}}")
     endif()
   elseif(("${var}" MATCHES "CMAKE_.*") AND NOT ("${var}" MATCHES "CMAKE_BUILD_TYPE") AND NOT ("${var}" MATCHES "CMAKE_HOME_DIRECTORY"))
@@ -55,11 +57,23 @@ if (NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
       BUILD_IN_SOURCE ON
       INSTALL_COMMAND "")
     set(CADICAL ${CMAKE_BINARY_DIR}/cadical/cadical${CMAKE_EXECUTABLE_SUFFIX} CACHE FILEPATH "path to cadical binary" FORCE)
-    set(EXTRA_DEPENDS "cadical")
+    list(APPEND EXTRA_DEPENDS cadical)
   endif()
   list(APPEND CL_ARGS -DCADICAL=${CADICAL})
 endif()
 
+if (USE_MIMALLOC)
+  ExternalProject_add(mimalloc
+    PREFIX mimalloc
+    GIT_REPOSITORY https://github.com/microsoft/mimalloc
+    GIT_TAG v2.2.3
+    CMAKE_ARGS -DCMAKE_INSTALL_PREFIX=${CMAKE_BINARY_DIR}/mimalloc -DMI_OVERRIDE=OFF
+      -DMI_INSTALL_TOPLEVEL=ON "-DCMAKE_C_FLAGS=-DMI_SHARED_LIB=1 -DMI_SHARED_LIB_EXPORT=1"
+    BUILD_COMMAND cmake --install .
+    INSTALL_COMMAND "")
+  list(APPEND EXTRA_DEPENDS mimalloc)
+endif()
+
 ExternalProject_add(stage0
   SOURCE_DIR "${LEAN_SOURCE_DIR}/stage0"
   SOURCE_SUBDIR src

Diff for: flake.nix

@@ -31,7 +31,7 @@
           stdenv = pkgs.overrideCC pkgs.stdenv lean-packages.llvmPackages.clang;
         } ({
           buildInputs = with pkgs; [
-            cmake gmp libuv mimalloc ccache cadical pkg-config
+            cmake gmp libuv ccache cadical pkg-config
             lean-packages.llvmPackages.llvm  # llvm-symbolizer for asan/lsan
             gdb
             tree  # for CI
@@ -65,7 +65,6 @@
           ZLIB = pkgsDist.zlib;
           # for CI coredumps
           GDB = pkgsDist.gdb;
-          MIMALLOC = pkgsDist.mimalloc;
         });
     in {
       packages = {

Diff for: nix/bootstrap.nix

@@ -17,7 +17,7 @@ lib.warn "The Nix-based build is deprecated" rec {
     '';
   } // args // {
     src = args.realSrc or (sourceByRegex args.src [ "[a-z].*" "CMakeLists\.txt" ]);
-    cmakeFlags = (args.cmakeFlags or [ "-DSTAGE=1" "-DPREV_STAGE=./faux-prev-stage" "-DUSE_GITHASH=OFF" "-DCADICAL=${cadical}/bin/cadical" ]) ++ (args.extraCMakeFlags or extraCMakeFlags) ++ lib.optional (args.debug or debug) [ "-DCMAKE_BUILD_TYPE=Debug" ];
+    cmakeFlags = ["-DUSE_MIMALLOC=OFF"] ++ (args.cmakeFlags or [ "-DSTAGE=1" "-DPREV_STAGE=./faux-prev-stage" "-DUSE_GITHASH=OFF" "-DCADICAL=${cadical}/bin/cadical" ]) ++ (args.extraCMakeFlags or extraCMakeFlags) ++ lib.optional (args.debug or debug) [ "-DCMAKE_BUILD_TYPE=Debug" ];
     preConfigure = args.preConfigure or "" + ''
       # ignore absence of submodule
       sed -i 's!lake/Lake.lean!!' CMakeLists.txt

Diff for: src/CMakeLists.txt

@@ -306,11 +306,6 @@ endif()
 
 if (USE_MIMALLOC)
   set(SMALL_ALLOCATOR OFF)
-  find_package(Mimalloc 2.0.0 REQUIRED)
-  include_directories(${MIMALLOC_INCLUDE_DIRS})
-  string(APPEND LEANC_EXTRA_CC_FLAGS " -I${MIMALLOC_INCLUDE_DIRS}")
-  list(JOIN MIMALLOC_LDFLAGS " " MIMALLOC_LDFLAGS)
-  string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${MIMALLOC_LDFLAGS}")
   set(LEAN_MIMALLOC "#define LEAN_MIMALLOC")
 endif()
 
@@ -554,6 +549,9 @@ else()
   set(LEAN_IS_STAGE0 "#define LEAN_IS_STAGE0 0")
 endif()
 configure_file("${LEAN_SOURCE_DIR}/config.h.in" "${LEAN_BINARY_DIR}/include/lean/config.h")
+if (USE_MIMALLOC)
+  file(COPY "${LEAN_BINARY_DIR}/../mimalloc/include/mimalloc.h" DESTINATION "${LEAN_BINARY_DIR}/include/lean")
+endif()
 install(DIRECTORY ${LEAN_BINARY_DIR}/include/ DESTINATION include)
 configure_file(${LEAN_SOURCE_DIR}/lean.mk.in ${LEAN_BINARY_DIR}/share/lean/lean.mk)
 install(DIRECTORY ${LEAN_BINARY_DIR}/share/ DESTINATION share)

Diff for: src/cmake/Modules/FindMimalloc.cmake

@@ -13,7 +13,7 @@ Author: Leonardo de Moura
 #include <lean/config.h>
 
 #ifdef LEAN_MIMALLOC
-#include <mimalloc.h>
+#include <lean/mimalloc.h>
 #endif
 
 #ifdef __cplusplus

Diff for: src/include/lean/lean.h

@@ -4,6 +4,10 @@ stackinfo.cpp compact.cpp init_module.cpp io.cpp hash.cpp
 platform.cpp alloc.cpp allocprof.cpp sharecommon.cpp stack_overflow.cpp
 process.cpp object_ref.cpp mpn.cpp mutex.cpp libuv.cpp uv/net_addr.cpp uv/event_loop.cpp
 uv/timer.cpp uv/tcp.cpp uv/udp.cpp)
+if (USE_MIMALLOC)
+  list(PREPEND RUNTIME_OBJS ${LEAN_BINARY_DIR}/../mimalloc/lib/mimalloc.o)
+endif()
+
 add_library(leanrt_initial-exec STATIC ${RUNTIME_OBJS})
 set_target_properties(leanrt_initial-exec PROPERTIES
   ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR})