I am getting strange errors when trying to
opam install coq-equations:
### output ### # [...] # make: *** [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
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.
ah, this is probably https://github.com/ocaml/opam/issues/4419 then
because of course opam fails at the core job of every package manager -- to keep track of the files it manages
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.
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