lean4/stage0/src/stdlib.make.in

# 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=
ifeq "${USE_LAKE}" "ON"
  export LEAN_CC=${CMAKE_C_COMPILER}
else
  export LEAN_CC=${CMAKE_C_COMPILER_LAUNCHER} ${CMAKE_C_COMPILER}
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

# 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

# These can be phony since the inner Makefile/Lake will have the correct dependencies and avoid rebuilds
.PHONY: Init Std Lean leanshared Lake libLake_shared lake lean LeanChecker leanchecker

ifeq "${USE_LAKE}" "ON"

# build in parallel
Init:
	${PREV_STAGE}/bin/lake build -f ${CMAKE_BINARY_DIR}/lakefile.toml $(LAKE_EXTRA_ARGS)

Std Lean Lake Leanc LeanChecker: Init

else

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)

Leanc: Lean
ifneq "${STAGE}" "0"
	+"${LEAN_BIN}/leanmake" -C "${CMAKE_BINARY_DIR}/leanc" lib PKG=Leanc $(LEANMAKE_OPTS) OUT="$(OUTARC)" LIB_OUT="$(OUTARC)" OLEAN_OUT="$(OUTARC)"
endif

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

LeanChecker: Lake
	+"${LEAN_BIN}/leanmake" lib PKG=LeanChecker $(LEANMAKE_OPTS) OUT="$(OUTARC)" LIB_OUT="$(OUTARC)" TEMP_OUT="${LIB}/temp" OLEAN_OUT="$(OUTARC)"

endif

${LIB}/temp/empty.c:
	touch $@

# the following targets are all invoked by separate `make` calls; see src/CMakeLists.txt

# Lake archive timestamps may be stale due to caching; use .trace files for rebuild decisions
ifeq "${USE_LAKE}" "ON"
$(OUTLIB)/libInit_shared$(SO): ${LIB}/lean/libInit.a.export.trace ${LIB}/lean/libStd.a.export.trace
$(OUTLIB)/libleanshared$(SO): ${LIB}/lean/libLean.a.export.trace
$(OUTLIB)/libLake_shared$(SO): ${LIB}/lean/libLean.a.export.trace ${LIB}/lean/libLake.a.export.trace
$(OUTBIN)/lake$(EXE): ${LIB}/temp/LakeMain.c.o.export.trace
$(OUTBIN)/leanc$(EXE): $(OUTARC)/libLeanc.a.trace
$(OUTBIN)/leanchecker$(EXE): $(OUTARC)/libLeanChecker.a.trace
endif

# we specify the precise file names here to avoid rebuilds
$(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"
	$(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
# 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: $(OUTLIB)/libInit_shared$(SO)

$(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"
	@rm -f $(OUTLIB)/libleanshared_1$(SO)
	@rm -f $(OUTLIB)/libleanshared_2$(SO)
# initial DLL to avoid symbol limit: include leancpp except for `initialize.cpp`
	$(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 "$(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
# can't use bundled llvm-ar before LLVM 16, https://github.com/llvm/llvm-project/issues/55023
	ar dP ${LIB}/lean/diff.a @${LIB}/temp/diff.a.in
	#"${CMAKE_AR}" tP ${LIB}/lean/diff.a
# now again up to `Lean.Meta`
	$(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 "$(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`
	$(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 "$(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
	$(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"
	$(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
	$(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
ifeq "${CMAKE_BUILD_TYPE}" "Release"
ifeq "${CMAKE_SYSTEM_NAME}" "Linux"
# We only strip like this on Linux for now as our other platforms already seem to exclude the
# unexported symbols by default
	strip --strip-unneeded $@
endif
endif

leanshared: $(OUTLIB)/libleanshared$(SO)

$(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: $(OUTLIB)/libLake_shared$(SO)

$(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: $(OUTBIN)/lake$(EXE)

$(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: $(OUTBIN)/lean$(EXE)

$(OUTBIN)/leanc$(EXE): $(OUTARC)/libLeanc.a
	$(link-preamble)
	$(LEANC_SH) $< ${CMAKE_EXE_LINKER_FLAGS_MAKE} ${LEAN_EXE_LINKER_FLAGS} ${LEANC_OPTS} -o $@

leanc: $(OUTBIN)/leanc$(EXE)

$(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: $(OUTBIN)/leanchecker$(EXE)