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 --- lib/system.mli | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'lib/system.mli') diff --git a/lib/system.mli b/lib/system.mli index 2513ca19d..2e286a40c 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -52,6 +52,10 @@ val marshal_in : string -> in_channel -> 'a val digest_out : out_channel -> Digest.t -> unit val digest_in : string -> in_channel -> Digest.t +val marshal_out_segment : string -> out_channel -> 'a -> unit +val marshal_in_segment : string -> in_channel -> 'a * int * Digest.t +val skip_in_segment : string -> in_channel -> int * Digest.t + (** {6 Sending/receiving once with external executable } *) val connect : (out_channel -> unit) -> (in_channel -> 'a) -> string -> 'a -- cgit v1.2.3