lean4-htt/src/stdlib.make.in
2021-01-25 15:24:16 +01:00

28 lines
1.1 KiB
Text

SHELL := /usr/bin/env bash -euo pipefail
# any absolute path to the stdlib breaks the Makefile
LEAN_PATH=
# link GMP statically if STATIC=ON
LEANC_GMP="${GMP_LIBRARIES}"
# 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=\
LEAN="${PREV_STAGE}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}"\
OUT="${LIB}"\
LIB_OUT="${LIB}/lean"\
OLEAN_OUT="${LIB}/lean"\
BIN_OUT="${CMAKE_BINARY_DIR}/bin"\
LEAN_OPTS+="${LEAN_EXTRA_MAKE_OPTS} -Dinterpreter.prefer_native=false"\
LEANC_OPTS+="${LEANC_OPTS}"\
LEAN_CXX="${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER}"\
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)
+"${LEAN_BIN}/leanmake" bin PKG=Leanpkg BIN_NAME=leanpkg $(LEANMAKE_OPTS) LINK_OPTS="${CMAKE_EXE_LINKER_FLAGS}"