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...)
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
it should probably be distributed as a git submodule instead of something to copy-paste, but I don't remember complaints about it.
@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...
That's also something I wonder about. Libraries I've touched (including QuickChick) basically have a separate
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.
@Arthur Azevedo de Amorim
there might be more but let me find a link
@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
and that was basically a copy of the original files (under BSD license)
@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)
Fancy! I haven't done that no.
Have you tried setting up tests in a dune project yet?
Not yet. Does the
teststanza work for Coq?
It doesn’t. But I would like to make it work, or make an analogous stanza for coq.
Last updated: Dec 05 2023 at 12:01 UTC