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

chore: simplify stdlib.make.in

Browse source
This commit is contained in:
Sebastian Ullrich 2020-05-27 19:42:44 +02:00
parent 50fc961037
commit 8227eea87b
1 changed files with 17 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

46
src/stdlib.make.in
View file

@ -1,34 +1,22 @@
SHELL := /usr/bin/env bash -euo pipefail
# MORE_DEPS: rebuild the stdlib whenever the compiler has changed
LEANMAKE_OPTS=\
OUT="${LIB}"\
LIB_OUT="${LIB}/lean"\
OLEAN_OUT="${LIB}/lean"\
LEANC_OPTS="${LEANC_OPTS}"\
MORE_DEPS="${LEAN_BIN}/lean${CMAKE_EXECUTABLE_SUFFIX}"
stdlib:
# (I don't know how to add comments inside a multiline rule, so all comments go first)
# Use `+` to use the Make jobserver with `leanmake` for parallelized builds
ifeq "${STAGE}" "0.5"
# In the case of stage 0.5, we simply hardlink .olean files and libInit.a from stage 0 (but not libleancpp.a,
# which is different from stage 0).
# Otherwise, we build the library with `leanmake`. We rebuild it (`MORE_DEPS`) whenever the compiler has changed.
+if [ ${STAGE} == 0.5 ]; then\
mkdir -p "${LIB}/lean";\
cp -rf $$(find "${PREV_STAGE}/lib/lean" -mindepth 1 -maxdepth 1 -not -name libleancpp.a) "${LIB}/lean";\
else\
"${LEAN_BIN}/leanmake" lib\
PKG=Init\
"OUT=${LIB}"\
"LIB_OUT=${LIB}/lean"\
"OLEAN_OUT=${LIB}/lean"\
"LEANC_OPTS=${LEANC_OPTS}"\
"MORE_DEPS=${LEAN_BIN}/lean${CMAKE_EXECUTABLE_SUFFIX}";\
"${LEAN_BIN}/leanmake" lib\
PKG=Std\
"OUT=${LIB}"\
"LIB_OUT=${LIB}/lean"\
"OLEAN_OUT=${LIB}/lean"\
"LEANC_OPTS=${LEANC_OPTS}"\
"MORE_DEPS=${LEAN_BIN}/lean${CMAKE_EXECUTABLE_SUFFIX}";\
"${LEAN_BIN}/leanmake" lib\
PKG=Lean\
"OUT=${LIB}"\
"LIB_OUT=${LIB}/lean"\
"OLEAN_OUT=${LIB}/lean"\
"LEANC_OPTS=${LEANC_OPTS}"\
"MORE_DEPS=${LEAN_BIN}/lean${CMAKE_EXECUTABLE_SUFFIX}";\
fi
mkdir -p "${LIB}/lean"
cp -rf $$(find "${PREV_STAGE}/lib/lean" -mindepth 1 -maxdepth 1 -not -name libleancpp.a) "${LIB}/lean"
else
# Use `+` to use the Make jobserver with `leanmake` for parallelized builds
+"${LEAN_BIN}/leanmake" lib PKG=Init $(LEANMAKE_OPTS)
+"${LEAN_BIN}/leanmake" lib PKG=Std $(LEANMAKE_OPTS)
+"${LEAN_BIN}/leanmake" lib PKG=Lean $(LEANMAKE_OPTS)
endif