I think there was support to get per-line time diffs to study performance issues, where/how do I find it?
I'd like to investigate the slowdowns in this PR: https://github.com/coq/coq/pull/13969
If you're doing it yourself locally, pass TIMING=after
and TIMING=before
to get .after-timing
and .before-timing
for every file (if you pass anything else, the extension is just .timing
). You can then use the target all.timing.diff
to build .timing.diff
files for each file.
If you're looking for per-line timing on the bench on that PR, I think you're out of luck, as it seems that artifacts are not uploaded if the bench script times out. (Perhaps this should be fixed in the bench script?) If you re-run the bench in a way that gets it to upload the artifacts (perhaps just redo the bench with coq-fiat-parsers
, coq-math-classes
, and coq-bedrock2
?), you should see .timing
files for every compiled file. These can be made into a table with Python scripts shipped with Coq, which can be invoked via, e.g., make print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing
(see https://github.com/coq/coq/blob/1a64b1560ce88855a76e2faa14cec2864de2f37c/tools/CoqMakefile.in#L389-L402). I think the html versions of the diffs might also be automatically generated and show up in some nearly-top-level html
folder in the artifact? And I think @Pierre-Marie Pédrot also has his own scripts for exploring the timing info.
Last updated: Dec 06 2023 at 14:01 UTC