From b245a6c46bc3ef70142e8a165f6cde54265b941e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 20 May 2019 11:51:31 +0200
Subject: Statically ensure the content of delayed proofs in vio file.

Before, we would store futures, but it was actually ensured by the
upper layers that they were either evaluated or stored by the STM
somewhere else. We simply replace this type with an option, thus
removing the Future.computation type from vo/vio files.

This also enhances debug printing, as the latter is unable to properly
print futures.
---
 library/library.ml  | 22 ++++++----------------
 library/library.mli |  4 ++--
 2 files changed, 8 insertions(+), 18 deletions(-)

(limited to 'library')

diff --git a/library/library.ml b/library/library.ml
index 9f4eb531ed..3bc2e84054 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -276,8 +276,8 @@ let in_import_library : DirPath.t list * bool -> obj =
 (** Delayed / available tables of opaque terms *)
 
 type 'a table_status =
-  | ToFetch of 'a Future.computation array delayed
-  | Fetched of 'a Future.computation array
+  | ToFetch of 'a option array delayed
+  | Fetched of 'a option array
 
 let opaque_tables =
   ref (LibraryMap.empty : (Constr.constr table_status) LibraryMap.t)
@@ -315,7 +315,7 @@ let access_opaque_table dp i =
 let access_univ_table dp i =
   try
     let what = "universe contexts of opaque proofs" in
-    Some (access_table what univ_tables dp i)
+    access_table what univ_tables dp i
   with Not_found -> None
 
 let () =
@@ -328,9 +328,9 @@ let () =
 type seg_sum = summary_disk
 type seg_lib = library_disk
 type seg_univ = (* true = vivo, false = vi *)
-  Univ.ContextSet.t Future.computation array * Univ.ContextSet.t * bool
+  Univ.ContextSet.t option array * Univ.ContextSet.t * bool
 type seg_discharge = Opaqueproof.cooking_info list array
-type seg_proofs = Constr.constr Future.computation array
+type seg_proofs = Constr.constr option array
 
 let mk_library sd md digests univs =
   {
@@ -590,7 +590,7 @@ let save_library_to ?todo ~output_native_objects dir f otab =
         List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e)
           Future.UUIDSet.empty l in
   let cenv, seg, ast = Declaremods.end_library ~output_native_objects ~except dir in
-  let opaque_table, univ_table, disch_table, f2t_map = Opaqueproof.dump otab in
+  let opaque_table, univ_table, disch_table, f2t_map = Opaqueproof.dump ~except otab in
   let tasks, utab, dtab =
     match todo with
     | None -> None, None, None
@@ -603,16 +603,6 @@ let save_library_to ?todo ~output_native_objects dir f otab =
         Some (tasks,rcbackup),
         Some (univ_table,Univ.ContextSet.empty,false),
         Some disch_table in
-  let except =
-    Future.UUIDSet.fold (fun uuid acc ->
-      try Int.Set.add (Future.UUIDMap.find uuid f2t_map) acc
-      with Not_found -> acc)
-      except Int.Set.empty in
-  let is_done_or_todo i x = Future.is_val x || Int.Set.mem i except in
-  Array.iteri (fun i x ->
-    if not(is_done_or_todo i x) then CErrors.user_err ~hdr:"library"
-      Pp.(str"Proof object "++int i++str" is not checked nor to be checked"))
-    opaque_table;
   let sd = {
     md_name = dir;
     md_deps = Array.of_list (current_deps ());
diff --git a/library/library.mli b/library/library.mli
index f3186d847f..d2b0c4f202 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -34,9 +34,9 @@ val require_library_from_dirpath
 type seg_sum
 type seg_lib
 type seg_univ = (* cst, all_cst, finished? *)
-  Univ.ContextSet.t Future.computation array * Univ.ContextSet.t * bool
+  Univ.ContextSet.t option array * Univ.ContextSet.t * bool
 type seg_discharge = Opaqueproof.cooking_info list array
-type seg_proofs = Constr.constr Future.computation array
+type seg_proofs = Constr.constr option array
 
 (** Open a module (or a library); if the boolean is true then it's also
    an export otherwise just a simple import *)
-- 
cgit v1.2.3