@Jason Gross it seems that the coq-rewriter-perf-SuperFast opam package does not honour the TIMING flag to give detailed info for the bench, is it expected?
@Pierre-Marie Pédrot The
TIMING flag gives per-line timing, and this is not very useful for the targets in
coq-rewriter-perf-SuperFast which are not already in
coq-rewriter, because each file contains only one line which runs a tactic which does the tests. The reason you don't get the timing information is because these files are already set up to redirect their output to
src/Rewriter/Rewriter/Examples/PerfTesting/*/*.log. You can find the timing information you want there. Also, once https://github.com/coq/opam-coq-archive/pull/1391 is merged, you can get the more fine-grained timing information more conveniently in the
perf.csv file that will be generated at top-level.
This needs to be made in a way that is compatible with the coq bench though.
If there is little difference between coq-rewriter and its SuperFast version, how come https://github.com/coq/coq/pull/12565 shows an observable slowdown in the latter?
@Pierre-Marie Pédrot Sorry for the delay in response. What do you mean by "in a way compatible with the coq bench"? If https://github.com/coq/coq/pull/12900 gets merged, the raw files should be available. If you want me to just rename the files from
.timing, I can also do that, and then they'll get picked up sort-of-by-accident. Should I do that?
And regarding the difference: My claim is not that there is no difference. It's just that you won't see any difference on the line-by-line granularity, only on the per-file granularity, as all of the files that differ between them are essentially one-line files.
I just wanted to say that these files need to have a specific extension so that they are recognized as bench logs.
For now we fetch *.html and files in _bench/log, so maybe the yaml script needs to be tweaked accordingly
The PR will make the yaml script pick up the relevant logs. If you want them to be turned into html files by the bench script, feel free to open an issue on the relevant repos and I'll try to get around to it in the near future.
(I'm currently a bit short on both time and mental-space-for-tracking things, which is why I want to offload the tracking of this to the GH issue tracker)
Last updated: Feb 05 2023 at 21:03 UTC