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?
"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)
I think @Jim Fehrle meant "does not work" here.
@Jim Fehrle The Makefile in
test-suite is the one you should use in all cases, including when Coq was built with
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?
Yes, I mean "does not work" in one place (edited above).
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]
Are they run when doing cd test-suite; make?
/home/proj/coq$ make -f Makefile.dune world
dune build coq-core.install coq-stdlib.install coqide-server.install coqide.install
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
you still have _build_vo around? if yes delete it
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.
_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.
configure devel also mentions _build_vo, this is the main compat issue when trying to use Makefile.dune I think
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