Merge PR #8642: Compiled interfaces with -vos and -vok options

Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot

2 files changed, 16 insertions, 6 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index 5c6df26cbb..c399b69a77 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2801,13 +2801,21 @@ let handle_failure (e, info) vcs =
   VCS.print ();
   Exninfo.iraise (e, info)
 
-let snapshot_vio ~doc ~output_native_objects ldir long_f_dot_vo =
+let snapshot_vio ~create_vos ~doc ~output_native_objects ldir long_f_dot_vo =
   let doc = finish ~doc in
   if List.length (VCS.branches ()) > 1 then
     CErrors.user_err ~hdr:"stm" (str"Cannot dump a vio with open proofs");
-  Library.save_library_to ~todo:(dump_snapshot ()) ~output_native_objects
-    ldir long_f_dot_vo
-    (Global.opaque_tables ());
+  (* LATER: when create_vos is true, it could be more efficient to not allocate the futures; but for now it seems useful for synchronization of the workers,
+  below, [snapshot] gets computed even if [create_vos] is true. *)
+  let (tasks,counters) = dump_snapshot() in
+  let except = List.fold_left (fun e (r,_) ->
+     Future.UUIDSet.add r.Stateid.uuid e) Future.UUIDSet.empty tasks in
+  let todo_proofs =
+    if create_vos
+      then Library.ProofsTodoSomeEmpty except
+      else Library.ProofsTodoSome (except,tasks,counters)
+    in
+  Library.save_library_to todo_proofs ~output_native_objects ldir long_f_dot_vo (Global.opaque_tables ());
   doc
 
 let reset_task_queue = Slaves.reset_task_queue
diff --git a/stm/stm.mli b/stm/stm.mli
index 29e4b02e3f..841adcf05b 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -159,8 +159,10 @@ val join : doc:doc -> doc
    - if the worker pool is empty, all tasks are saved
    - if the worker proof is not empty, then it waits until all workers
      are done with their current jobs and then dumps (or fails if one
-     of the completed tasks is a failure) *)
-val snapshot_vio : doc:doc -> output_native_objects:bool -> DirPath.t -> string -> doc
+     of the completed tasks is a failure).
+   Note: the create_vos argument is used in the "-vos" mode, where the
+   proof tasks are not dumped into the output file. *)
+val snapshot_vio : create_vos:bool -> doc:doc -> output_native_objects:bool -> DirPath.t -> string -> doc
 
 (* Empties the task queue, can be used only if the worker pool is empty (E.g.
  * after having built a .vio in batch mode *)