From ecda2159a3c3176fb871bbc27b7c6b56d9f0830c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 20 Dec 2013 18:02:19 +0100 Subject: .vi files: .vo files without proofs File format: The .vo file format changed: - after the magic number there are 3 segments. A segment is made of 3 components: bynary int, an ocaml value, a digest. The binary int is the position of the digest, so that one can skip the value without unmarshalling it - the first segment is the library, as before - the second segment is the STM task list - the third segment is the opaque table, as before A .vo file has a complete opaque table (all proof terms are there). A .vi file follows the same format of a .vo file, but some entries in the opaque table are missing. A proof task is stocked instead. Utilities: coqc: option -quick generates a .vi insted of a .vo coq_makefile: target quick to generate all .vi coqdep: generate deps for .vi files too votour: can browse .vi files too, the first question is which segment should be read coqchk: rejects .vi files --- library/library.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'library/library.mli') diff --git a/library/library.mli b/library/library.mli index 8ed3afd66..530209485 100644 --- a/library/library.mli +++ b/library/library.mli @@ -37,7 +37,7 @@ val import_module : bool -> qualid located -> unit val start_library : string -> DirPath.t * string (** {6 End the compilation of a library and save it to a ".vo" file } *) -val save_library_to : DirPath.t -> string -> unit +val save_library_to : ?todo:'a -> DirPath.t -> string -> unit (** {6 Interrogate the status of libraries } *) -- cgit v1.2.3