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=before to get
.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-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: Oct 16 2021 at 02:03 UTC