chore: clean up stdlib.make.in (#12614)

This commit is contained in:
Sebastian Ullrich
2026-02-20 17:59:34 +01:00
committed by GitHub
parent 722813105d
commit 7b30214e54

View File

@@ -13,6 +13,21 @@ else
endif
export LEAN_ABORT_ON_PANIC=1
# Short aliases for verbose CMake variables
OUTLIB := ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}
OUTBIN := ${CMAKE_BINARY_DIR}/bin
OUTARC := ${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}
SO := ${CMAKE_SHARED_LIBRARY_SUFFIX}
EXE := ${CMAKE_EXECUTABLE_SUFFIX}
LEANC_SH := "${CMAKE_BINARY_DIR}/leanc.sh"
# Common preamble for link targets
define link-preamble
@echo "[ ] Building $@"
# on Windows, must remove file before writing a new one (since the old one may be in use)
@rm -f $@
endef
# 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=\
@@ -61,7 +76,7 @@ Lean: Std
Leanc: Lean
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}"
+"${LEAN_BIN}/leanmake" -C "${CMAKE_BINARY_DIR}/leanc" lib PKG=Leanc $(LEANMAKE_OPTS) OUT="$(OUTARC)" LIB_OUT="$(OUTARC)" OLEAN_OUT="$(OUTARC)"
endif
Lake: Lean
@@ -69,7 +84,7 @@ Lake: 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" EXTRA_SRC_ROOTS=LakeMain.lean
LeanChecker: Lake
+"${LEAN_BIN}/leanmake" lib PKG=LeanChecker $(LEANMAKE_OPTS) OUT="${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}" LIB_OUT="${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}" OLEAN_OUT="${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}"
+"${LEAN_BIN}/leanmake" lib PKG=LeanChecker $(LEANMAKE_OPTS) OUT="$(OUTARC)" LIB_OUT="$(OUTARC)" OLEAN_OUT="$(OUTARC)"
endif
@@ -79,33 +94,29 @@ ${LIB}/temp/empty.c:
# 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}/lean/libInit.a.export ${LIB}/lean/libStd.a.export ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LIB}/temp/empty.c
@echo "[ ] Building $@"
$(OUTLIB)/libInit_shared$(SO): ${LIB}/lean/libInit.a.export ${LIB}/lean/libStd.a.export ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LIB}/temp/empty.c
$(link-preamble)
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 $@ \
$(LEANC_SH) -shared -o $@ \
-Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/lean/libInit.a.export ${CMAKE_BINARY_DIR}/lib/lean/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}
# empty library on platforms without restrictive symbol limits; avoids costly indirections and troubles with cross-library exceptions
$(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}
Init_shared: $(OUTLIB)/libInit_shared$(SO)
${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX} ${LIB}/lean/libLean.a.export ${LIB}/lean/libleancpp.a ${LIB}/temp/libleanshell.a ${LIB}/temp/libleaninitialize.a
@echo "[ ] Building $@"
$(OUTLIB)/libleanshared$(SO): $(OUTLIB)/libInit_shared$(SO) ${LIB}/lean/libLean.a.export ${LIB}/lean/libleancpp.a ${LIB}/temp/libleanshell.a ${LIB}/temp/libleaninitialize.a
$(link-preamble)
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${CMAKE_SHARED_LIBRARY_SUFFIX}
@rm -f ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_1${CMAKE_SHARED_LIBRARY_SUFFIX}
@rm -f ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_2${CMAKE_SHARED_LIBRARY_SUFFIX}
@rm -f $(OUTLIB)/libleanshared_1$(SO)
@rm -f $(OUTLIB)/libleanshared_2$(SO)
# initial DLL to avoid symbol limit: include leancpp except for `initialize.cpp`
"${CMAKE_BINARY_DIR}/leanc.sh" -shared -o ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_1${CMAKE_SHARED_LIBRARY_SUFFIX} \
$(LEANC_SH) -shared -o $(OUTLIB)/libleanshared_1$(SO) \
-Wl,--start-group ${LIB}/lean/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
echo -n "${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_1${CMAKE_SHARED_LIBRARY_SUFFIX} symbols: "
nm ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_1${CMAKE_SHARED_LIBRARY_SUFFIX} --extern-only | wc -l
echo -n "$(OUTLIB)/libleanshared_1$(SO) symbols: "
nm $(OUTLIB)/libleanshared_1$(SO) --extern-only | wc -l
# now delete included symbols from libLean.a
cp ${LIB}/lean/libLean.a.export ${LIB}/lean/diff.a
sed -En 's/.*\s(\S*\.o\.export):.*/\1/p' ${LIB}/temp/libleanshared_1.map > ${LIB}/temp/diff.a.in
@@ -113,28 +124,28 @@ ifeq "${CMAKE_SYSTEM_NAME}" "Windows"
ar dP ${LIB}/lean/diff.a @${LIB}/temp/diff.a.in
#"${CMAKE_AR}" tP ${LIB}/lean/diff.a
# now again up to `Lean.Meta`
"${CMAKE_BINARY_DIR}/leanc.sh" -shared -o ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_2${CMAKE_SHARED_LIBRARY_SUFFIX} \
$(LEANC_SH) -shared -o $(OUTLIB)/libleanshared_2$(SO) \
${LIB}/lean/../temp/Lean/Meta.*o.export ${LIB}/lean/diff.a -Wl,--no-whole-archive -lleanshared_1 -lInit_shared -Wl,--out-implib,${LIB}/lean/libleanshared_2.dll.a ${LEANSHARED_LINKER_FLAGS} ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS} -Wl,-Map=${LIB}/temp/libleanshared_2.map
echo -n "${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_2${CMAKE_SHARED_LIBRARY_SUFFIX} symbols: "
nm ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_2${CMAKE_SHARED_LIBRARY_SUFFIX} --extern-only | wc -l
echo -n "$(OUTLIB)/libleanshared_2$(SO) symbols: "
nm $(OUTLIB)/libleanshared_2$(SO) --extern-only | wc -l
sed -En 's/.*\s(\S*\.o\.export):.*/\1/p' ${LIB}/temp/libleanshared_2.map > ${LIB}/temp/diff.a.in
ar dP ${LIB}/lean/diff.a @${LIB}/temp/diff.a.in
#"${CMAKE_AR}" tP ${LIB}/lean/diff.a
# now include `Lean` and the diff library in `leanshared`
"${CMAKE_BINARY_DIR}/leanc.sh" -shared -o $@ \
$(LEANC_SH) -shared -o $@ \
-Wl,--whole-archive ${LIB}/lean/diff.a ${LIB}/temp/libleanshell.a ${LIB}/temp/libleaninitialize.a -Wl,--no-whole-archive -lleanshared_2 -lleanshared_1 -lInit_shared -Wl,--out-implib,${LIB}/lean/libleanshared.dll.a ${LEANSHARED_LINKER_FLAGS} ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS}
echo -n "${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX} symbols: "
nm ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX} --extern-only | wc -l
echo -n "$(OUTLIB)/libleanshared$(SO) symbols: "
nm $(OUTLIB)/libleanshared$(SO) --extern-only | wc -l
rm ${LIB}/lean/diff.a
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}
"${CMAKE_BINARY_DIR}/leanc.sh" -shared -o ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_2${CMAKE_SHARED_LIBRARY_SUFFIX} ${LIB}/temp/empty.c ${LEANSHARED_2_LINKER_FLAGS} ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS}
$(LEANC_SH) -shared -o $(OUTLIB)/libleanshared_1$(SO) ${LIB}/temp/empty.c ${LEANSHARED_1_LINKER_FLAGS} ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS}
$(LEANC_SH) -shared -o $(OUTLIB)/libleanshared_2$(SO) ${LIB}/temp/empty.c ${LEANSHARED_2_LINKER_FLAGS} ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS}
ifeq "${CMAKE_SYSTEM_NAME}" "Darwin"
"${CMAKE_BINARY_DIR}/leanc.sh" -shared -o $@ \
$(LEANC_SH) -shared -o $@ \
${LIB}/temp/Lean.*o.export -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 $@ \
$(LEANC_SH) -shared -o $@ \
-Wl,--whole-archive ${LIB}/temp/Lean.*o.export ${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
@@ -146,45 +157,35 @@ ifeq "${CMAKE_SYSTEM_NAME}" "Linux"
endif
endif
leanshared: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}
leanshared: $(OUTLIB)/libleanshared$(SO)
${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_2${CMAKE_SHARED_LIBRARY_SUFFIX} ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_1${CMAKE_SHARED_LIBRARY_SUFFIX} ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX} ${LIB}/lean/libLean.a.export ${LIB}/lean/libLake.a.export
@echo "[ ] Building $@"
# on Windows, must remove file before writing a new one (since the old one may be in use)
@rm -f ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}
"${CMAKE_BINARY_DIR}/leanc.sh" -shared -o $@ \
$(OUTLIB)/libLake_shared$(SO): $(OUTLIB)/libInit_shared$(SO) $(OUTLIB)/libleanshared_2$(SO) $(OUTLIB)/libleanshared_1$(SO) $(OUTLIB)/libleanshared$(SO) ${LIB}/lean/libLean.a.export ${LIB}/lean/libLake.a.export
$(link-preamble)
$(LEANC_SH) -shared -o $@ \
${LAKESHARED_LINKER_FLAGS} -lleanshared -lleanshared_2 -lleanshared_1 -lInit_shared ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS}
libLake_shared: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}
libLake_shared: $(OUTLIB)/libLake_shared$(SO)
${CMAKE_BINARY_DIR}/bin/lake${CMAKE_EXECUTABLE_SUFFIX}: ${LIB}/temp/LakeMain.*o.export ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}
@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" $< -lLake_shared ${CMAKE_EXE_LINKER_FLAGS_MAKE} ${LEANC_OPTS} -o $@
$(OUTBIN)/lake$(EXE): ${LIB}/temp/LakeMain.*o.export $(OUTLIB)/libLake_shared$(SO)
$(link-preamble)
$(LEANC_SH) $< -lLake_shared ${CMAKE_EXE_LINKER_FLAGS_MAKE} ${LEANC_OPTS} -o $@
lake: ${CMAKE_BINARY_DIR}/bin/lake${CMAKE_EXECUTABLE_SUFFIX}
lake: $(OUTBIN)/lake$(EXE)
${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX} ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_2${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/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 $@
$(OUTBIN)/lean$(EXE): $(OUTLIB)/libInit_shared$(SO) $(OUTLIB)/libleanshared_2$(SO) $(OUTLIB)/libleanshared_1$(SO) $(OUTLIB)/libleanshared$(SO) ${LIB}/temp/libleanmain.a
$(link-preamble)
$(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}
lean: $(OUTBIN)/lean$(EXE)
${CMAKE_BINARY_DIR}/bin/leanc${CMAKE_EXECUTABLE_SUFFIX}: ${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}/libLeanc.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" $< ${CMAKE_EXE_LINKER_FLAGS_MAKE} ${LEAN_EXE_LINKER_FLAGS} ${LEANC_OPTS} -o $@
$(OUTBIN)/leanc$(EXE): $(OUTARC)/libLeanc.a
$(link-preamble)
$(LEANC_SH) $< ${CMAKE_EXE_LINKER_FLAGS_MAKE} ${LEAN_EXE_LINKER_FLAGS} ${LEANC_OPTS} -o $@
leanc: ${CMAKE_BINARY_DIR}/bin/leanc${CMAKE_EXECUTABLE_SUFFIX}
leanc: $(OUTBIN)/leanc$(EXE)
${CMAKE_BINARY_DIR}/bin/leanchecker${CMAKE_EXECUTABLE_SUFFIX}: ${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}/libLeanChecker.a ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}
@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" $< -lLake_shared ${CMAKE_EXE_LINKER_FLAGS_MAKE} ${LEAN_EXE_LINKER_FLAGS} ${LEANC_OPTS} -o $@
$(OUTBIN)/leanchecker$(EXE): $(OUTARC)/libLeanChecker.a $(OUTLIB)/libLake_shared$(SO)
$(link-preamble)
$(LEANC_SH) $< -lLake_shared ${CMAKE_EXE_LINKER_FLAGS_MAKE} ${LEAN_EXE_LINKER_FLAGS} ${LEANC_OPTS} -o $@
leanchecker: ${CMAKE_BINARY_DIR}/bin/leanchecker${CMAKE_EXECUTABLE_SUFFIX}
leanchecker: $(OUTBIN)/leanchecker$(EXE)