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
---
 kernel/safe_typing.ml  | 6 ++++--
 kernel/safe_typing.mli | 6 ++++--
 2 files changed, 8 insertions(+), 4 deletions(-)

(limited to 'kernel')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 66bc907897..3e9b646c17 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -657,9 +657,11 @@ let start_library dir senv =
     modvariant = LIBRARY;
     imports = senv.imports }
 
-let export senv dir =
+let export compilation_mode senv dir =
   let senv =
-    try join_safe_environment senv
+    try
+      if compilation_mode = Flags.BuildVi then senv (* FIXME: cleanup future*)
+      else join_safe_environment senv
     with e -> Errors.errorlabstrm "future" (Errors.print e)
   in
   let () = check_current_library dir senv in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index dcdb866bfc..e2d1e37e9d 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -115,8 +115,10 @@ type native_library = Nativecode.global list
 
 val start_library : DirPath.t -> module_path safe_transformer
 
-val export : safe_environment -> DirPath.t ->
-  module_path * compiled_library * native_library
+val export :
+  Flags.compilation_mode ->
+  safe_environment -> DirPath.t ->
+    module_path * compiled_library * native_library
 
 val import : compiled_library -> Digest.t ->
   (module_path * Nativecode.symbol array) safe_transformer
-- 
cgit v1.2.3