Stream: Coq users

Topic: how portable are .vo files?


view this post on Zulip Ralph Matthes (Apr 27 2022 at 16:17):

I would like to compile numerous .v files on a powerful machine and then copy the obtained .vo files to a consumer laptop and continue development of the .v files from there (but rather on the leaves of the dependency tree). What do I have to observe to avoid rejection of the injected .vo files when executing import statements, say in ProofGeneral? I expect that I have to compile with the same version of Ocaml. But does it go beyond? Does it need to be the same OPAM version on both sides? What if one system runs with Ubuntu, the other with Debian (maybe of different years)? May there be a problem if one processor is from AMD, the other from Intel?

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2022 at 16:19):

at least, you need the same architecture (32 vs 64 bit)

view this post on Zulip Karl Palmskog (Apr 27 2022 at 16:19):

same OCaml compiler version as well

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2022 at 16:20):

this will be indirectly checked by comparing the checksum of the cmi files

view this post on Zulip Gaëtan Gilbert (Apr 27 2022 at 16:20):

does the ocaml version actually matter?

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2022 at 16:21):

@Gaëtan Gilbert not strictly necessarily so, as long as the produced binary files are the same

view this post on Zulip Gaëtan Gilbert (Apr 27 2022 at 16:21):

Pierre-Marie Pédrot said:

this will be indirectly checked by comparing the checksum of the cmi files

I don't think those are in .vo

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2022 at 16:22):

the hash of the plugins on which a vo file depends are stored in the vo

view this post on Zulip Gaëtan Gilbert (Apr 27 2022 at 16:24):

but isn't checked afair

view this post on Zulip Ralph Matthes (Apr 27 2022 at 16:24):

What else enters into that "magic number"? But I am already warned about the plugins.

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2022 at 16:24):

@Gaëtan Gilbert it will indirectly change the hash of depending files, won't it?

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2022 at 16:25):

@Ralph Matthes the magic number in itself is just the Coq version. We also store the hashes of the depending vo files

view this post on Zulip Gaëtan Gilbert (Apr 27 2022 at 16:25):

but not in a way leading to a check failure

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2022 at 16:25):

(Doubt)

view this post on Zulip Gaëtan Gilbert (Apr 27 2022 at 16:28):

suppose you compile ltac once, so ltac_plugin.cmxs has checksum 1
then you get the 1 in Ltac.vo because it has the declare ML blabla, so Ltac.vo has checksum 1'
then Prelude.vo has checksum 1'' because it depends on Ltac.vo
now you recompile ltac_plugin getting checksum 2
you can still load Prelude.vo
if you coqc Hurkens.vo (without recompiling ltac.vo/prelude.vo) it will get checksum 1''' without ever computing the current checksum of ltac_plugin.cmxs

view this post on Zulip Gaëtan Gilbert (Apr 27 2022 at 16:29):

however if you now recompile Ltac.vo it gets checksum 2', and loading Prelude.vo or Hurkens.vo will fail because they expect it to have checksum 1'

view this post on Zulip Ralph Matthes (Apr 27 2022 at 16:30):

Based on your helpful answers, I'll conduct precise tests for my scenario and report back. I can assure you that all is 64 bit (and Ubuntu and Debian).

view this post on Zulip Ralph Matthes (Apr 30 2022 at 08:32):

@Gaëtan Gilbert I am worried about recompilation of ltac_plugin leading to a different checksum. Do you mean because of code changes? Or inevitably? If I understand you well, I can have Coq installations on two different machines, with their separately compiled plugins (an aside: can the compiled code be moved between systems and stay functional?), but I have to use the very same .vo files of the Coq library (at least all those whose .v files have the "ML blabla") on both machines if I want to be able to move .vo files of my application library between the two machines (which was my initial desire).

view this post on Zulip Gaëtan Gilbert (Apr 30 2022 at 09:06):

Do you mean because of code changes?

yes

view this post on Zulip Gaëtan Gilbert (Apr 30 2022 at 09:07):

I should have said "edit and recompile" not just recompile

view this post on Zulip Guillaume Melquiond (Apr 30 2022 at 10:03):

I don't think it has been written yet, but of all these horror stories about checksum only matters for the master branch of Coq. If you are using Coq 8.15 or earlier, .vo files do not depend on plugins, as far as I understand.

view this post on Zulip Gaëtan Gilbert (Apr 30 2022 at 10:04):

no, the checksums have been in vo files for a while

view this post on Zulip Gaëtan Gilbert (Apr 30 2022 at 10:06):

https://github.com/coq/coq/commit/5dc3efa19bf27613a8441c43b68121d222cdc675 https://github.com/coq/coq/pull/11407 8.12

view this post on Zulip Guillaume Melquiond (Apr 30 2022 at 10:12):

So, it is only the Findlib-based plugins whose checksums were ignored?

view this post on Zulip Gaëtan Gilbert (Apr 30 2022 at 10:17):

only for a couple weeks between https://github.com/coq/coq/pull/15220 and https://github.com/coq/coq/pull/15651

view this post on Zulip Ralph Matthes (May 01 2022 at 23:00):

@Gaëtan Gilbert I have successfully injected all .vo files of Coq and all .vo files of UniMath from a machine with AMD CPU running Debian 10 into my installation on a machine with Intel CPU running Ubuntu 22.04. So, I can step through all UniMath .v files with ProofGeneral and can compile selectively on the target machine. Such injection can save me close to 2 CPU hours (adding the activity on all physical threads). For many years, this worked out of the box just by doing a full synchronization of the directory of my UniMath clone between the computers (and if I am not totally mistaken, I did not need to synchronize the Coq installations that resided in a submodule of UniMath). As you wrote, there is no need to transport plugin code, which was my encouragement - thank you for that.

view this post on Zulip Paolo Giarrusso (May 22 2022 at 22:38):

Have things changed since https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/Incompatible.20assumptions.20error.20after.20re-compiling.20Coq.208.2E13 ? That thread suggests that rebuilding the same coqc can (could?) produce different binaries.

view this post on Zulip Paolo Giarrusso (May 22 2022 at 22:43):

... I see the problem: the most relevant change (https://github.com/coq/coq/pull/13863) omits a changelog.

view this post on Zulip Paolo Giarrusso (May 22 2022 at 22:44):

does Coq accept patches for changelogs of past releases?

view this post on Zulip Li-yao (May 22 2022 at 23:11):

I would assume so.

view this post on Zulip Théo Zimmermann (May 24 2022 at 15:58):

Sure, but the change to the changelog will only be visible when looking at the documentation of a newer version. That's still useful.


Last updated: Jan 31 2023 at 12:01 UTC