New compilation mode -vi2vo

To obtain a.vo one can now:
1) coqtop -quick -compile a
2) coqtop -vi2vo a.vi

To make that possible the .vo structure has been complicated.  It is now
made of 5 segments.

               |  vo  | vi  | vi2vo | contents
 --------------+------+-----+-------+------------------------------------
 lib           | Yes  | Yes | Yes   | libstack (modules, notations,...)
 opauqe_univs  | No   | Yes | Yes   | constraints coming from opaque proofs
 discharge     | No   | Yes | No    | data needed to close sections
 tasks         | No   | Yes | No    | STM tasks to produce proof terms
 opaque_proofs | Yes  | Yes | Yes   | proof terms
 --------------+------+-----+-------+------------------------------------

This means one can load only the strictly necessay parts.  Usually one
does not load the tasks segment of a .vi nor the opaque_proof segment of
a .vo, unless one is turning a .vi into a .vo, in which case he load
all the segments.

Optional segments are marshalled as None.  But for lib, all segments
are Array.t of:

               | type
 --------------+---------------------------------------------------------
 lib           | a list of Libobject.obj (n'importe quoi)
 opauqe_univs  | Univ.consraints Future.computation
 discharge     | what Cooking.cook_constr needs
 tasks         | Stm.tasks (a task is system_state * vernacexpr list)
 opaque_proofs | Term.constr Future.computation
 --------------+------+-----+-------+------------------------------------

Invariant: all Future.computation in a vo file (obtained by a vi2vo
compilation or not) have been terminated with Future.join (or
Future.sink).  This means they are values (inside a box).
This invariant does not hold for vi files.  E.g. opauqe_proofs can be
dangling Future.computation (i.e. NotHere exception).  The vi2vo
compilation step will replace them by true values.

Rationale for opaque_univs: in the vi2vo transformation we want to reuse
the lib segment.  Hence the missing pieces have to be put on the side,
not inside.  Opaque proof terms are already in a separte segment.
Universe constraints are not, hence the new opauqe_univs segment.  Such
segment, if present in a .vo file, is always loaded, and
Declare.open_constant will add to the environment the constraints stored
there.  For regular constants this is not necessay since the constraints
are already in their enclosing module (and also in the constant_body).
With vi2vo the constraints coming from the proof are not in the
constant_body (hence not in the enclosing module) but there and are
added to the environment explicitly by Declare.open_constant.

Rationale for discharge: vi2vo produces a proof term in its original
context (in the middle of a section).  Then it has to discharge the
object.  This segment contains the data that is needed in order to do
so.  It is morally the input that Lib.close_section passes to Cooking
(via the insane rewinding of libstack, GlobalRecipe, etc chain).

Checksums: the checksum of .vi and a .vo obtain from it is the same.
This means that if if b.vo has been compiled using a.vi, and then
a.vi is compiled into a.vo, Require Import b works (and recursively
loads a.vo).

7 files changed, 95 insertions, 38 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 74a94465e6..8a133fc483 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -355,6 +355,7 @@ let parse_args arglist =
     |"-with-geoproof" -> Coq_config.with_geoproof := get_bool opt (next ())
     |"-main-channel" -> Spawned.main_channel := get_host_port opt (next())
     |"-control-channel" -> Spawned.control_channel := get_host_port opt (next())
+    |"-vi2vo" -> add_compile false (next ()); Flags.compilation_mode := Vi2Vo
 
     (* Options with zero arg *)
     |"-batch" -> set_batch_mode ()
diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli
index a74f694568..aa64e3f22a 100644
--- a/toplevel/discharge.mli
+++ b/toplevel/discharge.mli
@@ -10,6 +10,7 @@ open Context
 open Cooking
 open Declarations
 open Entries
+open Lazyconstr
 
 val process_inductive :
   named_context -> work_list -> mutual_inductive_body -> mutual_inductive_entry
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 9e3d943c03..e73774c97e 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -635,9 +635,13 @@ module Slaves : sig
     (?redefine_qed:bool -> cache:Summary.marshallable -> Stateid.t -> unit) -> unit
 
   type tasks
-  val dump : unit -> tasks
+  val dump : (Future.UUID.t * int) list -> tasks
   val check_task : string -> tasks -> int -> bool
   val info_tasks : tasks -> (string * float * int) list
+  val finish_task :
+    string ->
+    Library.seg_univ -> Library.seg_discharge -> Library.seg_proofs ->
+    tasks -> int -> unit
 
   val cancel_worker : int -> unit
 
@@ -762,11 +766,11 @@ end = struct (* {{{ *)
   let reach_known_state = ref (fun ?redefine_qed ~cache id -> ())
   let set_reach_known_state f = reach_known_state := f
 
-  type request =
+  type 'a request =
     ReqBuildProof of
-      (Stateid.t * Stateid.t) * Stateid.t * VCS.vcs * Loc.t * string
+      (Stateid.t * Stateid.t) * Stateid.t * VCS.vcs * Loc.t * 'a * string
 
-  let name_of_request (ReqBuildProof (_,_,_,_,s)) = s
+  let name_of_request (ReqBuildProof (_,_,_,_,_,s)) = s
 
   type response =
     | RespBuiltProof of Entries.proof_output list 
@@ -791,19 +795,19 @@ end = struct (* {{{ *)
   type task =
     | TaskBuildProof of (Stateid.t * Stateid.t) * Stateid.t * Stateid.t *
         (Entries.proof_output list Future.assignement -> unit) * cancel_switch
-        * Loc.t * string
+        * Loc.t * Future.UUID.t * string
   let pr_task = function
-    | TaskBuildProof(_,bop,eop,_,_,_,s) ->
+    | TaskBuildProof(_,bop,eop,_,_,_,_,s) ->
         "TaskBuilProof("^Stateid.to_string bop^","^Stateid.to_string eop^
           ","^s^")"
 
-  let request_of_task task =
+  let request_of_task task : Future.UUID.t request =
     match task with
-    | TaskBuildProof (exn_info,bop,eop,_,_,loc,s) ->
-        ReqBuildProof(exn_info,eop,VCS.slice ~start:eop ~stop:bop,loc,s)
+    | TaskBuildProof (exn_info,bop,eop,_,_,loc,uuid,s) ->
+        ReqBuildProof(exn_info,eop,VCS.slice ~start:eop ~stop:bop,loc,uuid,s)
 
   let cancel_switch_of_task = function
-    | TaskBuildProof (_,_,_,_,c,_,_) -> c
+    | TaskBuildProof (_,_,_,_,c,_,_,_) -> c
 
   let build_proof_here_core loc eop () =
     let wall_clock1 = Unix.gettimeofday () in
@@ -818,25 +822,24 @@ end = struct (* {{{ *)
 
   let slave_respond msg =
     match msg with
-    | ReqBuildProof(exn_info,eop,vcs,loc,_) ->
+    | ReqBuildProof(exn_info,eop,vcs,loc,_,_) ->
         VCS.restore vcs;
         VCS.print ();
         let r = RespBuiltProof (
           let l = Future.force (build_proof_here exn_info loc eop) in
           List.iter (fun (_,se) -> Declareops.iter_side_effects (function
             | Declarations.SEsubproof(_,
-               { Declarations.const_body = Declarations.OpaqueDef f;
-                 const_constraints = cst} ) -> 
-                  ignore(Future.join f); ignore(Future.join cst)
+               { Declarations.const_body = Declarations.OpaqueDef f } ) ->
+               Lazyconstr.join_lazy_constr f
             | _ -> ())
           se) l;
           l) in
         VCS.print ();
         r
 
-  let check_task name l i =
+  let check_task_aux name l i =
     match List.nth l i with
-    | ReqBuildProof ((id,valid),eop,vcs,loc,s) ->
+    | ReqBuildProof ((id,valid),eop,vcs,loc,_,s) as req ->
         Pp.msg_info(str(Printf.sprintf "Checking task %d (%s) of %s" i s name));
         VCS.restore vcs;
         try
@@ -848,7 +851,7 @@ end = struct (* {{{ *)
           vernac_interp eop ~proof
             { verbose = false; loc;
               expr = (VernacEndProof (Proved (true,None))) };
-          true
+          Some (req,proof)
         with e -> (try
           match Stateid.get e with
           | None ->
@@ -872,10 +875,38 @@ end = struct (* {{{ *)
                     spc () ++ print e)
         with e ->
           Pp.msg_error (str"unable to print error message: " ++
-                        str (Printexc.to_string e))); false
+                        str (Printexc.to_string e))); None
+
+  let finish_task name u d p l i =
+    match check_task_aux name l i with
+    | None -> exit 1
+    | Some (ReqBuildProof ((id,valid),eop,vcs,loc,bucket,s), (po,pt)) ->
+        let discharge c = List.fold_right Cooking.cook_constr d.(bucket) c in
+        let con =
+          Nametab.locate_constant
+            (Libnames.qualid_of_ident po.Proof_global.id) in
+        let c = Global.lookup_constant con in
+        match c.Declarations.const_body with
+        | Declarations.OpaqueDef lc ->
+            let pr, uc = Lazyconstr.get_opaque_futures lc in
+            let pr = Future.chain ~greedy:true ~pure:true pr discharge in
+            let pr = Future.chain ~greedy:true ~pure:true pr Constr.hcons in
+            ignore(Future.join pr);
+            ignore(Future.join uc);
+            Pp.msg_info(str(Printf.sprintf
+              "Assigning output of task %d (%s) of %s to bucket %d"
+              i s name bucket));
+            u.(bucket) <- uc;
+            p.(bucket) <- pr
+        | _ -> assert false
+  
+  let check_task name l i =
+    match check_task_aux name l i with
+    | Some _ -> true
+    | None -> false
 
   let info_tasks l =
-    CList.map_i (fun i (ReqBuildProof(_,_,_,loc,s)) ->
+    CList.map_i (fun i (ReqBuildProof(_,_,_,loc,_,s)) ->
       let time1 =
         try float_of_string (Aux_file.get !hints loc "proof_build_time")
         with Not_found -> 0.0 in
@@ -894,13 +925,13 @@ end = struct (* {{{ *)
 
   let marshal_err s = raise (MarshalError s)
 
-  let marshal_request oc (req : request) =
+  let marshal_request oc (req : Future.UUID.t request) =
     try marshal_to_channel oc req
     with Failure s | Invalid_argument s | Sys_error s ->
       marshal_err ("marshal_request: "^s)
 
   let unmarshal_request ic =
-    try (Marshal.from_channel ic : request)
+    try (Marshal.from_channel ic : Future.UUID.t request)
     with Failure s | Invalid_argument s | Sys_error s ->
       marshal_err ("unmarshal_request: "^s)
 
@@ -938,16 +969,18 @@ end = struct (* {{{ *)
         let force () : Entries.proof_output list Future.assignement =
           try `Val (build_proof_here_core loc stop ()) with e -> `Exn e in
         let f,assign = Future.create_delegate ~force (State.exn_on id ~valid) in
+        let uuid = Future.uuid f in
         TQueue.push queue
-          (TaskBuildProof(exn_info,start,stop,assign,cancel_switch,loc,name));
+          (TaskBuildProof(exn_info,start,stop,assign,cancel_switch,loc,uuid,name));
         f, cancel_switch
       end else
         build_proof_here exn_info loc stop, cancel_switch
     else 
       let f, assign = Future.create_delegate (State.exn_on id ~valid) in
+      let uuid = Future.uuid f in
       Pp.feedback (Interface.InProgress 1);
       TQueue.push queue
-        (TaskBuildProof(exn_info,start,stop,assign,cancel_switch,loc,name));
+        (TaskBuildProof(exn_info,start,stop,assign,cancel_switch,loc,uuid,name));
       f, cancel_switch
 
   exception RemoteException of std_ppcmds
@@ -991,13 +1024,13 @@ end = struct (* {{{ *)
           let rec loop () =
             let response = unmarshal_response ic in
             match task, response with
-            | TaskBuildProof(_,_,_, assign,_,_,_), RespBuiltProof pl ->
+            | TaskBuildProof(_,_,_, assign,_,_,_,_), RespBuiltProof pl ->
                 assign (`Val pl);
                 (* We restart the slave, to avoid memory leaks.  We could just
                    Pp.feedback (Interface.InProgress ~-1) *)
                 last_task := None;
                 raise KillRespawn
-            | TaskBuildProof(_,_,_, assign,_,_,_),RespError(err_id,valid,e,s) ->
+            | TaskBuildProof(_,_,_, assign,_,_,_,_),RespError(err_id,valid,e,s) ->
                 let e = Stateid.add ~valid (RemoteException e) err_id in
                 assign (`Exn e);
                 Option.iter (State.assign valid) s;
@@ -1029,7 +1062,7 @@ end = struct (* {{{ *)
             msg_warning(strbrk("Marshalling error: "^s^". "^
               "The system state could not be sent to the worker process. "^
               "Falling back to local, lazy, evaluation."));
-            let TaskBuildProof (exn_info, _, stop, assign,_,loc,_) = task in
+            let TaskBuildProof (exn_info, _, stop, assign,_,loc,_,_) = task in
             assign(`Comp(build_proof_here exn_info loc stop));
             Pp.feedback (Interface.InProgress ~-1)
         | MarshalError s ->
@@ -1052,7 +1085,7 @@ end = struct (* {{{ *)
     | Sys_error _ | Invalid_argument _ | End_of_file when !task_cancelled ->
         msg_warning(strbrk "The worker was cancelled.");
         Option.iter (fun task ->
-          let TaskBuildProof (_, start, _, assign, _,_,_) = task in
+          let TaskBuildProof (_, start, _, assign, _,_,_,_) = task in
           let s = "Worker cancelled by the user" in
           let e = Stateid.add ~valid:start (RemoteException (strbrk s)) start in
           assign (`Exn e);
@@ -1066,7 +1099,7 @@ end = struct (* {{{ *)
         msg_warning(strbrk "The worker process died badly.");
         Option.iter (fun task ->
           msg_warning(strbrk "Falling back to local, lazy, evaluation.");
-          let TaskBuildProof (exn_info, _, stop, assign,_,loc,_) = task in
+          let TaskBuildProof (exn_info, _, stop, assign,_,loc,_,_) = task in
           assign(`Comp(build_proof_here exn_info loc stop));
           Pp.feedback (Interface.InProgress ~-1);
         ) !last_task;
@@ -1158,13 +1191,14 @@ end = struct (* {{{ *)
     done
 
   (* For external users this name is nicer than request *)
-  type tasks = request list
-  let dump () =
+  type tasks = int request list
+  let dump f2t_map =
     assert(SlavesPool.is_empty ()); (* ATM, we allow that only if no slaves *)
     let tasks = TQueue.dump queue in
     prerr_endline (Printf.sprintf "dumping %d\n" (List.length tasks));
     let tasks = List.map request_of_task tasks in
-    tasks
+    List.map (function ReqBuildProof(a,b,c,d,x,e) ->
+      ReqBuildProof(a,b,c,d,List.assoc x f2t_map,e)) tasks
 
 end (* }}} *)
 
@@ -1562,7 +1596,7 @@ let join () =
   VCS.print ()
 
 type tasks = Slaves.tasks
-let dump () = Slaves.dump ()
+let dump x = Slaves.dump x
 let check_task name tasks i =
   let vcs = VCS.backup () in
   try
@@ -1572,6 +1606,16 @@ let check_task name tasks i =
     rc
   with e when Errors.noncritical e -> VCS.restore vcs; false
 let info_tasks tasks = Slaves.info_tasks tasks
+let finish_tasks name u d p tasks =
+  let finish_task (_,_,i) =
+    let vcs = VCS.backup () in
+    Future.purify (Slaves.finish_task name u d p tasks) i;
+    Pp.pperr_flush ();
+    VCS.restore vcs in
+  try List.iter finish_task (info_tasks tasks)
+  with e ->
+    Pp.pperrnl Pp.(str"File " ++ str name ++ str ":" ++ spc () ++ print e);
+    exit 1
 
 let merge_proof_branch qast keep brname =
   let brinfo = VCS.get_branch brname in
diff --git a/toplevel/stm.mli b/toplevel/stm.mli
index 0a7473792f..c47bacf651 100644
--- a/toplevel/stm.mli
+++ b/toplevel/stm.mli
@@ -44,10 +44,13 @@ val stop_worker : int -> unit
 val join : unit -> unit
 (* To save to disk an incomplete document *)
 type tasks
-val dump : unit -> tasks
+val dump : (Future.UUID.t * int) list -> tasks
 
 val check_task : string -> tasks -> int -> bool
 val info_tasks : tasks -> (string * float * int) list
+val finish_tasks : string ->
+  Library.seg_univ -> Library.seg_discharge -> Library.seg_proofs ->
+  tasks -> unit
 
 (* Id of the tip of the current branch *)
 val get_current_state : unit -> Stateid.t
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index 6f39725ffd..16cc510866 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -18,10 +18,10 @@ Vernacentries
 Vernac_classifier
 Stm
 Whelp
+Vi_checking
 Vernac
 Ide_slave
 Usage
 Coqloop
 Coqinit
-Vi_checking
 Coqtop
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index abf58df459..b35929fef2 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -367,6 +367,14 @@ let compile verbosely f =
       let _ = load_vernac verbosely long_f_dot_v in
       Stm.finish ();
       check_pending_proofs ();
-      let todo = Stm.dump () in
-      Library.save_library_to ~todo ldir long_f_dot_v
+      Library.save_library_to ~todo:Stm.dump ldir long_f_dot_v
+  | Vi2Vo ->
+      let open Filename in
+      let open Library in
+      Dumpglob.noglob ();
+      let f = if check_suffix f ".vi" then chop_extension f else f in
+      let lfdv, lib, univs, disch, tasks, proofs = load_library_todo f in
+      Stm.set_compilation_hints (Aux_file.load_aux_file_for lfdv);
+      Stm.finish_tasks lfdv univs disch proofs tasks;
+      Library.save_library_raw lfdv lib univs proofs
 
diff --git a/toplevel/vi_checking.ml b/toplevel/vi_checking.ml
index a52a83dfe7..5fae1c4592 100644
--- a/toplevel/vi_checking.ml
+++ b/toplevel/vi_checking.ml
@@ -10,7 +10,7 @@ open Util
 
 let check_vi (ts,f) =
   Dumpglob.noglob ();
-  let tasks, long_f_dot_v = Library.load_library_todo f in
+  let long_f_dot_v, _, _, _, tasks, _ = Library.load_library_todo f in
   Stm.set_compilation_hints (Aux_file.load_aux_file_for long_f_dot_v);
   List.fold_left (fun acc ids -> Stm.check_task f tasks ids && acc) true ts
 
@@ -38,7 +38,7 @@ let schedule_vi_checking j fs =
     let f =
       if Filename.check_suffix f ".vi" then Filename.chop_extension f
       else f in
-    let tasks, long_f_dot_v = Library.load_library_todo f in
+    let long_f_dot_v, _,_,_, tasks, _ = Library.load_library_todo f in
     Stm.set_compilation_hints (Aux_file.load_aux_file_for long_f_dot_v);
     let infos = Stm.info_tasks tasks in
     let eta = List.fold_left (fun a (_,t,_) -> a +. t) 0.0 infos in