feat: separate benchmark for profiling the stdlib per-file
This commit is contained in:
parent
acc1752874
commit
72fc3f6679
2 changed files with 21 additions and 1 deletions
|
|
@ -10,4 +10,7 @@ for m in re.findall("^([^\n\d]+)([\d.]+)(m?)s$", data, re.MULTILINE):
|
|||
cats[m[0].strip()] += float(m[1]) * (1e-3 if m[2] else 1)
|
||||
|
||||
for cat in sorted(cats.keys()):
|
||||
print(f"{cat!r}: {cats[cat]}")
|
||||
cat2 = cat
|
||||
if len(sys.argv) > 1:
|
||||
cat2 = f"{sys.argv[1]} {cat}"
|
||||
print(f"{cat2!r}: {cats[cat]:f}")
|
||||
|
|
|
|||
17
tests/bench/full-stdlib.exec.yaml
Normal file
17
tests/bench/full-stdlib.exec.yaml
Normal file
|
|
@ -0,0 +1,17 @@
|
|||
- attributes:
|
||||
description: stdlib
|
||||
tags: [slow]
|
||||
time: &time
|
||||
#runner: time
|
||||
# alternative config: use `perf stat` for extended properties
|
||||
runner: perf_stat
|
||||
perf_stat:
|
||||
properties: ['wall-clock', 'task-clock', 'instructions']
|
||||
rusage_properties: ['maxrss']
|
||||
run_config:
|
||||
<<: *time
|
||||
cwd: ../../src/
|
||||
cmd: |
|
||||
find . -name '*.lean' -exec bash -c 'lean --stats -Dprofiler=true -Dprofiler.threshold=9999 {} 2>&1 | ../tests/bench/accumulate_profile.py {}' \;
|
||||
max_runs: 2
|
||||
parse_output: true
|
||||
Loading…
Add table
Reference in a new issue