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

chore: fix passing additional LEAN(C)_OPTS to make

Browse source
This commit is contained in:
Sebastian Ullrich 2020-10-22 12:00:39 +02:00
parent 4e74e36331
commit ce96fab8de
2 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/stdlib.make.in
View file

@ -2,14 +2,14 @@ SHELL := /usr/bin/env bash -euo pipefail
# 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+=\
LEANMAKE_OPTS=\
LEAN="${PREV_STAGE}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}"\
OUT="${LIB}"\
LIB_OUT="${LIB}/lean"\
OLEAN_OUT="${LIB}/lean"\
LEAN_OPTS="${LEAN_EXTRA_MAKE_OPTS} -Dinterpreter.prefer_native=false"\
LEANC_OPTS="${LEANC_OPTS}"\
MORE_DEPS="${PREV_STAGE}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}"\
LEAN_OPTS+="${LEAN_EXTRA_MAKE_OPTS} -Dinterpreter.prefer_native=false"\
LEANC_OPTS+="${LEANC_OPTS}"\
MORE_DEPS+="${PREV_STAGE}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}"\
CMAKE_LIKE_OUTPUT=1
stdlib:

2
tests/bench/speedcenter.exec.velcom.yaml
View file

@ -11,7 +11,7 @@
run_config:
<<: *time
cmd: |
bash -c 'bench=$PWD; cd ${BUILD:-../../build/release}/stage1; find lib/lean ! -name libleancpp.a -delete; LEANMAKE_OPTS=LEAN_OPTS="--stats\ -Dprofiler=true\ -Dprofiler.threshold=9999" make -O -j5 make_stdlib 2>&1 > /dev/null | $bench/accumulate_profile.py'
bash -c 'bench=$PWD; cd ${BUILD:-../../build/release}/stage1; find lib/lean ! -name libleancpp.a -delete; LEAN_OPTS="--stats -Dprofiler=true -Dprofiler.threshold=9999" make -O -j5 make_stdlib 2>&1 > /dev/null | $bench/accumulate_profile.py'
max_runs: 2
parse_output: true
# Warmup. Somehow ccache doesn't reuse the cache from the original build? Weird.