diff --git a/tests/bench/accumulate_profile.py b/tests/bench/accumulate_profile.py index 673da061c5..2eb4779ed1 100755 --- a/tests/bench/accumulate_profile.py +++ b/tests/bench/accumulate_profile.py @@ -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()): diff --git a/tests/bench/speedcenter.exec.yaml b/tests/bench/speedcenter.exec.yaml index a4372e5e08..86a7ecb7d1 100644 --- a/tests/bench/speedcenter.exec.yaml +++ b/tests/bench/speedcenter.exec.yaml @@ -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: