I'm struggling with a fresh checkout of coq. I run make world
which completes without errors, then I run make test-suite
and it says:
$ make world
dune build --root . theories_dune ltac2_dune
gen_rules ltac2_dune
gen_rules theories_dune
touch .dune-stamp
cp -a _build/default/theories_dune theories/dune && chmod +w theories/dune
cp -a _build/default/ltac2_dune user-contrib/Ltac2/dune && chmod +w user-contrib/Ltac2/dune
dune build coq-core.install coq-stdlib.install coqide-server.install coqide.install coq.install
$ make test-suite
dune build --root . theories_dune ltac2_dune
touch .dune-stamp
cp -a _build/default/theories_dune theories/dune && chmod +w theories/dune
cp -a _build/default/ltac2_dune user-contrib/Ltac2/dune && chmod +w user-contrib/Ltac2/dune
dune runtest --no-buffer
Done: 99% (14518/14519, 1 left) (jobs: 1)make[1]: Entering directory '/home/gmalecha/code/coq/clean/_build/default/test-suite'
Coq's standard library has not been built; please run:
- make world
make[1]: *** [Makefile:176: all] Error 1
make[1]: Leaving directory '/home/gmalecha/code/coq/clean/_build/default/test-suite'
File "test-suite/dune", line 15, characters 0-1112:
15 | (rule
16 | (targets summary.log)
17 | (deps
....49 | (action
50 | (progn
51 | (bash "make -j %{env:NJOBS=2} BIN=%{read:bin.inc} COQLIB=%{read:libpath.inc} PRINT_LOGS=1 UNIT_TESTS=%{env:COQ_UNIT_TEST=unit-tests}"))))
bash test-suite/summary.log (exit 2)
make: *** [Makefile.dune:148: test-suite] Error 1
It seems the issue that i have is that I moved my coq checkout and did not re-run configure
(since make
says that you should not run configure
)
however, even after a git clean -x
and such, i've been unable to find where the old path is coming from
don't use make test-suite
, use make -C test-suite
instead
Yup @Gregory Malecha , the setup is brittle as of today, but are working on porting the test-suite to dune too which should solve the issue.
Should we update the documentation from the Makefile
to suggest people not use make test-suite
until these fixes land?
Gregory Malecha has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC