Testing best practices · Coq users

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...)

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

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.

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...

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.

Paolo Giarrusso (Nov 30 2020 at 20:07):

@Arthur Azevedo de Amorim Makefile.coq.local

Paolo Giarrusso (Nov 30 2020 at 20:07):

there might be more but let me find a link

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

Paolo Giarrusso (Nov 30 2020 at 20:09):

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

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)