Ali Caglayan (May 09 2022 at 17:26): Ali Caglayan (May 09 2022 at 17:26):Running 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 (/home/ali/coq)
Paolo Giarrusso (May 09 2022 at 18:42):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)
Ali Caglayan (May 09 2022 at 18:44):So coq.dev is not the active switch nor is it in the env.
Paolo Giarrusso (May 09 2022 at 18:45):and there’s no ./_opam making it active in the current folder?
Ali Caglayan (May 09 2022 at 18:45):Nope
Ali Caglayan (May 09 2022 at 18:45):I've deleted _build_ci and started again seems to be working
Ali Caglayan (May 09 2022 at 18:46):I guess maybe something switched during setup of _build_ci
Notification Bot (May 09 2022 at 18:46):Ali Caglayan has marked this topic as resolved.
Emilio Jesús Gallego Arias (May 09 2022 at 20:38):@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
Enrico Tassi (May 10 2022 at 06:55):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
Enrico Tassi (May 10 2022 at 06:56):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