I'm getting stack overflows from the renderer of bench results, here: https://gitlab.com/coq/coq/-/jobs/2562907286
it got so slow that there are too many nontrivial lines for List.map ?
TIL that stdlib List.map is not tail recursive...
Timings table is 50mb as a text file so I can't post it here
I've submitted a patch too https://github.com/coq/coq/pull/16162
Thanks Ali! Indeed they are degenerate traces but quite useful to investigate the slowdowns in my PR.
BTW, is there an easy way to locally find the hotspots in a given contrib given the bench artifacts?
@Matthieu Sozeau The "render_line_results.exe" script recurses down in the directory it was run. If go to html/contrib-of-interest
in the bench artifacts and then do dune exec --root=/your/coq -- dev/bench/render_line_results.exe
it will do it locally for that folder.
it will print the top 25 speed ups and slow downs by default in the terminal, and also produce the tables in files in the current directory. timings
contains all the timings sorted.
You can also tweak some numbers in render_line_results.ml to spit out 50 instead of 25 (just look for 25).
I also have a tweak where %diff tables are also produced, but I haven't merged that yet since I am still trying to teach coqbot about it
Ali Caglayan said:
it will print the top 25 speed ups and slow downs by default in the terminal, and also produce the tables in files in the current directory.
timings
contains all the timings sorted.
It works like a charm, thanks!
Last updated: Nov 29 2023 at 19:01 UTC