chore(tests/bench/speedcenter.exec.yaml): simplify 'stdlib' benchmark

@leodemoura This removes the need for `--output-sync` and cmake hackery. It
doesn't quite measure actual `make stdlib` times (no parallelization, no
.olean/.cpp/.o output), but all of these actually seem to be negligible.
This commit is contained in:
Sebastian Ullrich 2019-07-05 10:51:44 +02:00
parent ea6eee516b
commit 2d60a4eb50

View file

@ -9,13 +9,9 @@
# properties: ['cache-misses', 'wall-clock']
run_config:
<<: *time
cwd: ../../build/release/
cwd: ../../library
cmd: |
bash -c "
set -euo pipefail &&
cmake . -DLEAN_EXTRA_MAKE_OPTS='-Dprofiler=true -Dprofiler.threshold=9999' >&2 &&
cmake --build . --target clean-olean >&2 &&
cmake --build . --target stdlib 2>&1 | ../../tests/bench/accumulate_profile.py"
bash -c "find . -name '*.lean' -exec ../bin/lean -Dprofiler=true -Dprofiler.threshold=9999 {} \; 2>&1 | ../tests/bench/accumulate_profile.py"
max_runs: 3
parse_output: true
- attributes: