Daniel Hilst Selli (Jan 31 2022 at 22:21): Daniel Hilst Selli (Jan 31 2022 at 22:21):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.
Karl Palmskog (Jan 31 2022 at 23:59):See the Time command for benchmarking. The closest to JUnit is QuickChick.
Paolo Giarrusso (Feb 01 2022 at 00:04):There are also options for outputting per-line timing...
Paolo Giarrusso (Feb 01 2022 at 00:06):... 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.
Paolo Giarrusso (Feb 01 2022 at 00:06):(no need for a coq plugin tho I think)
Daniel Hilst Selli (Feb 01 2022 at 00:23):Thanks Paolo make TIMED=1 pretty-timed is already something :)
Paolo Giarrusso (Feb 01 2022 at 00:46):If you want more, the coq manual shows lots of options.
Paolo Giarrusso (Feb 01 2022 at 00:47):Then I've seen scripts where timing diffs are overlaid on the source and code that got slower becomes red.
Paolo Giarrusso (Feb 01 2022 at 00:47):Sadly, those timings aren't integrated with perf.
Last updated: Apr 16 2024 at 21:01 UTC