diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 6f747e6c25..ab1fe882ac 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -144,11 +144,12 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Windows") # do not import the world from windows.h using appropriately named flag string(APPEND LEAN_EXTRA_CXX_FLAGS " -D WIN32_LEAN_AND_MEAN") # DLLs must go next to executables on Windows - set(CMAKE_LIBRARY_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/bin") + set(CMAKE_RELATIVE_LIBRARY_OUTPUT_DIRECTORY "bin") else() - set(CMAKE_LIBRARY_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/lib/lean") + set(CMAKE_RELATIVE_LIBRARY_OUTPUT_DIRECTORY "lib/lean") endif() +set(CMAKE_LIBRARY_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/${CMAKE_RELATIVE_LIBRARY_OUTPUT_DIRECTORY}") set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/lib/lean") # OSX default thread stack size is very small. Moreover, in Debug mode, each new stack frame consumes a lot of extra memory. diff --git a/src/stdlib.make.in b/src/stdlib.make.in index 9c15811176..904ace5eb8 100644 --- a/src/stdlib.make.in +++ b/src/stdlib.make.in @@ -29,7 +29,7 @@ ifeq "${STAGE}" "0" LEANMAKE_OPTS+=C_ONLY=1 C_OUT=${LEAN_SOURCE_DIR}/../stdlib/ endif -.PHONY: Init Std Lean leanshared Lake Lake_shared lake lean +.PHONY: Init Std Lean leanshared Lake libLake_shared lake lean # These can be phony since the inner Makefile will have the correct dependencies and avoid rebuilds Init: @@ -101,7 +101,7 @@ leanshared: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRAR Lake: # lake is in its own subdirectory, so must adjust relative paths... - +"${LEAN_BIN}/leanmake" -C lake lib lib.export ../${LIB}/temp/LakeMain.o.export PKG=Lake $(LEANMAKE_OPTS) OUT="../${LIB}" LIB_OUT="../${LIB}/lean" TEMP_OUT="../${LIB}/temp" OLEAN_OUT="../${LIB}/lean" EXTRA_SRC_ROOTS=LakeMain.lean + +"${LEAN_BIN}/leanmake" -C lake lib lib.export ../${LIB}/temp/LakeMain.o.export PKG=Lake $(LEANMAKE_OPTS) OUT="../${LIB}" LIB_OUT="../${LIB}/lean" TEMP_OUT="../${LIB}/temp" OLEAN_OUT="../${LIB}/lean" LEAN_OPTS+="--plugin=${PREV_STAGE}/${CMAKE_RELATIVE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}" EXTRA_SRC_ROOTS=LakeMain.lean ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX} ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_1${CMAKE_SHARED_LIBRARY_SUFFIX} ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX} ${LIB}/temp/libLean.a.export ${LIB}/temp/libLake.a.export @echo "[ ] Building $@"