Stream: Coq users

Topic: coq-equations install error


view this post on Zulip Ralf Jung (Jun 21 2021 at 12:09):

I am getting strange errors when trying to opam install coq-equations:

### output ###
# [...]
# make[1]: *** [Makefile.coq:654: src/subterm.cmi] Error 2
# File "src/noconf.mli", line 1:
# Error: /home/r/Dokumente/Unisachen/iris/coq-users/examples/_opam/lib/coq//tactics/declare.cmi
#        is not a compiled interface for this version of OCaml.
# It seems to be for an older version of OCaml.

I already reinstalled Coq inside this opam, still the same error

view this post on Zulip Guillaume Melquiond (Jun 21 2021 at 12:11):

There is no file tactics/declare.cmi in recent versions of Coq. So, this is presumably some leftover from an old version, which thus confuses the compiler.

view this post on Zulip Ralf Jung (Jun 21 2021 at 13:08):

ah, this is probably https://github.com/ocaml/opam/issues/4419 then

view this post on Zulip Ralf Jung (Jun 21 2021 at 13:09):

because of course opam fails at the core job of every package manager -- to keep track of the files it manages

view this post on Zulip Janno (Jun 21 2021 at 13:10):

I've had this problem quite often in the past and I've taken to simply deleting the file. My thinking was that if it's a file that should be there I can always reinstall the corresponding package. Interestingly this situation never occurred so deleting is the only thing I ever have to do. If I see multiple errors from the same package I delete the entire package (manually, as in rm) and reinstall it.

view this post on Zulip Ralf Jung (Jun 21 2021 at 13:18):

Yeah, opam uninstall coq followed by rm _opam/lib/coq -rf and reinstalling everything fixed the problem


Last updated: Jan 27 2023 at 02:04 UTC