Compiling Coq Standard Library · Coq users

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?

Alex Sanchez-Stern (Feb 22 2023 at 22:25):

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.

Alex Sanchez-Stern (Feb 22 2023 at 22:30):

Anomaly "Uncaught exception Not_found."
Please report at http://coq.inria.fr/bugs/.

Declare ML Module \"int63_syntax_plugin\".

Other files fail because of a lack of setoid import without the coqlib argument.

Paolo Giarrusso (Feb 23 2023 at 00:22):

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

Paolo Giarrusso (Feb 23 2023 at 00:24):

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?

Paolo Giarrusso (Feb 23 2023 at 00:26):

re 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

Emilio Jesús Gallego Arias (Feb 23 2023 at 00:29):

@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.

Alex Sanchez-Stern (Feb 23 2023 at 18:52):

Hmm, but both Coq's share the same OCaml install I think, so why would the cmxs files be incompatible?

Gaëtan Gilbert (Feb 23 2023 at 18:54):

Alex Sanchez-Stern (Feb 23 2023 at 19:39):

Ahh hmm I'll have to check that. There's an -opaque flag to ocaml too? I thought that was just a coq flag

Paolo Giarrusso (Feb 23 2023 at 20:01):

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

Stream: Coq users

Topic: Compiling Coq Standard Library

Alex Sanchez-Stern (Feb 22 2023 at 22:22):