fix: benchmarks CI

This commit is contained in:
Sebastian Ullrich 2020-05-08 15:27:38 +02:00
parent 984fec7387
commit 9476ee2f54
2 changed files with 5 additions and 5 deletions

View file

@ -100,7 +100,7 @@ jobs:
run: nix-shell --run "cd build; make -j4 check-stage3"
if: matrix.check-stage3
- name: Test Speedcenter Benchmarks
run: nix-shell --run "cd tests/bench; PATH=../../bin:$PATH temci exec --config speedcenter.yaml --runs 1"
run: PATH=$(realpath build/stage1/bin):$PATH nix-shell --run 'cd tests/bench; temci exec --config speedcenter.yaml --runs 1'
if: matrix.test-speedcenter
- name: CCache stats
run: nix-shell --run "ccache -s"

View file

@ -11,7 +11,7 @@
<<: *time
cwd: ../../src
cmd: |
bash -c "find . -name '*.lean' -exec ../bin/lean --stats -Dprofiler=true -Dprofiler.threshold=9999 {} \; 2>&1 | ../tests/bench/accumulate_profile.py"
bash -c "find . -name '*.lean' -exec lean --stats -Dprofiler=true -Dprofiler.threshold=9999 {} \; 2>&1 | ../tests/bench/accumulate_profile.py"
max_runs: 3
parse_output: true
- attributes:
@ -25,7 +25,7 @@
echo -n 'lines: ' &&
find src -name '*.lean' -print0 | wc -l --files0-from=- | tail -1 | cut -d' ' -f 1
echo -n 'bytes .olean: ' &&
find src -name '*.olean' -print0 | wc -c --files0-from=- | tail -1 | cut -d' ' -f 1
find $(dirname $(which lean))/../lib/lean -name '*.olean' -print0 | wc -c --files0-from=- | tail -1 | cut -d' ' -f 1
echo -n 'lines C++: ' &&
find src \( -name '*.h' -o -name '*.cpp' \) -print0 | wc -l --files0-from=- | tail -1 | cut -d' ' -f 1
"
@ -38,7 +38,7 @@
cmd: |
set -eu
echo -n 'binary size: '
wc -c ../../bin/lean | cut -d' ' -f 1
wc -c $(which lean) | cut -d' ' -f 1
max_runs: 1
runner: output
- attributes:
@ -62,7 +62,7 @@
set -euxo pipefail
ulimit -s unlimited
for f in *.args; do
../../bin/lean --run ${f%.args} $(cat $f)
lean --run ${f%.args} $(cat $f)
done
'
max_runs: 5