Skip to content

Commit 301d638

Browse files
KhaKha
committed
build directly
1 parent 76ddc52 commit 301d638

6 files changed

Lines changed: 24 additions & 24 deletions

File tree

‎CMakeLists.txt‎

Lines changed: 15 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,7 @@
11
cmake_minimum_required(VERSION 3.11)
2+
3+
option(USE_MIMALLOC "use mimalloc" ON)
4+
25
# store all variables passed on the command line into CL_ARGS so we can pass them to the stage builds
36
# https://stackoverflow.com/a/48555098/161659
47
# MUST be done before call to 'project'
@@ -14,8 +17,7 @@ foreach(var ${vars})
1417
if("${var}" MATCHES "USE_GMP|CHECK_OLEAN_VERSION")
1518
# must forward options that generate incompatible .olean format
1619
list(APPEND STAGE0_ARGS "-D${var}=${${var}}")
17-
endif()
18-
if("${var}" MATCHES "LLVM*|PKG_CONFIG|USE_LAKE")
20+
elseif("${var}" MATCHES "LLVM*|PKG_CONFIG|USE_LAKE|USE_MIMALLOC")
1921
list(APPEND STAGE0_ARGS "-D${var}=${${var}}")
2022
endif()
2123
elseif(("${var}" MATCHES "CMAKE_.*") AND NOT ("${var}" MATCHES "CMAKE_BUILD_TYPE") AND NOT ("${var}" MATCHES "CMAKE_HOME_DIRECTORY"))
@@ -55,11 +57,21 @@ if (NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
5557
BUILD_IN_SOURCE ON
5658
INSTALL_COMMAND "")
5759
set(CADICAL ${CMAKE_BINARY_DIR}/cadical/cadical${CMAKE_EXECUTABLE_SUFFIX} CACHE FILEPATH "path to cadical binary" FORCE)
58-
set(EXTRA_DEPENDS "cadical")
60+
list(APPEND EXTRA_DEPENDS cadical)
5961
endif()
6062
list(APPEND CL_ARGS -DCADICAL=${CADICAL})
6163
endif()
6264

65+
if (USE_MIMALLOC)
66+
ExternalProject_add(mimalloc
67+
PREFIX mimalloc
68+
GIT_REPOSITORY https://github.com/microsoft/mimalloc
69+
GIT_TAG v2.2.3
70+
CMAKE_ARGS -DCMAKE_INSTALL_PREFIX=${CMAKE_BINARY_DIR}/mimalloc -DMI_OVERRIDE=OFF
71+
-DMI_INSTALL_TOPLEVEL=ON "-DCMAKE_C_FLAGS=-DMI_SHARED_LIB=1 -DMI_SHARED_LIB_EXPORT=1")
72+
list(APPEND EXTRA_DEPENDS mimalloc)
73+
endif()
74+
6375
ExternalProject_add(stage0
6476
SOURCE_DIR "${LEAN_SOURCE_DIR}/stage0"
6577
SOURCE_SUBDIR src

‎flake.nix‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,7 @@
3131
stdenv = pkgs.overrideCC pkgs.stdenv lean-packages.llvmPackages.clang;
3232
} ({
3333
buildInputs = with pkgs; [
34-
cmake gmp libuv mimalloc ccache cadical pkg-config
34+
cmake gmp libuv ccache cadical pkg-config
3535
lean-packages.llvmPackages.llvm # llvm-symbolizer for asan/lsan
3636
gdb
3737
tree # for CI
@@ -65,7 +65,6 @@
6565
ZLIB = pkgsDist.zlib;
6666
# for CI coredumps
6767
GDB = pkgsDist.gdb;
68-
MIMALLOC = pkgsDist.mimalloc;
6968
});
7069
in {
7170
packages = {

‎src/CMakeLists.txt‎

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -306,11 +306,6 @@ endif()
306306

307307
if (USE_MIMALLOC)
308308
set(SMALL_ALLOCATOR OFF)
309-
find_package(Mimalloc 2.0.0 REQUIRED)
310-
include_directories(${MIMALLOC_INCLUDE_DIRS})
311-
string(APPEND LEANC_EXTRA_CC_FLAGS " -I${MIMALLOC_INCLUDE_DIRS}")
312-
list(JOIN MIMALLOC_LDFLAGS " " MIMALLOC_LDFLAGS)
313-
string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${MIMALLOC_LDFLAGS}")
314309
set(LEAN_MIMALLOC "#define LEAN_MIMALLOC")
315310
endif()
316311

@@ -554,6 +549,9 @@ else()
554549
set(LEAN_IS_STAGE0 "#define LEAN_IS_STAGE0 0")
555550
endif()
556551
configure_file("${LEAN_SOURCE_DIR}/config.h.in" "${LEAN_BINARY_DIR}/include/lean/config.h")
552+
if (USE_MIMALLOC)
553+
file(COPY "${LEAN_BINARY_DIR}/../mimalloc/include/mimalloc.h" DESTINATION "${LEAN_BINARY_DIR}/include/lean")
554+
endif()
557555
install(DIRECTORY ${LEAN_BINARY_DIR}/include/ DESTINATION include)
558556
configure_file(${LEAN_SOURCE_DIR}/lean.mk.in ${LEAN_BINARY_DIR}/share/lean/lean.mk)
559557
install(DIRECTORY ${LEAN_BINARY_DIR}/share/ DESTINATION share)

‎src/cmake/Modules/FindMimalloc.cmake‎

Lines changed: 0 additions & 13 deletions
This file was deleted.

‎src/include/lean/lean.h‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ Author: Leonardo de Moura
1313
#include <lean/config.h>
1414

1515
#ifdef LEAN_MIMALLOC
16-
#include <mimalloc.h>
16+
#include <lean/mimalloc.h>
1717
#endif
1818

1919
#ifdef __cplusplus

‎src/runtime/CMakeLists.txt‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,10 @@ stackinfo.cpp compact.cpp init_module.cpp io.cpp hash.cpp
44
platform.cpp alloc.cpp allocprof.cpp sharecommon.cpp stack_overflow.cpp
55
process.cpp object_ref.cpp mpn.cpp mutex.cpp libuv.cpp uv/net_addr.cpp uv/event_loop.cpp
66
uv/timer.cpp uv/tcp.cpp uv/udp.cpp)
7+
if (USE_MIMALLOC)
8+
list(PREPEND RUNTIME_OBJS ${LEAN_BINARY_DIR}/../mimalloc/lib/mimalloc.o)
9+
endif()
10+
711
add_library(leanrt_initial-exec STATIC ${RUNTIME_OBJS})
812
set_target_properties(leanrt_initial-exec PROPERTIES
913
ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR})

0 commit comments

Comments
 (0)