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 --- checker/check.ml | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) (limited to 'checker/check.ml') diff --git a/checker/check.ml b/checker/check.ml index 366eb3695..5a1671fe6 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -301,12 +301,11 @@ let intern_from_file (dir, f) = let (md,table,digest) = try let ch = with_magic_number_check raw_intern_library f in - let (md:Cic.library_disk) = System.marshal_in f ch in - let digest = System.digest_in f ch in - let (table:Cic.opaque_table) = System.marshal_in f ch in + let (md:Cic.library_disk), _, digest = System.marshal_in_segment f ch in + let (tasks:'a option), _, _ = System.marshal_in_segment f ch in + let (table:Cic.opaque_table), pos, checksum = + System.marshal_in_segment f ch in (* Verification of the final checksum *) - let pos = pos_in ch in - let checksum = System.digest_in f ch in let () = close_in ch in let ch = open_in f in if not (String.equal (Digest.channel ch pos) checksum) then @@ -315,6 +314,9 @@ let intern_from_file (dir, f) = if dir <> md.md_name then errorlabstrm "intern_from_file" (name_clash_message dir md.md_name f); + if tasks <> None then + errorlabstrm "intern_from_file" + (str "The file "++str f++str " contains unfinished tasks"); (* Verification of the unmarshalled values *) Validate.validate !Flags.debug Values.v_lib md; Validate.validate !Flags.debug Values.v_opaques table; -- cgit v1.2.3