I was trying to update the Coq test in its Homebrew formula (https://github.com/Homebrew/homebrew-core/pull/68692) and surprisingly merely recompiling Coq made math-comp incompatible, with the usual "makes inconsistent assumptions for Ltac" message when you upgrade Coq. Is this expected? It's the exact same source code for Coq. I don't know enough about Coq's dependency tracking to understand what's going on here.
Coq code keep a hash of the ML plugins they depend on. Furthermore, OCaml code keeps metadata related to compilation details like time and whatnot. The net result is that if you have a vo file that depends on a plugin that was recompiled, it will error out.
So essentially you have to recompile mathcomp from scratch
Okay that makes sense. I guess it basically boils down to Coq builds not being reproducible due to a timestamp.
More precisely, it is the configure
script which sets the timestamp. If you do not reconfigure Coq, you will get byte-to-byte identical .vo
files.
Even without reconfiguring, OCaml plugin linking is still going to fail, I believe.
It happens a lot for me.
So if you're dev is pure vo it might be fine, but otherwise expect trouble.
It should not. (And because I was not completely sure, I tried before answering. The checksums are identical.)
That said, I suppose it might depend on OCaml version.
(To be precise, I tried with both plugins/firstorder/ground_plugin.cmxs
and theories/Reals/Reals.vo
, hoping that would be representative enough.)
Hm, this is weird. Are you sure these files were properly recompiled?
Or maybe you're using a version of OCaml that solved reproducibility issues?
I am sure they were recompiled. (It was a fullblown make clean
.) As for the version of OCaml, it is 4.07.1, so nothing fancy.
By the way, if you want a feel of whether OCaml programs can be built reproducibly, have a look at https://tests.reproducible-builds.org/debian/issues/stretch/ocaml_captures_build_path_issue.html
As you can see, a bunch of packages can be built reproducibly (despite OCaml's best efforts).
perhaps related to https://github.com/coq/coq/issues/11229
Oh right, I had forgotten about the garbage collector being dependent on the content of the directories, and thus on the compilation order chosen by the build system.
Last updated: Jun 08 2023 at 04:01 UTC