lean4-htt/src/stdlib.make.in
Sebastian Ullrich f73fca1da7 chore: make_stdlib: use everything but lean from the current stage
Finally the stage 1 stdlib will be built against the headers in src/, not stage0/src/
2020-09-24 18:57:53 +02:00

17 lines
611 B
Text

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="${PREV_STAGE}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}"\
CMAKE_LIKE_OUTPUT=1
stdlib:
# 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)