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: Jun 04 2023 at 23:30 UTC