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:
Doesn't exist. So is there anything special I need to do due to the coq-core split?
(I built Coq using dune obviously)
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.
Sorry for that
this transitions is so messy, would have been so much faster to do it long time ago
It's ok, it has to be messy at first :)
Last updated: Feb 06 2023 at 18:03 UTC