Stream: Coq devs & plugin devs

Topic: Struggling with `make test-suite`


view this post on Zulip Gregory Malecha (Sep 30 2022 at 03:08):

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

view this post on Zulip Gregory Malecha (Sep 30 2022 at 13:25):

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)

view this post on Zulip Gregory Malecha (Sep 30 2022 at 13:25):

however, even after a git clean -x and such, i've been unable to find where the old path is coming from

view this post on Zulip Gaëtan Gilbert (Sep 30 2022 at 13:30):

don't use make test-suite, use make -C test-suite instead

view this post on Zulip Emilio Jesús Gallego Arias (Oct 01 2022 at 08:11):

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.

view this post on Zulip Gregory Malecha (Oct 01 2022 at 11:22):

Should we update the documentation from the Makefile to suggest people not use make test-suite until these fixes land?


Last updated: Feb 01 2023 at 14:03 UTC