chore: avoid calling into lake twice from CMake build (#9688)

Keeps the output cleaner and save a little time and potential
re-rebuilds
This commit is contained in:
Sebastian Ullrich 2025-08-02 22:48:45 +02:00 committed by GitHub
parent 1e83f62d31
commit 77646f7149
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 8 additions and 8 deletions

View file

@ -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

View file

@ -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