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

4 files changed, 53 insertions, 19 deletions

diff --git a/vernac/library.ml b/vernac/library.ml
index 8125c3de35..244424de6b 100644
--- a/vernac/library.ml
+++ b/vernac/library.ml
@@ -430,23 +430,33 @@ let error_recursively_dependent_library dir =
 (* Security weakness: file might have been changed on disk between
    writing the content and computing the checksum... *)
 
-let save_library_to ?todo ~output_native_objects dir f otab =
-  let except = match todo with
-    | None ->
-        (* XXX *)
-        (* assert(!Flags.compilation_mode = Flags.BuildVo); *)
-        assert(Filename.check_suffix f ".vo");
-        Future.UUIDSet.empty
-    | Some (l,_) ->
-        assert(Filename.check_suffix f ".vio");
-        List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e)
-          Future.UUIDSet.empty l in
+type ('document,'counters) todo_proofs =
+ | ProofsTodoNone (* for .vo *)
+ | ProofsTodoSomeEmpty of Future.UUIDSet.t (* for .vos *)
+ | ProofsTodoSome of Future.UUIDSet.t * ((Future.UUID.t,'document) Stateid.request * bool) list * 'counters (* for .vio *)
+
+let save_library_to todo_proofs ~output_native_objects dir f otab =
+  assert(
+    let expected_extension = match todo_proofs with
+      | ProofsTodoNone -> ".vo"
+      | ProofsTodoSomeEmpty _ -> ".vos"
+      | ProofsTodoSome _ -> ".vio"
+      in
+    Filename.check_suffix f expected_extension);
+  let except = match todo_proofs with
+    | ProofsTodoNone -> Future.UUIDSet.empty
+    | ProofsTodoSomeEmpty except -> except
+    | ProofsTodoSome (except,l,_) -> except
+    in
   let cenv, seg, ast = Declaremods.end_library ~output_native_objects ~except dir in
   let opaque_table, f2t_map = Opaqueproof.dump ~except otab in
   let tasks, utab =
-    match todo with
-    | None -> None, None
-    | Some (tasks, rcbackup) ->
+    match todo_proofs with
+    | ProofsTodoNone -> None, None
+    | ProofsTodoSomeEmpty _except ->
+        None,
+        Some (Univ.ContextSet.empty,false)
+    | ProofsTodoSome (_except, tasks, rcbackup) ->
         let tasks =
           List.map Stateid.(fun (r,b) ->
             try { r with uuid = Future.UUIDMap.find r.uuid f2t_map }, b
diff --git a/vernac/library.mli b/vernac/library.mli
index 6a32413248..ec485e6408 100644
--- a/vernac/library.mli
+++ b/vernac/library.mli
@@ -36,10 +36,18 @@ type seg_univ = (* all_cst, finished? *)
   Univ.ContextSet.t * bool
 type seg_proofs = Opaqueproof.opaque_proofterm array
 
-(** End the compilation of a library and save it to a ".vo" file.
+(** End the compilation of a library and save it to a ".vo" file,
+    a ".vio" file, or a ".vos" file, depending on the todo_proofs
+    argument.
     [output_native_objects]: when producing vo objects, also compile the native-code version. *)
+
+type ('document,'counters) todo_proofs =
+ | ProofsTodoNone (* for .vo *)
+ | ProofsTodoSomeEmpty of Future.UUIDSet.t (* for .vos *)
+ | ProofsTodoSome of Future.UUIDSet.t * ((Future.UUID.t,'document) Stateid.request * bool) list * 'counters (* for .vio *)
+
 val save_library_to :
-  ?todo:(((Future.UUID.t,'document) Stateid.request * bool) list * 'counters) ->
+  ('document,'counters) todo_proofs ->
   output_native_objects:bool ->
   DirPath.t -> string -> Opaqueproof.opaquetab -> unit
 
diff --git a/vernac/loadpath.ml b/vernac/loadpath.ml
index bea0c943c3..b3dc254a63 100644
--- a/vernac/loadpath.ml
+++ b/vernac/loadpath.ml
@@ -138,6 +138,18 @@ let select_vo_file ~warn loadpath base =
         System.where_in_path ~warn loadpath name in
       Some (lpath, file)
     with Not_found -> None in
+  if !Flags.load_vos_libraries then begin
+    (* If the .vos file exists and is not empty, it describes the library.
+       If the .vos file exists and is empty, then load the .vo file.
+       If the .vos file is missing, then fail. *)
+    match find ".vos" with
+    | None -> Error LibNotFound
+    | Some (_, vos as resvos) ->
+        if (Unix.stat vos).Unix.st_size > 0 then Ok resvos else
+        match find ".vo" with
+        | None -> Error LibNotFound
+        | Some resvo -> Ok resvo
+  end else
   match find ".vo", find ".vio" with
   | None, None ->
     Error LibNotFound
@@ -189,8 +201,10 @@ let error_unmapped_dir qid =
             ])
 
 let error_lib_not_found qid =
+  let vos = !Flags.load_vos_libraries in
+  let vos_msg = if vos then [Pp.str " (while searching for a .vos file)"] else [] in
   CErrors.user_err ~hdr:"load_absolute_library_from"
-    Pp.(seq [ str "Cannot find library "; Libnames.pr_qualid qid; str" in loadpath"])
+    Pp.(seq ([ str "Cannot find library "; Libnames.pr_qualid qid; str" in loadpath"]@vos_msg))
 
 let try_locate_absolute_library dir =
   match locate_absolute_library dir with
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index edff80af00..ade291918e 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -406,8 +406,10 @@ let err_notfound_library ?from qid =
   | Some from ->
     str " with prefix " ++ DirPath.print from ++ str "."
   in
+  let bonus =
+    if !Flags.load_vos_libraries then " (While searching for a .vos file.)" else "" in
   user_err ?loc:qid.CAst.loc ~hdr:"locate_library"
-     (strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix)
+     (strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix ++ str bonus)
 
 let print_located_library qid =
   let open Loadpath in
@@ -830,7 +832,7 @@ let vernac_scheme l =
 	       Option.iter (fun lid -> Dumpglob.dump_definition lid false "def") lid;
 	       match s with
 	       | InductionScheme (_, r, _)
-	       | CaseScheme (_, r, _) 
+               | CaseScheme (_, r, _)
 	       | EqualityScheme r -> dump_global r) l;
   Indschemes.do_scheme l