Stream: Coq Platform devs & users

Topic: Weird opam effect

view this post on Zulip Michael Soegtrop (Mar 25 2022 at 10:47):

@Karl Palmskog : I have a weird opam effect - maybe you can help me with it. I have coq-vst and coq-compcert installed. Now when I try to uninstall coq-vst, it wants to recompile compcert:

coq-platform-main$ opam uninstall coq-vst
The following actions will be performed:
  - remove    coq-vst      2.9.1
  - recompile coq-compcert 3.10  [uses coq-vst]
===== 1 to recompile | 1 to remove =====
Do you want to continue? [Y/n] n

According to opam, coq-compcert does not use coq-vst, but the other way around. Dou you have a good explanation for this? Is this a bug in opam?

view this post on Zulip Karl Palmskog (Mar 25 2022 at 10:53):

@Michael Soegtrop might be a bug in opam. I don't have any explanation for this, the dependencies in the package definitions all look good.

view this post on Zulip Michael Soegtrop (Mar 25 2022 at 10:55):

Thanks - I will report it then.

Last updated: Jun 03 2023 at 04:30 UTC