Stream: Dune devs & users

Topic: ✔ Dune, Coq and @runtests

Jerome Hugues (Sep 08 2021 at 01:25):

21:24

Hi,

I post here a question I asked initially in Coq Users:

I converted a project to Dune with much success. I would like to try the equivalent of @runtests for Coq. That is:

I have a couple of .v files that are basically tests, i.e. a collection of lemma foo x = bar that checks that foo x returns the right value. Those are usually proved through a mere trivial. I would like to instruct dune to consider those files only when I run tests (i.e. dune build @install @runtest). I could imagine grouping those .v files in a dedicated tests directory. But I miss the next step for dune to consider those only when I run a dune build. Do I need to write a dedicated backend? Did someone already try this?

Thanks,

Lasse Blaauwbroek (Sep 08 2021 at 01:33):

I had the same problem, see here for the discussion: https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs.20.26.20users/topic/Composable.20builds.20coqdep/near/220338092

Jerome Hugues (Sep 08 2021 at 01:43):

Lasse said:

I had the same problem, see here for the discussion: https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs.20.26.20users/topic/Composable.20builds.20coqdep/near/220338092

Thanks, this is exactly what I needed to find.

Notification Bot (Sep 08 2021 at 01:44):

Jerome Hugues has marked this topic as resolved.

Last updated: Jun 04 2023 at 23:30 UTC