max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: include full build in stdlib benchmark (#3104)

Browse source
This commit is contained in:
Sebastian Ullrich 2023-12-23 17:27:07 +01:00 • committed by GitHub
parent 7c38649527
commit caf7a21c6f
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 6 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
tests/bench/accumulate_profile.py
View file

@ -4,10 +4,11 @@ import collections
import re
import sys
data = sys.stdin.read()
cats = collections.defaultdict(lambda: 0)
for m in re.findall("^(.+?) ([\d.]+)(m?)s$", data, re.MULTILINE):
cats[m[0].strip()] += float(m[1]) * (1e-3 if m[2] else 1)
for line in sys.stdin:
if m := re.match("(.+?) ([\d.]+)(m?)s", line):
cats[m[1].strip()] += float(m[2]) * (1e-3 if m[3] else 1)
sys.stderr.write(line)
for cat in sorted(cats.keys()):
cat2 = cat

4
tests/bench/speedcenter.exec.velcom.yaml
View file

@ -11,13 +11,13 @@
run_config:
<<: *time
cmd: |
bash -c 'set -eo pipefail; make LEAN_OPTS="-Dprofiler=true -Dprofiler.threshold=9999" -C ${BUILD:-../../build/release}/stage2 --output-sync --always-make -j$(nproc) make_stdlib 2>&1 > log | ./accumulate_profile.py'
bash -c 'set -eo pipefail; touch ../../src/Init/Prelude.lean; make LEAN_OPTS="-Dprofiler=true -Dprofiler.threshold=9999" -C ${BUILD:-../../build/release}/stage2 --output-sync -j$(nproc) make_stdlib 2>&1 | ./accumulate_profile.py'
max_runs: 2
parse_output: true
# initialize stage2 cmake + warmup
build_config:
cmd: |
bash -c 'make -C ${BUILD:-../../build/release} stage2 -j8'
bash -c 'make -C ${BUILD:-../../build/release} stage2 -j$(nproc)'
- attributes:
description: stdlib size
tags: [deterministic, fast]