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/global.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'library/global.ml') diff --git a/library/global.ml b/library/global.ml index dac840ddb..9515ff1a8 100644 --- a/library/global.ml +++ b/library/global.ml @@ -24,7 +24,8 @@ end = struct let global_env = ref Safe_typing.empty_environment let join_safe_environment () = - global_env := Safe_typing.join_safe_environment !global_env + if !Flags.compilation_mode <> Flags.BuildVi then + global_env := Safe_typing.join_safe_environment !global_env let () = Summary.declare_summary "Global environment" @@ -127,7 +128,7 @@ let mind_of_delta_kn kn = (** Operations on libraries *) let start_library dir = globalize (Safe_typing.start_library dir) -let export s = Safe_typing.export (safe_env ()) s +let export s = Safe_typing.export !Flags.compilation_mode (safe_env ()) s let import cenv digest = globalize (Safe_typing.import cenv digest) -- cgit v1.2.3