chore(tests/bench/speedcenter.exec.yaml): stdlib: time imports

This commit is contained in:
Sebastian Ullrich 2019-07-05 15:54:35 +02:00
parent ca464d2517
commit a87591af40
2 changed files with 2 additions and 2 deletions

View file

@ -6,7 +6,7 @@ import sys
data = sys.stdin.read()
cats = collections.defaultdict(lambda: 0)
for m in re.findall("^([^\n\d]+)([\d.]+)(m?)s", data, re.MULTILINE):
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()):

View file

@ -11,7 +11,7 @@
<<: *time
cwd: ../../library
cmd: |
bash -c "find . -name '*.lean' -exec ../bin/lean -Dprofiler=true -Dprofiler.threshold=9999 {} \; 2>&1 | ../tests/bench/accumulate_profile.py"
bash -c "find . -name '*.lean' -exec ../bin/lean --stats -Dprofiler=true -Dprofiler.threshold=9999 {} \; 2>&1 | ../tests/bench/accumulate_profile.py"
max_runs: 3
parse_output: true
- attributes: