Stream: Coq devs & plugin devs

Topic: ✔ findlib finding coq-core/META from another opam switch


view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (May 09 2022 at 18:40):

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)

view this post on Zulip 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)

view this post on Zulip Ali Caglayan (May 09 2022 at 18:44):

So coq.dev is not the active switch nor is it in the env.

view this post on Zulip Paolo Giarrusso (May 09 2022 at 18:45):

and there’s no ./_opam making it active in the current folder?

view this post on Zulip Ali Caglayan (May 09 2022 at 18:45):

Nope

view this post on Zulip Ali Caglayan (May 09 2022 at 18:45):

I've deleted _build_ci and started again seems to be working

view this post on Zulip Ali Caglayan (May 09 2022 at 18:46):

I guess maybe something switched during setup of _build_ci

view this post on Zulip Notification Bot (May 09 2022 at 18:46):

Ali Caglayan has marked this topic as resolved.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Feb 05 2023 at 23:30 UTC