参考手册(第14.4节)表明coqchk将获取.vo文件列表并键入检查生成它们的.v文件中的内容.(可能)不太可靠的来源表明.vo文件不包含完整的证明条款.因此问题:.vo文件包含什么？coqchk如何使用该信息执行类型检查？
.vo文件包含某些核心结构的"封送"视图,主要是Libobject表的副本,其中包含任意模块级信息,如符号,声明等等.Marshaling是OCaml编译器提供的二进制级序列化格式,因此,.vo文件往往在不同的Coq版本之间不兼容.存储在任何次要数据结构中的任何微小变化Libobject都会造成麻烦.
为避免出现问题,使用校验和.OCaml编译器共享此方法以生成其.cmo文件.
要了解更多细节,我建议您查看负责保存的实际代码.vo,在这里您可以跟踪写入磁盘的确切表.正如您所提到的,"不透明"样张会得到特殊处理,因此确实.vo可以在没有它们的情况下保存文件.这些是所谓的.vio文件.
特别是,关键对象是seg_lib包含Lib.lib_objects模块所携带的所有内容.正如我们之前提到的,a lib_object基本上是一个Dyn.t元素,因此事实上它只能由多态marshaller编写/读取.这是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保持同步的类型.