lean4-htt/tests/bench/accumulate_profile.py
Sebastian Ullrich f0347ee719
chore: lean --stats gives number of imported bytes (#8725)
Thanks to `mmap`, startup time is not necessarily related to this
figure, but it can be used as a rough measure for that and how much data
the module depends on, i.e. the rebuild chance.

Also adds new cumulative benchmarks for this metric as well as the
number of imported constants and env ext entries.
2025-06-12 08:29:42 +00:00

18 lines
555 B
Python
Executable file

#!/usr/bin/env python3
import collections
import re
import sys
cats = collections.defaultdict(lambda: 0)
for line in sys.stdin:
if m := re.match(r"(.+?) ([\d.]+)(m?)s", line) or \
re.match(r"\s*(number of imported bytes|number of imported consts|number of imported entries):\s+(\d+)()", 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
if len(sys.argv) > 1:
cat2 = f"{sys.argv[1]} {cat}"
print(f"{cat2!r}: {cats[cat]:f}")