Matthieu Sozeau (Mar 31 2021 at 16:29): Matthieu Sozeau (Mar 31 2021 at 16:29):I think there was support to get per-line time diffs to study performance issues, where/how do I find it?
Matthieu Sozeau (Mar 31 2021 at 16:29):I'd like to investigate the slowdowns in this PR: https://github.com/coq/coq/pull/13969
Jason Gross (Apr 01 2021 at 12:18):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: Jun 09 2023 at 08:01 UTC