a是怎样的。vo文件的结构是否便于coqchk使用?

.vo 文件包含某些核心结构的“封送”视图,主要是 Libobject 表,其中包含任意模块级信息,如符号、声明等。。。 Marshaling 是OCaml编译器提供的二进制级别序列化格式,因此, .vo公司 不同Coq版本之间的文件往往不兼容。存储在 Libobject 会制造麻烦。

为了避免问题,使用校验和。OCaml编译器共享这种方法来生成 .cmo 文件夹。

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

特别是,关键对象是 seg_lib ,包含所有 Lib.lib_objects 模块携带的。如前所述 lib_object 基本上是 Dyn.t 元素,因此实际上它只能由多态封送拆收器写入/读取。这是Coq的一个薄弱(但方便)点 vo 实施使用时 Marshal 另一方面,它的速度很慢,而且最重要的是,有许多对象是不可序列化的,但是类型系统不会发现这个问题。

进入checker后,它只需读取保存的术语并再次键入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保持同步的。

A. .vo 文件包含完整的定义和证明术语。我相信它还包括参考手册中提到的“非逻辑信息”(例如,符号和策略),以便在从 coqtop .

另一方面 .vio 文件(制作人 coqc -quick )仅包含定义,不包含完整的证明术语。