Stream: Coq users

Topic: Compiling Coq Standard Library


view this post on Zulip Alex Sanchez-Stern (Feb 22 2023 at 22:22):

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?

view this post on Zulip 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.

view this post on Zulip Alex Sanchez-Stern (Feb 22 2023 at 22:30):

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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Feb 23 2023 at 18:54):

maybe one got compiled with -opaque and not the other

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Feb 23 2023 at 20:03):

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: Jun 20 2024 at 12:02 UTC