max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: staged CMake build with Lake as a plugin (#6929)

Browse source 
This PR passes the shared library of the previous stage's Lake as a
plugin to the next stage's Lake in the CMake build. This enables Lake to
use its own builtin elaborators / initializers at build time.
This commit is contained in:
Mac Malone 2025-02-20 23:03:50 -05:00 • committed by GitHub
parent 6c609028b3
commit 36c798964e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 5 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/CMakeLists.txt
View file

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

4
src/stdlib.make.in
View file

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