Jim Fehrle (Nov 07 2021 at 00:23): 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?
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)
Théo Zimmermann (Nov 08 2021 at 10:21):I think @Jim Fehrle meant "does not work" here.
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.
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?
Jim Fehrle (Nov 08 2021 at 19:55):Yes, I mean "does not work" in one place (edited above).
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:
- states: build a minimal functional coqtop
- world: build all public binaries and libraries
- watch: build all public binaries and libraries [continuous build]
- check: build all ML files as fast as possible
- test-suite: run Coq's test suite [env NJOBS=N to set job parallelism]
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
Gaëtan Gilbert (Nov 08 2021 at 20:17):you still have _build_vo around? if yes delete it
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.
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.
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
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: Jun 04 2023 at 23:30 UTC