It seems QCDune command does not work with quickChick CLI tool

[anton-trunov]

For example (the stlc.v file below uses QCDune and QCOpen commands):

quickChick -color -top stlc
Testing base...
coqc stlc.v
QuickChecking prop_generator_makes_well_typed_terms
cp -r extr /var/folders/qy/cwhzbpsj75g81gtv3hjzn4mw0000gn/T/QuickChick/193524
awk: can't open file dune
 source line number 1
File "./stlc.v", line 237, characters 0-49:
Error:
/var/folders/qy/cwhzbpsj75g81gtv3hjzn4mw0000gn/T/QuickChick/193524/_build/default/QuickChick8e0e92.exe: Exited with status 127

/bin/sh: /var/folders/qy/cwhzbpsj75g81gtv3hjzn4mw0000gn/T/QuickChick/193524/_build/default/QuickChick8e0e92.exe: No such file or directory

[Lysxia]

The QCtool CLI utility follows quite a different codepath from the plugin. Sadly this means recent features like dune support (which get added into the plugin first) might need some more work for QCtool to catch up.

Would you mind letting me have a look at your use case? That would help me figure out what the tool needs to do here.

[anton-trunov]

Thanks for looking into this issue!

So, we have a codebase that uses QuickChick to test the implementation of Scilla. We describe a simplified version of Scilla's syntax, write generators, shrinkers, properties, etc. in Coq and write some wrapper OCaml code to translate the simplified syntax to native Scilla syntax. QuickChick then assembles everything into one working system (it relies on the fact that the OCaml side will be accessible from Coq via extraction of axioms). Initially, I thought Dune would build the project, but that didn't work and @lemonidas added some helper vernacular which greatly helped to get the project get off the ground.

Having some principled solution where Dune can work with QuickChick code just like with any extracted Coq code would help with this, I think. For example, I wouldn't mind putting properties into several .v files and adding more executable targets to dune files, so I could run a subset of properties via Dune: dune run prop1 (or something like this). What do you think?

[Lysxia]

Yeah, what you describe sounds like a good solution! If I understand correctly, the existing vernaculars should be enough (at least for common use cases), and this is more about documenting how one might set up QC tests with dune. This doesn't need the CLI tool, which I think is rather aimed towards mutation testing.

[anton-trunov]

this is more about documenting how one might set up QC tests with dune

This would be really really helpful!

This doesn't need the CLI tool, which I think is rather aimed towards mutation testing.

Mutation testing might come in handy at a later stage of our project, I'd like that to also cooperate with Dune if it's doable.