coq - .vo 文件的结构如何使 coqchk 可以使用它？

Question

引用手册 (Section 14.4) 表明 coqchk 将获取 .vo 文件列表并检查生成它们的 .v 文件中的任何内容。一个(可能)不太可靠的来源表明 .vo 文件不包含完整的证明条款。因此问题是:.vo 文件包含什么？ coqchk 如何使用这些信息来执行类型检查？

Answer 1

.vo文件包含某些核心结构的“编码” View ，主要是 Libobject 的副本表，其中包含任意模块级信息，例如符号、声明等... Marshaling是 OCaml 编译器提供的二进制级序列化格式，因此，.vo文件在不同的 Coq 版本之间往往不兼容。存储在 Libobject 中的任何次要数据结构的任何次要更改会制造麻烦。

为避免出现问题，使用了校验和。此方法由 OCaml 编译器共享以生成其 .cmo文件。

要了解更多详细信息，我建议您查看 the actual code负责保存 .vo ，在这里您可以跟踪写入磁盘的确切表。正如您所提到的，“不透明”证明被给予特殊处理，所以确实是 .vo没有它们也可以保存文件。这些就是所谓的.vio文件。

特别是，关键对象是 seg_lib , 包含所有 Lib.lib_objects模块携带的。正如我们之前提到的，lib_object基本上是 Dyn.t元素，因此实际上它只能由多态编码器写入/读取。这是 IMVHO Coq 的 vo 的一个弱点(但方便)。执行。使用 Marshal 时使消费者不必定义繁琐的序列化函数，另一方面，它很慢，最重要的是有很多对象是不可序列化的，但是类型系统不会遇到这个问题。

一旦进入检查器，它只会读取保存的术语并再次对它们进行类型检查。它需要与 Coq 中使用的内部表示保持同步。见 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

所以在这里你可以看到检查器输入了所有的库信息，但忽略了很多数据类型。模块中的类型 Cic是检查器会知道的，并且必须与 Coq 保持同步的。