Ralf Jung (Jun 21 2021 at 12:09): 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
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.
Ralf Jung (Jun 21 2021 at 13:08):ah, this is probably https://github.com/ocaml/opam/issues/4419 then
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
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.
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: Sep 26 2023 at 13:01 UTC