Tej Chajed (Jan 10 2021 at 17:37): Tej Chajed (Jan 10 2021 at 17:37):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.
Pierre-Marie Pédrot (Jan 10 2021 at 17:39):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.
Pierre-Marie Pédrot (Jan 10 2021 at 17:41):So essentially you have to recompile mathcomp from scratch
Tej Chajed (Jan 10 2021 at 19:03):Okay that makes sense. I guess it basically boils down to Coq builds not being reproducible due to a timestamp.
Guillaume Melquiond (Jan 10 2021 at 19:44):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.
Pierre-Marie Pédrot (Jan 10 2021 at 19:46):Even without reconfiguring, OCaml plugin linking is still going to fail, I believe.
Pierre-Marie Pédrot (Jan 10 2021 at 19:46):It happens a lot for me.
Pierre-Marie Pédrot (Jan 10 2021 at 19:46):So if you're dev is pure vo it might be fine, but otherwise expect trouble.
Guillaume Melquiond (Jan 10 2021 at 19:47):It should not. (And because I was not completely sure, I tried before answering. The checksums are identical.)
Guillaume Melquiond (Jan 10 2021 at 19:48):That said, I suppose it might depend on OCaml version.
Guillaume Melquiond (Jan 10 2021 at 19:52):(To be precise, I tried with both plugins/firstorder/ground_plugin.cmxs and theories/Reals/Reals.vo, hoping that would be representative enough.)
Pierre-Marie Pédrot (Jan 10 2021 at 19:59):Hm, this is weird. Are you sure these files were properly recompiled?
Pierre-Marie Pédrot (Jan 10 2021 at 20:00):Or maybe you're using a version of OCaml that solved reproducibility issues?
Guillaume Melquiond (Jan 10 2021 at 20:08):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.
Guillaume Melquiond (Jan 10 2021 at 20:08):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
Guillaume Melquiond (Jan 10 2021 at 20:10):As you can see, a bunch of packages can be built reproducibly (despite OCaml's best efforts).
Gaëtan Gilbert (Jan 10 2021 at 20:43):perhaps related to https://github.com/coq/coq/issues/11229
Guillaume Melquiond (Jan 10 2021 at 21:08):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: Dec 01 2023 at 06:01 UTC