43 lines
1.6 KiB
Text
43 lines
1.6 KiB
Text
SHELL := /usr/bin/env bash -euo pipefail
|
|
|
|
# any absolute path to the stdlib breaks the Makefile
|
|
export LEAN_PATH=
|
|
|
|
# link GMP statically if STATIC=ON
|
|
export 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="${CMAKE_CROSSCOMPILING_EMULATOR} ${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}"\
|
|
LEANC_OPTS+="${LEANC_OPTS}"\
|
|
LEAN_CXX="${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER}"\
|
|
LEAN_AR="${CMAKE_AR}"\
|
|
MORE_DEPS+="${PREV_STAGE}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}"\
|
|
CMAKE_LIKE_OUTPUT=1\
|
|
$(MORE_LEANMAKE_OPTS)
|
|
|
|
.PHONY: Init Std Lean leanshared Leanpkg
|
|
|
|
Init:
|
|
# Use `+` to use the Make jobserver with `leanmake` for parallelized builds
|
|
+"${LEAN_BIN}/leanmake" lib PKG=Init $(LEANMAKE_OPTS)
|
|
|
|
Std: Init
|
|
+"${LEAN_BIN}/leanmake" lib PKG=Std $(LEANMAKE_OPTS)
|
|
|
|
Lean: Init Std
|
|
+"${LEAN_BIN}/leanmake" lib PKG=Lean $(LEANMAKE_OPTS)
|
|
|
|
leanshared: Init Std Lean
|
|
@mkdir -p "${CMAKE_LIBRARY_OUTPUT_DIRECTORY}" || true
|
|
# can't use leanc here since it would try to link against leanshared
|
|
${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER} -shared -o "${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}" ${LEANSHARED_LINKER_FLAGS} ${LEANC_GMP} -L${LIB}/lean
|
|
|
|
Leanpkg: Init Std Lean leanshared
|
|
+"${LEAN_BIN}/leanmake" bin PKG=Leanpkg BIN_NAME=leanpkg${CMAKE_EXECUTABLE_SUFFIX} $(LEANMAKE_OPTS) LINK_OPTS='-lleanshared ${CMAKE_EXE_LINKER_FLAGS_MAKE}'
|