Stream: Dune devs & users

Topic: Running the test suite


view this post on Zulip Jim Fehrle (Nov 07 2021 at 00:23):

When I run "make -f Makefile.dune test-suite" on master, I get hundreds of tests with the message "Cannot find plugins directory".
Also it appears that unit test were not run, while "cd test-suite; make unit-tests" does run them. "cd test-suite; make -f Makefile.dune unit-tests" does not work. Are there workarounds/fixes for this?

view this post on Zulip Gaëtan Gilbert (Nov 07 2021 at 08:59):

"cd test-suite; make -f Makefile.dune unit-tests" does work

wtf that shouldn't be possible (there's no Makefile.dune in test-suite)

view this post on Zulip Théo Zimmermann (Nov 08 2021 at 10:21):

I think @Jim Fehrle meant "does not work" here.

view this post on Zulip Théo Zimmermann (Nov 08 2021 at 10:22):

@Jim Fehrle The Makefile in test-suite is the one you should use in all cases, including when Coq was built with Makefile.dune.

view this post on Zulip Théo Zimmermann (Nov 08 2021 at 10:23):

The fact that unit tests are not run when doing make -f Makefile.dune test-suite is surprising. Are they run when doing cd test-suite; make?

view this post on Zulip Jim Fehrle (Nov 08 2021 at 19:55):

Yes, I mean "does not work" in one place (edited above).

view this post on Zulip Jim Fehrle (Nov 08 2021 at 19:59):

Then the last line in this info from the makefile is incorrect:

$ make -f Makefile.dune

Welcome to Coq's Dune-based build system. Common developer targets are:

view this post on Zulip Jim Fehrle (Nov 08 2021 at 20:00):

Are they run when doing cd test-suite; make?

Nope.

/home/proj/coq$ make -f Makefile.dune world
dune build coq-core.install coq-stdlib.install coqide-server.install coqide.install
/home/proj/coq$ pushd
/home/proj/coq/test-suite /home/proj/coq
/home/proj/coq/test-suite$ make

Coq's standard library has not been built; please run any of:

- make -j NJOBS world if you used -profile devel in configure
- make -f Makefile.dune world if you want to use dune autogenerated configure setup

Makefile:171: recipe for target 'all' failed
make: *** [all] Error 1

view this post on Zulip Gaëtan Gilbert (Nov 08 2021 at 20:17):

you still have _build_vo around? if yes delete it

view this post on Zulip Jim Fehrle (Nov 15 2021 at 02:49):

What creates _build_vo? If it's a problem, why doesn't make -f Makefile.dune clean remove it? Dune's details are completely opaque. Or alternatively, have dune generate an error message if it's present when it shouldn't be.

view this post on Zulip Théo Zimmermann (Nov 15 2021 at 11:25):

_build_vo is what is created by Makefile.make. It's not a problem to build Coq itself. It's only a problem to run the test suite because the test suite Makefile will decide how Coq was built depending on whether _build_vo exists or not.

view this post on Zulip Gaëtan Gilbert (Nov 15 2021 at 11:32):

configure devel also mentions _build_vo, this is the main compat issue when trying to use Makefile.dune I think

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 11:43):

I tried to add a check to makefile.dune that will complain if _build_vo does exists, but it defies my make knowlegde


Last updated: Feb 04 2023 at 02:03 UTC