Hey all, I have an error message question. I've been messing around with compiling parts of the Coq standard library with an external Coq so that I can integrate them into my proof search infrastructure. Most of the files compile fine after some tweaks, but there are a couple of files that have issues.
When trying to compile
theories/Numbers/Cyclic/Int63/Int63.v, I'm getting the error
Error: while loading <coq-directory>/plugins/ltac/ltac_plugin.cmxs: implementation mismatch on Vernacextend
If I use the version of Coq that is in
bin/coqc, in the build directory then there's no error, but the same flags with my global coqc give that error. Both coqc's are 8.10.2 with ocaml 4.07.1, the only difference in the --version output is the build date. It seems like something is encoded into the ltac_plugin.cmxs file that is specific to the
bin/coqc compiler, causing the mismatch.
So first, what does this error message actually mean? And second, is there a way I can get around it, either by ignoring the incompatibility with a flag, or building the cmxs file with respect to my global coq install?
Oh, and if I don't use the
-coqlib . flag that error doesn't appear and it instead fails later down in the file. I'm guessing that flag is what's causing it to try to load the plugins directory.
Without -coqlib, this file gives the error:
Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/.
when trying to run the statement:
Declare ML Module \"int63_syntax_plugin\".
Other files fail because of a lack of setoid import without the coqlib argument.
details have varied, but different builds need not be binary compatible — which shouldn't be a problem as long as you never mix two Coq builds
assuming sertop isn't involved here, however many patches you've added to your "external Coq", can you use the pertaining ltac plugin and stdlib?
Declare Module, I guess that's a typo for
Declare ML Module "int63_syntax_plugin". — and if it is, nothing to add there, except the mismatch might be relevant again
@Alex Sanchez-Stern indeed both OCaml and Coq encode a hash of the modules they import in a module, hence the mismatch.
That's a safety feature over just segfaulting if the modules / vo don't share the same binary interface, and indeed, in general it is not possible to avoid.
Hmm, but both Coq's share the same OCaml install I think, so why would the cmxs files be incompatible?
maybe one got compiled with -opaque and not the other
Ahh hmm I'll have to check that. There's an -opaque flag to ocaml too? I thought that was just a coq flag
Even rebuilding the same Coq isn't necessarily safe, speaking from my devops experience; Coq dropped build timestamps from the internal version check but I think that was after 8.10? The version hashes include hashes of some Coq binaries/plugin, so I wouldn't expect code changes to preserve compatibility
However, this isn't documented, changed over time, and bugs exist https://github.com/coq/coq/issues/11037 https://github.com/coq/coq/issues/11229 https://github.com/coq/coq/pull/11227 https://github.com/coq/coq/issues/17207
Last updated: Oct 04 2023 at 20:01 UTC