diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index d1e7aa37db..eac2b0a342 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -116,6 +116,7 @@ jobs: if: matrix.check-stage3 - name: Test Speedcenter Benchmarks run: | + echo -1 | sudo tee /proc/sys/kernel/perf_event_paranoid export BUILD=$PWD/build PATH=$PWD/build/stage1/bin:$PATH cd tests/bench; temci exec --config speedcenter.yaml --included_blocks fast --runs 1 if: matrix.test-speedcenter diff --git a/tests/bench/speedcenter.exec.yaml b/tests/bench/speedcenter.exec.yaml deleted file mode 100644 index 6e50bcbfce..0000000000 --- a/tests/bench/speedcenter.exec.yaml +++ /dev/null @@ -1,143 +0,0 @@ -- attributes: - description: stdlib - tags: [slow] - time: &time - runner: time - # alternative config: use `perf stat` for extended properties - #runner: perf_stat - #perf_stat: - # properties: ['cache-misses', 'wall-clock'] - run_config: - <<: *time - cmd: | - bash -c 'bench=$PWD; cd ${BUILD:-../../build/release}/stage0; 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' - max_runs: 2 - parse_output: true - # Warmup. Somehow ccache doesn't reuse the cache from the original build? Weird. - build_config: - cmd: | - bash -c 'cd ${BUILD:-../../build/release}/stage0; find lib/lean/ ! -name libleancpp.a -type f -delete; make -j5 make_stdlib' -- attributes: - description: stdlib size - tags: [deterministic, fast] - run_config: - cwd: ../../ - cmd: | - bash -c " - set -euxo pipefail && - echo -n 'lines: ' && - find src -name '*.lean' -print0 | wc -l --files0-from=- | tail -1 | cut -d' ' -f 1 - echo -n 'bytes .olean: ' && - 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 - " - max_runs: 1 - runner: output -- attributes: - description: bin/lean - tags: [deterministic, fast] - run_config: - cmd: | - set -eu - echo -n 'binary size: ' - wc -c $(which lean) | cut -d' ' -f 1 - max_runs: 1 - runner: output -- attributes: - description: tests/compiler - tags: [deterministic, slow] - run_config: - cwd: ../compiler/ - cmd: | - set -eu - printf 'sum binary sizes: ' - for f in *.lean; do ../bench/compile.sh $f; printf '%s\0' "$f.out"; done | wc -c --files0-from=- | tail -1 | cut -d' ' -f 1 - max_runs: 1 - runner: output -- attributes: - description: tests/bench/ interpreted - tags: [slow] - run_config: - <<: *time - cmd: | - bash -c ' - set -euxo pipefail - ulimit -s unlimited - for f in *.args; do - lean --run ${f%.args} $(cat $f) - done - ' - max_runs: 5 -- attributes: - description: binarytrees - tags: [fast, suite] - run_config: - <<: *time - cmd: ./binarytrees.lean.out 21 - build_config: - cmd: ./compile.sh binarytrees.lean -- attributes: - description: deriv - tags: [fast, suite] - run_config: - <<: *time - cmd: ./deriv.lean.out 10 - build_config: - cmd: ./compile.sh deriv.lean -- attributes: - description: const_fold - tags: [fast, suite] - run_config: - <<: *time - cmd: bash -c "ulimit -s unlimited && ./const_fold.lean.out 23" - build_config: - cmd: ./compile.sh const_fold.lean -- attributes: - description: new parser Core.lean - tags: [fast, suite] - run_config: - <<: *time - cmd: ./parser.lean.out ../../src/Init/Core.lean 100 - build_config: - cmd: ./compile.sh parser.lean -- attributes: - description: qsort - tags: [fast, suite] - run_config: - <<: *time - cmd: ./qsort.lean.out 400 - build_config: - cmd: ./compile.sh qsort.lean -- attributes: - description: rbmap - tags: [fast, suite] - run_config: - <<: *time - cmd: ./rbmap.lean.out 2000000 - build_config: - cmd: ./compile.sh rbmap.lean -- attributes: - description: rbmap_1 - tags: [fast, suite] - run_config: - <<: *time - cmd: ./rbmap_checkpoint.lean.out 2000000 1 - build_config: - cmd: ./compile.sh rbmap_checkpoint.lean -- attributes: - description: rbmap_10 - tags: [fast, suite] - run_config: - <<: *time - cmd: ./rbmap_checkpoint.lean.out 2000000 10 - build_config: - cmd: ./compile.sh rbmap_checkpoint.lean -- attributes: - description: unionfind - tags: [fast, suite] - run_config: - <<: *time - cmd: ./unionfind.lean.out 3000000 - build_config: - cmd: ./compile.sh unionfind.lean diff --git a/tests/bench/speedcenter.yaml b/tests/bench/speedcenter.yaml index 432469cef8..91a6570c1f 100644 --- a/tests/bench/speedcenter.yaml +++ b/tests/bench/speedcenter.yaml @@ -246,7 +246,7 @@ run: driver: exec # Input file with the program blocks to benchmark - in: speedcenter.exec.yaml + in: speedcenter.exec.velcom.yaml # List of included run blocks (all: include all), or their tag attribute or their number in the file (starting with 0) included_blocks: [all]