Stream: Dune devs & users

Topic: Cram test support for Coq

view this post on Zulip Rodolphe Lepigre (Jul 27 2022 at 07:28):

We (@Paolo Giarrusso and I) have been recently thinking about using dune cram tests for Coq, in a setting where we have a Coq theory and would like to run tests against it. The kind of workflow I hoped would work fails (see, so I'm wondering if people here have any thoughts on that.

I know @Ali Caglayan (if I'm not mistaken) used some hacks to support similar things, but explicitly calling coqc. Here I'm hoping to just be able to use dune to build the tests, which seems to work at least for OCaml. This would be robust to theories being moved around, because we would not need to give paths explicitly.

Last updated: Jan 30 2023 at 18:04 UTC