.vo 文件是如何构造的，以便 coqchk 可以使用它？

Question

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

Answer 1

.vo 文件包含完整的定义和证明条款。我相信它还包括参考手册中提到的 "non-logical information"（例如，符号和策略），以便在从 coqtop.

加载库时可以使用它

另一方面，.vio 文件（由 coqc -quick 生成）仅包含定义而不包含完整的证明项。

Answer 2

.vo 文件包含某些核心结构的 "marshaled" 视图，主要是 Libobject table 的副本，其中包含任意 module-level 信息，例如作为符号、声明等... Marshaling 是 OCaml 编译器提供的 binary-level 序列化格式，因此，.vo 文件在不同的 Coq 版本之间往往不兼容。 Libobject 中存储的任何次要数据结构的任何微小更改都会造成麻烦。

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

要了解更多详细信息，我建议您查看负责保存 .vo 的 the actual code，在这里您可以跟踪写入磁盘的确切 table。正如您所提到的，"opaque" 校样被给予特殊处理，因此 .vo 文件确实可以在没有它们的情况下保存。这些是 so-called .vio 个文件。

特别是，关键对象是seg_lib，包含模块携带的所有Lib.lib_objects。正如我们之前提到的，一个 lib_object 基本上是一个 Dyn.t 元素，因此实际上它只能被多态编组器 written/read 。这是 IMVHO Coq vo 实现的一个弱点（但很方便）。虽然使用 Marshal 使消费者不必定义繁琐的序列化函数，但另一方面，它很慢，而且最重要的是有许多对象不可序列化，但是类型系统不会发现这个问题。

进入检查器后，它只会读取保存的条款并再次 type-check 它们。它需要与 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 保持同步的类型。

.vo 文件是如何构造的，以便 coqchk 可以使用它？

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

file-format

coq