[red-knot] Add metrics collection #16005
dcreager
wants to merge
18 commits into
main
from
dcreager/metrics
Start recording some metrics
1c71f9b8
Initial JSON metrics exporter
25a84c7b
Include timestamp in JSON metrics
c8b2cc4e
Hide the thread-local buffer better
80efb01e
Better documentation
382349f8
Include executable name in metrics
e73374c1
Include time since start of process
5ec0cb32
Add --metrics flag
ca237345
Clippy
1e147007
Add initial plot script
88ef4567
Add histogram subcommand
ff5e65f6
Add README
5a7650d5
Optionally save output to file
f587a89a
Describe before/after comparisons
391917bc
pre-commit
b0beb935
Use default_missing_value instead of double-Option
5e34d79c
List comprehension
8e880c8f
Include scope kind in `scope_count` metric, add bar graph
70a53737
Reviewers
No reviews
Assignees
No one assigned
Labels
ty
Milestone
No milestone
Login to write a write a comment.
Login via GitHub