make ci-coqprime on a completely different opam switch, but findlib seems to find coq in another switch. What can I do about this?
findlib: [WARNING] Package coq-core has multiple definitions in /home/ali/coq/_build/install/default/lib/coq-core/META, /mnt/sdd1/.opam/coq.dev/lib/coq-core/META
Judging from just that message, that only shows one active switch (
coq.dev), and a META file from the project you’re building (
if you’re right, maybe
eval $(opam env) is needed to fix your environment. Otherwise, the workaround might be to not install Coq in the switch you use to develop Coq (robust but annoying), or extend tooling to shadow the installed Coq properly (useful but possibly nontrivial)
coq.dev is not the active switch nor is it in the env.
and there’s no
./_opam making it active in the current folder?
I've deleted _build_ci and started again seems to be working
I guess maybe something switched during setup of _build_ci
Ali Caglayan has marked this topic as resolved.
@Ali Caglayan I also found a few problem with the CI run due to stale deps, hopefully we can improve that by dunerizing a bit more
According to my tests, even you see the warning things works fine since findlib prefers the first one, which is the one in the sources/build tree of coq
I do regularly develop (master) in a switch with stable coq (8.15) installed, and it works
Last updated: Jun 04 2023 at 19:30 UTC