Stream: Coq users

Topic: Testing best practices


view this post on Zulip Arthur Azevedo de Amorim (Nov 30 2020 at 18:56):

Is there a set of best practices for testing Coq libraries? I noticed that Iris and MathComp set up their own testing infrastructure in an ad hoc way, but it would be nice if there were a more streamlined option. (Right now I am just including the test file with the rest of the library, which is far from ideal...)

view this post on Zulip Paolo Giarrusso (Nov 30 2020 at 18:59):

I wonder if quickchick has useful infrastructure here; I haven't worked with math-comp, but Iris's infrastructure is the best I've seen and is pretty reusable

view this post on Zulip Paolo Giarrusso (Nov 30 2020 at 19:00):

it should probably be distributed as a git submodule instead of something to copy-paste, but I don't remember complaints about it.

view this post on Zulip Arthur Azevedo de Amorim (Nov 30 2020 at 19:04):

@Paolo Giarrusso Do you mean the .v files that live under tests? I've been browsing around, but couldn't find exactly what compiles these files...

view this post on Zulip Li-yao (Nov 30 2020 at 19:10):

That's also something I wonder about. Libraries I've touched (including QuickChick) basically have a separate _CoqProject+Makefile setup for tests. But it's pretty inconsistent regarding how the tests depend on the library, ie. whether they depend on the library via opam, or by local inclusion (adding an explicit -Q to the test _CoqProject). With such a simplistic setup it's one or the other, and I never remember whether one of them works better with opam.

view this post on Zulip Paolo Giarrusso (Nov 30 2020 at 20:07):

@Arthur Azevedo de Amorim Makefile.coq.local

view this post on Zulip Paolo Giarrusso (Nov 30 2020 at 20:07):

there might be more but let me find a link

view this post on Zulip Paolo Giarrusso (Nov 30 2020 at 20:08):

@Arthur Azevedo de Amorim ah, also test-normalized.sed — here's how I added this to my project: https://github.com/Blaisorblade/dot-iris/commit/6ae29dbe869d04495ed430817052baa149ba4b9a#diff-6f708165431fa3d2ed655f153efa5c258f45ba47921d696bce59170ebe0094b5

view this post on Zulip Paolo Giarrusso (Nov 30 2020 at 20:09):

and that was basically a copy of the original files (under BSD license)

view this post on Zulip Paolo Giarrusso (Nov 30 2020 at 20:12):

@Li-yao do those tests have a recorded output to compare against? Both iris and coq do that (I don't think coq's setup is as easy to extract—never looked at it)

view this post on Zulip Li-yao (Nov 30 2020 at 20:20):

Fancy! I haven't done that no.

view this post on Zulip Rudi Grinberg (Dec 03 2020 at 16:03):

Li-yao
Have you tried setting up tests in a dune project yet?

view this post on Zulip Li-yao (Dec 03 2020 at 17:45):

Not yet. Does the teststanza work for Coq?

view this post on Zulip Rudi Grinberg (Dec 07 2020 at 04:05):

It doesn’t. But I would like to make it work, or make an analogous stanza for coq.


Last updated: Jan 29 2023 at 06:02 UTC