Is there a tool that gives you the lines that are most time consuming when executing a proof script?
I seem to recall it is in @Jason Gross coq-scripts, which also includes many other goodies:
thanks. Could not manage to make it work but it seems to be file- based rather than line-based
The tools have been merged upstream. If you have a makefile made by coq_makefile you can just pass TIMING=1 to make
Ps: I use
sort -n -k 6 to get the most-time consuming lines is there sometthing more fancy?
Beware that -n is not good enough
Maybe -g is what you need
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.
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: Jan 31 2023 at 13:02 UTC