Stream: Dune devs & users

Topic: ✔ Confused with cram tests using Coq in the dune repo

Rodolphe Lepigre (Mar 16 2023 at 08:22):

I want to work on fixing a dune bug, and for some reason I don't seem to be able to run cram tests (form the dune repo). They are simply not run when I call ./dune.exe build @test-alias(the command does not fail), even if I add an $ exit 1 line in the test. Do I need to do anything special for these tests to be enabled? I recall making and running tests like those a few months ago, and never had that problem.

Emilio Jesús Gallego Arias (Mar 16 2023 at 14:38):

I guess a few things to look @Rodolphe Lepigre is:

Emilio Jesús Gallego Arias (Mar 16 2023 at 14:38):

• your opam switch is up to date (see the make target in dune's makefile), if a dep is missing the tests won't be run
• the tests you want to run are not guarded with some flag (recently devs have done that to increase granularity, for example for Coq tests)

Rodolphe Lepigre (Mar 16 2023 at 14:50):

Indeed, a flag was introduced. I need to do DUNE_COQ_TEST=enable ./dune.exe build @test-alias. Thanks!

Notification Bot (Mar 16 2023 at 14:53):

Rodolphe Lepigre has marked this topic as resolved.

Ali Caglayan (Mar 16 2023 at 16:48):

Sorry about that, I should add a warning if a user tries to run a test but the flag is not set.

Last updated: Jun 04 2023 at 23:30 UTC