coqchk regression: "Fatal Error: User error: Inconsistent assumptions over module Coq.Init.Byte ."

[RalfJung]

Description of the problem

Yesterday, coqchk started failing on our CI. The commit where it started touches only docs, so this is most likely caused by a coqchk regression. You can see a failing log here.

Coq Version

Last version that worked:

name        coq
version     dev
source-hash fdcfe8b7
The Coq Proof Assistant, version 8.12+alpha (February 2020)
compiled on Feb 18 2020 8:27:53 with OCaml 4.07.1

First version that broke:

name        coq
version     dev
source-hash 43c3c7d6
The Coq Proof Assistant, version 8.12+alpha (February 2020)
compiled on Feb 18 2020 21:14:55 with OCaml 4.07.1

That corresponds to this commit range.

[SkySkimmer]

We make validate in our CI job for Iris so this is quite strange.

[SkySkimmer]

That corresponds to this commit range.

So #10204 #11529 #11530
I don't see how the other 2 could get this result so cc @ejgallego for #11529

[RalfJung]

Indeed something is strange, this does not reproduce locally.

Maybe there is a problem with upgrading an existing Coq install in-place?

[RalfJung]

Or maybe it is related to ocaml/opam#4091

[ejgallego]

Maybe there is a problem with upgrading an existing Coq install in-place?

If you are not doing make clean then indeed bad things can happen. Proper incremental builds using make are not supported if the set of target files changes [they will be once we have Dune, but only between commits after the bootstrap]

[RalfJung]

We are using opam, so we shouldn't have to manually clean anything.

[rjbou]

Some explanation in this ocaml/opam#4091 (comment)

[RalfJung]

@rjbou thanks!
So, could this lead to opam not removing old files when uninstalling/upgrading coq?

[RalfJung]

Yeah looks like clearing the opam state made this issue go away. Sorry for the noise!