Pierre-Marie Pédrot (Aug 20 2020 at 13:27): Pierre-Marie Pédrot (Aug 20 2020 at 13:27):@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?
Jason Gross (Aug 20 2020 at 17:38):@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.
Pierre-Marie Pédrot (Aug 20 2020 at 19:50):This needs to be made in a way that is compatible with the coq bench though.
Pierre-Marie Pédrot (Aug 20 2020 at 19:50):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?
Jason Gross (Aug 25 2020 at 18:07):@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 .log to .timing, I can also do that, and then they'll get picked up sort-of-by-accident. Should I do that?
Jason Gross (Aug 25 2020 at 18:08):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.
Pierre-Marie Pédrot (Aug 25 2020 at 18:31):I just wanted to say that these files need to have a specific extension so that they are recognized as bench logs.
Pierre-Marie Pédrot (Aug 25 2020 at 18:32):For now we fetch *.html and files in _bench/log, so maybe the yaml script needs to be tweaked accordingly
Jason Gross (Aug 26 2020 at 03:18):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.
Jason Gross (Aug 26 2020 at 03:18):(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: Dec 01 2023 at 06:01 UTC