Stream: Coq devs & plugin devs

Topic: Building test-suite with dune


view this post on Zulip Ali Caglayan (Jul 15 2021 at 19:20):

How can I stop dune from rebuilding the test-suite every time? I had to switch back to the legacy system because I couldn't get incremental builds

view this post on Zulip Gaëtan Gilbert (Jul 15 2021 at 19:23):

don't use dune runtest, instead cd test-suite; make
ignore unit test failures until https://github.com/coq/coq/pull/14625 merged (unit tests don't test anything interesting anyway)

view this post on Zulip Stéphane Desarzens (Jul 15 2021 at 19:38):

To only run part of the test-suite, when using dune, I modify last line the test-suite/dune file and add the name of the make-target before the closing double-quotes.


Last updated: Feb 01 2023 at 15:04 UTC