| # LEAN_BASH: Makes the Bash shell used by the Lean build configurable. | |
| # On Windows, when CMake/Make is spawned directly (e.g., VSCode's CMake Tools), | |
| # it lacks a proper shell environment, so we need to manually point it to Bash. | |
| LEAN_BASH ?= /usr/bin/env bash | |
| SHELL := $(LEAN_BASH) -eo pipefail | |
| # any absolute path to the stdlib breaks the Makefile | |
| export LEAN_PATH= | |
| export LEAN_CC=${CMAKE_C_COMPILER_LAUNCHER} ${CMAKE_C_COMPILER} | |
| export LEAN_ABORT_ON_PANIC=1 | |
| # LEAN_OPTS: don't use native code (except for primitives) since it is from the previous stage | |
| # MORE_DEPS: rebuild the stdlib whenever the compiler has changed | |
| LEANMAKE_OPTS=\ | |
| LEAN="${PREV_STAGE}/bin/lean${PREV_STAGE_CMAKE_EXECUTABLE_SUFFIX}"\ | |
| LEANC="${CMAKE_BINARY_DIR}/leanc.sh"\ | |
| OUT="${LIB}"\ | |
| LIB_OUT="${LIB}/lean"\ | |
| OLEAN_OUT="${LIB}/lean"\ | |
| BIN_OUT="${CMAKE_BINARY_DIR}/bin"\ | |
| LEAN_OPTS+="${LEAN_EXTRA_MAKE_OPTS}"\ | |
| LEANC_OPTS+="${LEANC_OPTS}"\ | |
| LEAN_AR="${CMAKE_AR}"\ | |
| MORE_DEPS+="${PREV_STAGE}/bin/lean${PREV_STAGE_CMAKE_EXECUTABLE_SUFFIX}"\ | |
| ${EXTRA_LEANMAKE_OPTS}\ | |
| CMAKE_LIKE_OUTPUT=1 | |
| ifeq "${STAGE}" "0" | |
| LEANMAKE_OPTS+=C_ONLY=1 C_OUT=${LEAN_SOURCE_DIR}/../stdlib/ | |
| endif | |
| .PHONY: Init Std Lean leanshared Lake lean | |
| # These can be phony since the inner Makefile will have the correct dependencies and avoid rebuilds | |
| Init: | |
| @mkdir -p "${LIB}/lean/Lean" "${LIB}/lean/Lake" "${LIB}/lean/Std" | |
| # Use `+` to use the Make jobserver with `leanmake` for parallelized builds | |
| # Build `.olean/.o`s of downstream libraries as well for better parallelism | |
| +"${LEAN_BIN}/leanmake" objs lib lib.export PKG=Init $(LEANMAKE_OPTS) \ | |
| EXTRA_SRC_ROOTS="Std Std.lean Lean Lean.lean" | |
| Std: Init | |
| +"${LEAN_BIN}/leanmake" lib lib.export PKG=Std $(LEANMAKE_OPTS) | |
| Lean: Std | |
| +"${LEAN_BIN}/leanmake" lib lib.export PKG=Lean $(LEANMAKE_OPTS) | |
| ${LIB}/temp/empty.c: | |
| touch $@ | |
| # the following targets are all invoked by separate `make` calls; see src/CMakeLists.txt | |
| # we specify the precise file names here to avoid rebuilds | |
| ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX}: ${LIB}/temp/libInit.a.export ${LIB}/temp/libStd.a.export ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LIB}/temp/empty.c | |
| @echo "[ ] Building $@" | |
| ifeq "${CMAKE_SYSTEM_NAME}" "Windows" | |
| # on Windows, must remove file before writing a new one (since the old one may be in use) | |
| @rm -f $@ | |
| "${CMAKE_BINARY_DIR}/leanc.sh" -shared -o $@ \ | |
| -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libInit.a.export ${CMAKE_BINARY_DIR}/lib/temp/libStd.a.export ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a -Wl,--no-whole-archive \ | |
| -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libInit_shared.dll.a ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS} | |
| else | |
| # create empty library on platforms without restrictive symbol limits; avoids costly indirections and troubles with cross-library exceptions | |
| "${CMAKE_BINARY_DIR}/leanc.sh" -shared -o $@ ${LIB}/temp/empty.c ${INIT_SHARED_LINKER_FLAGS} ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS} | |
| endif | |
| Init_shared: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX} | |
| ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX} ${LIB}/temp/libLean.a.export ${LIB}/lean/libleancpp.a ${LIB}/temp/libleanshell.a ${LIB}/temp/libleaninitialize.a | |
| @echo "[ ] Building $@" | |
| ifeq "${CMAKE_SYSTEM_NAME}" "Windows" | |
| # on Windows, must remove file before writing a new one (since the old one may be in use) | |
| @rm -f ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_1${CMAKE_SHARED_LIBRARY_SUFFIX} | |
| # "half-way point" DLL to avoid symbol limit | |
| # include Lean.Meta.WHNF and leancpp except for `initialize.cpp` | |
| "${CMAKE_BINARY_DIR}/leanc.sh" -shared -o ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_1${CMAKE_SHARED_LIBRARY_SUFFIX} \ | |
| ${LIB}/temp/Lean/Meta/WHNF.o.export -Wl,--start-group ${LIB}/temp/libLean.a.export -Wl,--whole-archive ${LIB}/temp/libleancpp_1.a -Wl,--no-whole-archive -Wl,--end-group -lInit_shared -Wl,--out-implib,${LIB}/lean/libleanshared_1.dll.a ${LEANSHARED_LINKER_FLAGS} ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS} -Wl,-Map=${LIB}/temp/libleanshared_1.map | |
| # now delete included symbols from libLean.a | |
| cp ${LIB}/temp/libLean.a.export ${LIB}/temp/diff.a | |
| sed -En 's/.*\s(\S*\.o\.export):.*/\1/p' ${LIB}/temp/libleanshared_1.map > ${LIB}/temp/diff.a.in | |
| # can't use bundled llvm-ar before LLVM 16, https://github.com/llvm/llvm-project/issues/55023 | |
| ar dP ${LIB}/temp/diff.a @${LIB}/temp/diff.a.in | |
| "${CMAKE_AR}" tP ${LIB}/temp/diff.a | |
| # now include Lean and the diff library in `leanshared` | |
| "${CMAKE_BINARY_DIR}/leanc.sh" -shared -o $@ \ | |
| -Wl,--whole-archive ${LIB}/temp/diff.a ${LIB}/temp/libleanshell.a ${LIB}/temp/libleaninitialize.a -Wl,--no-whole-archive -lleanshared_1 -lInit_shared -Wl,--out-implib,${LIB}/lean/libleanshared.dll.a ${LEANSHARED_LINKER_FLAGS} ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS} | |
| else | |
| # create empty library on platforms without restrictive symbol limits; avoids costly indirections and troubles with cross-library exceptions | |
| "${CMAKE_BINARY_DIR}/leanc.sh" -shared -o ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_1${CMAKE_SHARED_LIBRARY_SUFFIX} ${LIB}/temp/empty.c ${LEANSHARED_1_LINKER_FLAGS} ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS} | |
| ifeq "${CMAKE_SYSTEM_NAME}" "Darwin" | |
| "${CMAKE_BINARY_DIR}/leanc.sh" -shared -o $@ \ | |
| ${LIB}/temp/Lean.o -Wl,-force_load,${LIB}/temp/libleanshell.a -lInit -lStd -lLean -lleancpp ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS} ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS} | |
| else | |
| "${CMAKE_BINARY_DIR}/leanc.sh" -shared -o $@ \ | |
| -Wl,--whole-archive ${LIB}/temp/Lean.o ${LIB}/temp/libleanshell.a -Wl,--no-whole-archive -Wl,--start-group -lInit -lStd -lLean -lleancpp -Wl,--end-group ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS} ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS} | |
| endif | |
| endif | |
| leanshared: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX} | |
| Lake: | |
| # lake is in its own subdirectory, so must adjust relative paths... | |
| +"${LEAN_BIN}/leanmake" -C lake bin lib PKG=Lake BIN_NAME=lake${CMAKE_EXECUTABLE_SUFFIX} $(LEANMAKE_OPTS) LINK_OPTS='${CMAKE_EXE_LINKER_FLAGS_MAKE_MAKE}' OUT="../${LIB}" LIB_OUT="../${LIB}/lean" OLEAN_OUT="../${LIB}/lean" | |
| ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX} ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX} ${LIB}/temp/libleanmain.a | |
| @echo "[ ] Building $@" | |
| # on Windows, must remove file before writing a new one (since the old one may be in use) | |
| @rm -f $@ | |
| "${CMAKE_BINARY_DIR}/leanc.sh" ${LIB}/temp/libleanmain.a ${CMAKE_EXE_LINKER_FLAGS_MAKE} ${LEAN_EXE_LINKER_FLAGS} ${LEANC_OPTS} -o $@ | |
| lean: ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX} | |
| Leanc: | |
| +"${LEAN_BIN}/leanmake" bin PKG=Leanc BIN_NAME=leanc${CMAKE_EXECUTABLE_SUFFIX} $(LEANMAKE_OPTS) LINK_OPTS='${CMAKE_EXE_LINKER_FLAGS_MAKE_MAKE}' OUT="${CMAKE_BINARY_DIR}" OLEAN_OUT="${CMAKE_BINARY_DIR}" |