diff --git a/src/stdlib.make.in b/src/stdlib.make.in index cb89fa36d4..89451f813f 100644 --- a/src/stdlib.make.in +++ b/src/stdlib.make.in @@ -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: diff --git a/tests/bench/speedcenter.exec.velcom.yaml b/tests/bench/speedcenter.exec.velcom.yaml index 94debf3212..5345bd944f 100644 --- a/tests/bench/speedcenter.exec.velcom.yaml +++ b/tests/bench/speedcenter.exec.velcom.yaml @@ -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.