Ralph Matthes (Apr 27 2022 at 16:17): 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?
Pierre-Marie Pédrot (Apr 27 2022 at 16:19):at least, you need the same architecture (32 vs 64 bit)
Karl Palmskog (Apr 27 2022 at 16:19):same OCaml compiler version as well
Pierre-Marie Pédrot (Apr 27 2022 at 16:20):this will be indirectly checked by comparing the checksum of the cmi files
Gaëtan Gilbert (Apr 27 2022 at 16:20):does the ocaml version actually matter?
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
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
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
Gaëtan Gilbert (Apr 27 2022 at 16:24):but isn't checked afair
Ralph Matthes (Apr 27 2022 at 16:24):What else enters into that "magic number"? But I am already warned about the plugins.
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?
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
Gaëtan Gilbert (Apr 27 2022 at 16:25):but not in a way leading to a check failure
Pierre-Marie Pédrot (Apr 27 2022 at 16:25):(Doubt)
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
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'
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).
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).
Gaëtan Gilbert (Apr 30 2022 at 09:06):Do you mean because of code changes?
yes
Gaëtan Gilbert (Apr 30 2022 at 09:07):I should have said "edit and recompile" not just recompile
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.
Gaëtan Gilbert (Apr 30 2022 at 10:04):no, the checksums have been in vo files for a while
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
Guillaume Melquiond (Apr 30 2022 at 10:12):So, it is only the Findlib-based plugins whose checksums were ignored?
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
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.
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.
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.
Paolo Giarrusso (May 22 2022 at 22:44):does Coq accept patches for changelogs of past releases?
Li-yao (May 22 2022 at 23:11):I would assume so.
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: Apr 19 2024 at 11:02 UTC