I'm wondering if there is JUnit plugin for Coq to output junit.xml so that is possible to configure the CI to show what are and how much time each proof take.
If there is no such tool, it would be possible to do it as a plugin? Basically we need to take the name of each lemma/theorem, the time that it took to run and at the end output an .xml file.
Time command for benchmarking. The closest to JUnit is QuickChick.
There are also options for outputting per-line timing...
... and converting that output into junit might not be the ideal way to process timing information, tho I won't be shocked if it's the best tool for you.
(no need for a coq plugin tho I think)
make TIMED=1 pretty-timed is already something :)
If you want more, the coq manual shows lots of options.
Then I've seen scripts where timing diffs are overlaid on the source and code that got slower becomes red.
Sadly, those timings aren't integrated with perf.
Last updated: Oct 03 2023 at 21:01 UTC