chore: remove old speedcenter config

.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

tests/bench/speedcenter.exec.yaml

@@ -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

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]