How is a .vo file structured so that coqchk may use it?

Question

The reference manual (Section 14.4) indicates that coqchk will take a list of .vo files and type check whatever was in the .v files that produced them. A (possibly) less reliable source indicated that .vo files don't contain full proof terms. Hence the questions: What do .vo files contain? How does coqchk use that information to perform type checking?

Answer 1

.vo files contain a "marshaled" view of certain core structures, mainly a copy of the Libobject table, which contains arbitrary module-level information such as notations, declarations, etc... Marshaling is a binary-level serialization format provided by the OCaml compiler, thus, .vo files tend to be incompatible among different Coq versions. Any minor change in any minor data structure that is stored in the Libobject will create trouble.

To avoid problems, checksums are used. This approach is shared by the OCaml compiler to generate its .cmo files.

To understand more details I suggest you have a look to the actual code responsible of saving a .vo, here you can track the exact tables that are written to disk. As you have mentioned, "opaque" proofs are given special treatment, so indeed a .vo file can be saved without them. These are the so-called .vio files.

In particular, the key object is seg_lib, containinig all the Lib.lib_objects that the module carries. As we mentioned before, a lib_object is basically a Dyn.t element, thus in fact it can only be written/read by the polymorphic marshaller. This is IMVHO a weak (but convenient) point of Coq's vo implementation. While using Marshal frees consumers from having to define cumbersome serialization functions, on the other hand, it is slow, and above all there are many objects that are not serializable, however the type system won't catch this problem.

Once in the checker, it just reads the saved terms and type-check them again. It needs to be kept in sync with the internal representation used in Coq. See checker/check.ml:intern_from_file:

let ch = System.with_magic_number_check raw_intern_library f in
let (sd : Cic.summary_disk), _, digest = marshal_in_segment f ch in
let (md : Cic.library_disk), _, digest = marshal_in_segment f ch in
let (opaque_csts :'a option), _, udg   = marshal_in_segment f ch in
let (discharging :'a option), _, _     = marshal_in_segment f ch in
let (tasks : 'a option), _, _          = marshal_in_segment f ch in
let (table : Cic.opaque_table), pos, checksum = marshal_in_segment f ch

So here you can see the checker inputs all the library information, but ignores quite a few datatypes. The types in the module Cic are the ones that the checker will know about, and the ones that must be kept in sync with Coq.