Stream: Coq users

Topic: Is there any JUnit plugin for Coq?


view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Jan 31 2022 at 23:59):

See the Time command for benchmarking. The closest to JUnit is QuickChick.

view this post on Zulip Paolo Giarrusso (Feb 01 2022 at 00:04):

There are also options for outputting per-line timing...

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Feb 01 2022 at 00:06):

(no need for a coq plugin tho I think)

view this post on Zulip Daniel Hilst Selli (Feb 01 2022 at 00:23):

Thanks Paolo make TIMED=1 pretty-timed is already something :)

view this post on Zulip Paolo Giarrusso (Feb 01 2022 at 00:46):

If you want more, the coq manual shows lots of options.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Feb 01 2022 at 00:47):

Sadly, those timings aren't integrated with perf.


Last updated: Feb 06 2023 at 13:03 UTC