diff --git a/bin/leanc.in b/bin/leanc.in index 61499c7d39..6650661a25 100644 --- a/bin/leanc.in +++ b/bin/leanc.in @@ -16,4 +16,5 @@ for cxx in $LEAN_CXX @CMAKE_CXX_COMPILER@ /usr/bin/g++; do fi done [ -f $LEAN_CXX ] || command -v $LEAN_CXX || error "no suitable C++ compiler found!" -$LEAN_CXX -std=c++14 -D LEAN_MULTI_THREAD -pthread -fPIC "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" -lleanstatic -lleanstdlib -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument +# NOTE: leanstatic and leanstdlib are cyclically dependent +$LEAN_CXX -std=c++14 -D LEAN_MULTI_THREAD -pthread -fPIC "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" -lleanstatic -lleanstdlib -lleanstatic -lleanstdlib -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index d8359436a7..4f4b9cb822 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -457,13 +457,13 @@ add_library(leanstatic_stage0 ${LEAN_LIBRARY_TYPE} ${LEAN_OBJS} $" "$" "${LEAN_SOURCE_DIR}/../bin" + DEPENDS leanstatic leanstdlib ) # Configure leanc configure_file("${LEAN_SOURCE_DIR}/../bin/leanc.in" "${CMAKE_CURRENT_BINARY_DIR}/tmp/leanc") diff --git a/src/runtime/init_module.cpp b/src/runtime/init_module.cpp index 49690446c7..9f31641319 100644 --- a/src/runtime/init_module.cpp +++ b/src/runtime/init_module.cpp @@ -10,7 +10,6 @@ Author: Leonardo de Moura #include "runtime/thread.h" #include "runtime/object.h" #include "runtime/io.h" -#include "runtime/platform.h" namespace lean { void initialize_runtime_module() { @@ -20,10 +19,8 @@ void initialize_runtime_module() { initialize_io(); initialize_serializer(); initialize_thread(); - initialize_platform(); } void finalize_runtime_module() { - finalize_platform(); finalize_thread(); finalize_serializer(); finalize_io(); diff --git a/src/runtime/platform.cpp b/src/runtime/platform.cpp index 60ac9cb95c..a1d78fa3b0 100644 --- a/src/runtime/platform.cpp +++ b/src/runtime/platform.cpp @@ -22,7 +22,4 @@ extern "C" uint8 lean_system_platform_windows(obj_arg) { return 0; #endif } - -void initialize_platform() {} -void finalize_platform() {} } diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 2080aa4710..3e3b03e025 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -18,13 +18,17 @@ else() set(LEANC_OPTS "-g") endif() -add_custom_target(stdlib +add_custom_target(make_stdlib # '-G Ninja' complains otherwise BYPRODUCTS "${CMAKE_BINARY_DIR}/stage1/libleanstdlib.a" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../library" COMMAND ${CMAKE_COMMAND} -E env "LEAN_PATH=." make -j8 "${CMAKE_BINARY_DIR}/stage1/libleanstdlib.a" "LEAN=$" "LEANC_OPTS=${LEANC_OPTS}" "STAGE1_OUT=${CMAKE_BINARY_DIR}/stage1" DEPENDS lean_stage0) -install(FILES "${CMAKE_BINARY_DIR}/stage1/libleanstdlib.a" DESTINATION lib) +set_target_properties(leanstdlib PROPERTIES + IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/stage1/libleanstdlib.a" + IMPORTED_LINK_INTERFACE_LIBRARIES leanstatic) +add_dependencies(leanstdlib make_stdlib) +install(FILES "$" DESTINATION lib) add_custom_target(update-stage0 COMMAND make update-stage0 "STAGE1_OUT=${CMAKE_BINARY_DIR}/stage1"