Stream: Coq devs & plugin devs

Topic: Failing to build ci-mtac2 with Dune

Matthieu Sozeau (Mar 23 2021 at 18:27):

Dear devs, I can't seem to be able to run make ci-mtac2 successfully on a branch on master, the compilation fails with

CAMLOPT -c -for-pack MetaCoqPlugin src/run.ml
File "src/run.ml", line 468, characters 13-42:
Error: Unbound module Unicoq

And that's because the paths are wrong:

-I "/Volumes/Dev/coq/coq/_build/install/default/lib/coq/../coq-core///user-contrib/Unicoq"

Doesn't exist. So is there anything special I need to do due to the coq-core split?

Matthieu Sozeau (Mar 23 2021 at 18:28):

(I built Coq using dune obviously)

Emilio Jesús Gallego Arias (Mar 23 2021 at 21:53):

Ups, that's a bug in the current setup, is fixed by https://github.com/coq/coq/pull/13617 which removes all these hacks, let me see if I can find a workaround, for now the solution is to use make or just do a symlink.

Emilio Jesús Gallego Arias (Mar 23 2021 at 21:53):

Sorry for that

Emilio Jesús Gallego Arias (Mar 23 2021 at 21:53):

this transitions is so messy, would have been so much faster to do it long time ago

Matthieu Sozeau (Mar 23 2021 at 22:50):

It's ok, it has to be messy at first :)

Last updated: Jun 08 2023 at 04:01 UTC