diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 09a7134e08..cb0b0cdd01 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -684,12 +684,17 @@ if (LLVM AND ${STAGE} GREATER 0) set(EXTRA_LEANMAKE_OPTS "LLVM=1") endif() +set(STDLIBS Init Std Lean Leanc) +if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten") + list(APPEND STDLIBS Lake) +endif() + add_custom_target(make_stdlib ALL WORKING_DIRECTORY ${LEAN_SOURCE_DIR} # The actual rule is in a separate makefile because we want to prefix it with '+' to use the Make job server # for a parallelized nested build, but CMake doesn't let us do that. # We use `lean` from the previous stage, but `leanc`, headers, etc. from the current stage - COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Init Std Lean Leanc + COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make ${STDLIBS} VERBATIM) # if we have LLVM enabled, then build `lean.h.bc` which has the LLVM bitcode @@ -733,14 +738,9 @@ else() endif() if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten") - add_custom_target(lake_lib - WORKING_DIRECTORY ${LEAN_SOURCE_DIR} - DEPENDS leanshared - COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Lake - VERBATIM) add_custom_target(lake_shared WORKING_DIRECTORY ${LEAN_SOURCE_DIR} - DEPENDS lake_lib + DEPENDS leanshared COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make libLake_shared VERBATIM) add_custom_target(lake ALL diff --git a/src/stdlib.make.in b/src/stdlib.make.in index 4e12a3ae00..920ca6397d 100644 --- a/src/stdlib.make.in +++ b/src/stdlib.make.in @@ -64,7 +64,7 @@ ifneq "${STAGE}" "0" +"${LEAN_BIN}/leanmake" -C "${CMAKE_BINARY_DIR}/leanc" lib PKG=Leanc $(LEANMAKE_OPTS) OUT="${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}" LIB_OUT="${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}" OLEAN_OUT="${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}" endif -Lake: +Lake: Lean # 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