Stream: Coq users

Topic: Profiling proof script

Laurent Théry (May 19 2021 at 12:55):

Hi,
Is there a tool that gives you the lines that are most time consuming when executing a proof script?
Thanks

Bas Spitters (May 19 2021 at 13:00):

I seem to recall it is in @Jason Gross coq-scripts, which also includes many other goodies:
https://github.com/JasonGross/coq-scripts/tree/master/timing

Laurent Théry (May 19 2021 at 13:26):

thanks. Could not manage to make it work but it seems to be file- based rather than line-based

Jason Gross (May 19 2021 at 14:05):

The tools have been merged upstream. If you have a makefile made by coq_makefile you can just pass TIMING=1 to make

Laurent Théry (May 19 2021 at 14:14):

great!!
Ps: I use sort -n -k 6 to get the most-time consuming lines is there sometthing more fancy?

Enrico Tassi (May 19 2021 at 14:21):

Beware that -n is not good enough

Enrico Tassi (May 19 2021 at 14:22):

Maybe -g is what you need

Jason Gross (May 19 2021 at 15:15):

If you want the most time-consuming difference in a single file, there's make print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing. I haven't written a tool to display the sorted version of the per-line timing info, but it wouldn't be that hard. Feel free to open an issue on the Coq bug tracker and assign me if you want a coq_makefile target for this or something similar.

Jason Gross (May 19 2021 at 15:20):

You might also be interested in Set Ltac Profiling and Show Ltac Profile or passing the -profile-ltac argument (I think) to coqc (or sticking it in COQEXTRAFLAGS for make)

Last updated: Apr 19 2024 at 08:01 UTC