Rodolphe Lepigre (Jul 27 2022 at 07:28): 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 https://github.com/ocaml/dune/pull/6014), 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: Apr 20 2024 at 03:40 UTC