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

chore: make_stdlib: use everything but lean from the current stage

Browse source 
Finally the stage 1 stdlib will be built against the headers in src/, not stage0/src/
This commit is contained in:
Sebastian Ullrich 2020-09-23 15:52:41 +02:00
parent c0d40c6f86
commit f73fca1da7
3 changed files with 12 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/CMakeLists.txt
View file

@ -533,10 +533,11 @@ else()
endif()
install(FILES ${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a DESTINATION lib/lean)
# MSYS2 bash usually handles Windows paths relatively well, but not when putting them in the PATH
string(REGEX REPLACE "^([a-zA-Z]):" "/\\1" LEAN_BIN "${CMAKE_BINARY_DIR}/bin")
# make stdlib using previous stage
if(PREV_STAGE)
# MSYS2 bash usually handles Windows paths relatively well, but not when putting them in the PATH
string(REGEX REPLACE "^([a-zA-Z]):" "/\\1" LEAN_BIN "${PREV_STAGE}/bin")
# ...and Make doesn't like absolute Windows paths either
# (also looks nicer in the build log)
file(RELATIVE_PATH LIB ${LEAN_SOURCE_DIR} ${CMAKE_BINARY_DIR}/lib)
@ -549,6 +550,7 @@ if(PREV_STAGE)
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)
add_library(Init STATIC IMPORTED)

10
src/lean.mk.in
View file

@ -10,6 +10,8 @@ ifndef PKG
endif
endif
LEAN = lean
LEANC = leanc
OUT = build
OLEAN_OUT = $(OUT)
TEMP_OUT = $(OUT)/temp
@ -47,14 +49,14 @@ $(TEMP_OUT)/%.depend: %.lean | $(OLEAN_OUT)/$(PKG)
@mkdir -p "$(TEMP_OUT)/$(*D)"
# use separate assignment to ensure failure propagation
# convert path separators and newlines on Windows
@deps=`lean --deps $< | tr '\\\\' / | tr -d '\\r'`; echo $(OLEAN_OUT)/$(<:.lean=.olean): $$deps > $@
@deps=`$(LEAN) --deps $< | tr '\\\\' / | tr -d '\\r'`; echo $(OLEAN_OUT)/$(<:.lean=.olean): $$deps > $@
$(OLEAN_OUT)/%.olean: %.lean $(TEMP_OUT)/%.depend $(MORE_DEPS)
ifdef CMAKE_LIKE_OUTPUT
@echo "[ ] Building $<"
endif
@mkdir -p $(OLEAN_OUT)/$(*D)
lean $(LEAN_OPTS) -o "$@" --c="$(TEMP_OUT)/$*.c.tmp" $<
$(LEAN) $(LEAN_OPTS) -o "$@" --c="$(TEMP_OUT)/$*.c.tmp" $<
# create the .c file atomically
mv "$(TEMP_OUT)/$*.c.tmp" "$(TEMP_OUT)/$*.c"
# make sure the .olean file is newer than the .depend file to prevent infinite make cycles
@ -71,7 +73,7 @@ endif
ifdef PROFILE
\time -f "%U %S" leanc -c -o $@ $< $(LEANC_OPTS) 2>&1 > /dev/null | awk '{ printf "C compilation %fs\n", $$1 + $$2 }' > /dev/stderr
else
leanc -c -o $@ $< $(LEANC_OPTS)
$(LEANC) -c -o $@ $< $(LEANC_OPTS)
endif
$(BIN_OUT)/$(BIN_NAME): $(addprefix $(TEMP_OUT)/,$(SRCS:.lean=.o)) | $(BIN_OUT)
@ -81,7 +83,7 @@ endif
ifdef PROFILE
\time -f "%U %S" leanc -o "$@" -x none $^ $(LINK_OPTS) 2>&1 > /dev/null | awk '{ printf "C linking %fs\n", $$1 + $$2 }' > /dev/stderr
else
leanc -o "$@" -x none $^ $(LINK_OPTS)
$(LEANC) -o "$@" -x none $^ $(LINK_OPTS)
endif
$(LIB_OUT)/$(STATIC_LIB_NAME): $(addprefix $(TEMP_OUT)/,$(SRCS:.lean=.o)) | $(LIB_OUT)

3
src/stdlib.make.in
View file

@ -2,11 +2,12 @@ SHELL := /usr/bin/env bash -euo pipefail
# MORE_DEPS: rebuild the stdlib whenever the compiler has changed
LEANMAKE_OPTS+=\
LEAN="${PREV_STAGE}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}"\
OUT="${LIB}"\
LIB_OUT="${LIB}/lean"\
OLEAN_OUT="${LIB}/lean"\
LEANC_OPTS="${LEANC_OPTS}"\
MORE_DEPS="${LEAN_BIN}/lean${CMAKE_EXECUTABLE_SUFFIX}"\
MORE_DEPS="${PREV_STAGE}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}"\
CMAKE_LIKE_OUTPUT=1
stdlib: