Matthieu Sozeau (Jun 09 2022 at 09:17): Matthieu Sozeau (Jun 09 2022 at 09:17):I'm getting stack overflows from the renderer of bench results, here: https://gitlab.com/coq/coq/-/jobs/2562907286
Gaëtan Gilbert (Jun 09 2022 at 09:22):it got so slow that there are too many nontrivial lines for List.map ?
Ali Caglayan (Jun 09 2022 at 11:00):TIL that stdlib List.map is not tail recursive...
Ali Caglayan (Jun 09 2022 at 11:47): Ali Caglayan (Jun 09 2022 at 11:47):Timings table is 50mb as a text file so I can't post it here
Ali Caglayan (Jun 09 2022 at 11:50):I've submitted a patch too https://github.com/coq/coq/pull/16162
Matthieu Sozeau (Jun 09 2022 at 12:14):Thanks Ali! Indeed they are degenerate traces but quite useful to investigate the slowdowns in my PR.
Matthieu Sozeau (Jun 09 2022 at 12:19):BTW, is there an easy way to locally find the hotspots in a given contrib given the bench artifacts?
Ali Caglayan (Jun 09 2022 at 12:39):@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.
Ali Caglayan (Jun 09 2022 at 12:41):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.
Ali Caglayan (Jun 09 2022 at 12:41):You can also tweak some numbers in render_line_results.ml to spit out 50 instead of 25 (just look for 25).
Ali Caglayan (Jun 09 2022 at 12:43):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
Matthieu Sozeau (Jun 09 2022 at 18:38):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.
timingscontains all the timings sorted.
It works like a charm, thanks!
Last updated: Apr 20 2024 at 12:02 UTC