Stream: Coq devs & plugin devs

Topic: Stack overflow in bench


view this post on Zulip 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

view this post on Zulip Gaƫtan Gilbert (Jun 09 2022 at 09:22):

it got so slow that there are too many nontrivial lines for List.map ?

view this post on Zulip Ali Caglayan (Jun 09 2022 at 11:00):

TIL that stdlib List.map is not tail recursive...

view this post on Zulip Ali Caglayan (Jun 09 2022 at 11:47):

fast_table
slow_table

view this post on Zulip Ali Caglayan (Jun 09 2022 at 11:47):

Timings table is 50mb as a text file so I can't post it here

view this post on Zulip Ali Caglayan (Jun 09 2022 at 11:50):

I've submitted a patch too https://github.com/coq/coq/pull/16162

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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. timings contains all the timings sorted.

It works like a charm, thanks!


Last updated: Feb 05 2023 at 21:03 UTC