Stream: Coq devs & plugin devs

Topic: Incompatible assumptions error after re-compiling Coq 8.13


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

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

view this post on Zulip Pierre-Marie Pédrot (Jan 10 2021 at 17:41):

So essentially you have to recompile mathcomp from scratch

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

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

view this post on Zulip Pierre-Marie Pédrot (Jan 10 2021 at 19:46):

Even without reconfiguring, OCaml plugin linking is still going to fail, I believe.

view this post on Zulip Pierre-Marie Pédrot (Jan 10 2021 at 19:46):

It happens a lot for me.

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

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

view this post on Zulip Guillaume Melquiond (Jan 10 2021 at 19:48):

That said, I suppose it might depend on OCaml version.

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

view this post on Zulip Pierre-Marie Pédrot (Jan 10 2021 at 19:59):

Hm, this is weird. Are you sure these files were properly recompiled?

view this post on Zulip Pierre-Marie Pédrot (Jan 10 2021 at 20:00):

Or maybe you're using a version of OCaml that solved reproducibility issues?

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

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

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

view this post on Zulip Gaëtan Gilbert (Jan 10 2021 at 20:43):

perhaps related to https://github.com/coq/coq/issues/11229

view this post on Zulip 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: Oct 16 2021 at 02:03 UTC