Stream: Coq devs & plugin devs

Topic: `make unit-tests` not working

view this post on Zulip Ali Caglayan (Jul 09 2021 at 10:37):

When I do make unit-tests in test-suite I get to here:

TEST      unit-tests/clib/inteq.ml
ocamlfind: Package `coq-core.toplevel' not found
Makefile:325: recipe for target 'unit-tests/clib/inteq.ml.log' failed
make: *** [unit-tests/clib/inteq.ml.log] Error 2

Did I miss something?

view this post on Zulip Ali Caglayan (Jul 09 2021 at 10:38):

Originally happened within dune

view this post on Zulip Ali Caglayan (Jul 09 2021 at 10:39):

I'm not sure how to make things know about coq-core.toplevel

view this post on Zulip Gaëtan Gilbert (Jul 09 2021 at 10:53):

It's a bug, please open an issue

view this post on Zulip Ali Caglayan (Jul 09 2021 at 10:59):

OK submitted as https://github.com/coq/coq/issues/14624

view this post on Zulip Emilio Jesús Gallego Arias (Jul 09 2021 at 12:31):

For some reason OCAMLPATH is not properly set, or maybe coq was not built?

view this post on Zulip Gaëtan Gilbert (Jul 09 2021 at 12:32):

I made a PR, look at it

Last updated: Oct 13 2024 at 01:02 UTC