Merge PR #10258: Remove the delayed universe table from object files.

Reviewed-by: SkySkimmer
Reviewed-by: gares

8 files changed, 23 insertions, 49 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 76f40dbac2..c5bc59e72a 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -50,6 +50,7 @@ let pr_path sp =
 
 type compilation_unit_name = DirPath.t
 
+type seg_univ = Univ.ContextSet.t * bool
 type seg_proofs = Constr.constr option array
 
 type library_t = {
@@ -90,7 +91,6 @@ let register_loaded_library m =
 
 (* Map from library names to table of opaque terms *)
 let opaque_tables = ref LibraryMap.empty
-let opaque_univ_tables = ref LibraryMap.empty
 
 let access_opaque_table dp i =
   let t =
@@ -326,7 +326,7 @@ let intern_from_file ~intern_mode (dir, f) =
       let ch = System.with_magic_number_check raw_intern_library f in
       let (sd:summary_disk), _, digest = marshal_in_segment f ch in
       let (md:library_disk), _, digest = marshal_in_segment f ch in
-      let (opaque_csts:'a option), _, udg = marshal_in_segment f ch in
+      let (opaque_csts:seg_univ option), _, udg = marshal_in_segment f ch in
       let (discharging:'a option), _, _ = marshal_in_segment f ch in
       let (tasks:'a option), _, _ = marshal_in_segment f ch in
       let (table:seg_proofs option), pos, checksum =
@@ -345,7 +345,7 @@ let intern_from_file ~intern_mode (dir, f) =
           (str "The file "++str f++str " contains unfinished tasks");
       if opaque_csts <> None then begin
        Flags.if_verbose chk_pp (str " (was a vio file) ");
-      Option.iter (fun (_,_,b) -> if not b then
+      Option.iter (fun (_,b) -> if not b then
         user_err ~hdr:"intern_from_file"
           (str "The file "++str f++str " is still a .vio"))
         opaque_csts;
@@ -363,13 +363,9 @@ let intern_from_file ~intern_mode (dir, f) =
     with e -> Flags.if_verbose chk_pp (str" failed!]" ++ fnl ()); raise e in
   depgraph := LibraryMap.add sd.md_name sd.md_deps !depgraph;
   Option.iter (fun table -> opaque_tables := LibraryMap.add sd.md_name table !opaque_tables) table;
-  Option.iter (fun (opaque_csts,_,_) ->
-    opaque_univ_tables :=
-      LibraryMap.add sd.md_name opaque_csts !opaque_univ_tables)
-    opaque_csts;
   let extra_cst =
     Option.default Univ.ContextSet.empty
-      (Option.map (fun (_,cs,_) -> cs) opaque_csts) in
+      (Option.map (fun (cs,_) -> cs) opaque_csts) in
   mk_library sd md f table digest extra_cst
 
 let get_deps (dir, f) =
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 1cf07e7cc7..1bc5891517 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -13,7 +13,6 @@ let set_indirect_accessor f = get_proof := f
 
 let indirect_accessor = {
   Opaqueproof.access_proof = (fun dp n -> !get_proof dp n);
-  Opaqueproof.access_constraints = (fun _ _ -> assert false);
 }
 
 let check_constant_declaration env kn cb =
diff --git a/checker/values.ml b/checker/values.ml
index adee9b8bde..031f05dd6b 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -385,4 +385,4 @@ let v_lib =
 
 let v_opaques = Array (Opt v_constr)
 let v_univopaques =
-  Opt (Tuple ("univopaques",[|Array (Opt v_context_set);v_context_set;v_bool|]))
+  Opt (Tuple ("univopaques",[|v_context_set;v_bool|]))
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 0ff27eb4ea..1971c67c61 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -18,7 +18,6 @@ type work_list = (Instance.t * Id.t array) Cmap.t *
 
 type indirect_accessor = {
   access_proof : DirPath.t -> int -> constr option;
-  access_constraints : DirPath.t -> int -> Univ.ContextSet.t option;
 }
 
 type cooking_info = { 
@@ -107,14 +106,12 @@ let force_proof access { opaque_val = prfs; opaque_dir = odp; _ } = function
       let c = Future.force pt in
       force_constr (List.fold_right subst_substituted l (from_val c))
 
-let force_constraints access { opaque_val = prfs; opaque_dir = odp; _ } = function
+let force_constraints _access { opaque_val = prfs; opaque_dir = odp; _ } = function
   | Direct (_,cu) -> snd(Future.force cu)
   | Indirect (_,dp,i) ->
       if DirPath.equal dp odp
       then snd (Future.force (snd (Int.Map.find i prfs)))
-      else match access.access_constraints dp i with
-        | None -> Univ.ContextSet.empty
-        | Some u -> u
+      else Univ.ContextSet.empty
 
 let get_direct_constraints = function
 | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
@@ -124,15 +121,13 @@ module FMap = Future.UUIDMap
 
 let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _ } =
   let opaque_table = Array.make n None in
-  let univ_table = Array.make n None in
   let disch_table = Array.make n [] in
   let f2t_map = ref FMap.empty in
   let iter n (d, cu) =
     let uid = Future.uuid cu in
     let () = f2t_map := FMap.add (Future.uuid cu) n !f2t_map in
     if Future.is_val cu then
-      let (c, u) = Future.force cu in
-      let () = univ_table.(n) <- Some u in
+      let (c, _) = Future.force cu in
       opaque_table.(n) <- Some c
     else if Future.UUIDSet.mem uid except then
       disch_table.(n) <- d
@@ -141,4 +136,4 @@ let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _
         Pp.(str"Proof object "++int n++str" is not checked nor to be checked")
   in
   let () = Int.Map.iter iter otab in
-  opaque_table, univ_table, disch_table, !f2t_map
+  opaque_table, disch_table, !f2t_map
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 4646206e55..46b0500507 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -37,7 +37,6 @@ val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab
 
 type indirect_accessor = {
   access_proof : DirPath.t -> int -> constr option;
-  access_constraints : DirPath.t -> int -> Univ.ContextSet.t option;
 }
 (** When stored indirectly, opaque terms are indexed by their library
     dirpath and an integer index. The two functions above activate
@@ -70,6 +69,5 @@ val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit
 
 val dump : ?except:Future.UUIDSet.t -> opaquetab ->
   Constr.t option array *
-  Univ.ContextSet.t option array *
   cooking_info list array *
   int Future.UUIDMap.t
diff --git a/library/library.ml b/library/library.ml
index 039124635e..e3b8511af1 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -281,13 +281,9 @@ type 'a table_status =
 
 let opaque_tables =
   ref (LibraryMap.empty : (Constr.constr table_status) LibraryMap.t)
-let univ_tables =
-  ref (LibraryMap.empty : (Univ.ContextSet.t table_status) LibraryMap.t)
 
 let add_opaque_table dp st =
   opaque_tables := LibraryMap.add dp st !opaque_tables
-let add_univ_table dp st =
-  univ_tables := LibraryMap.add dp st !univ_tables
 
 let access_table what tables dp i =
   let t = match LibraryMap.find dp !tables with
@@ -312,15 +308,8 @@ let access_opaque_table dp i =
   let what = "opaque proofs" in
   access_table what opaque_tables dp i
 
-let access_univ_table dp i =
-  try
-    let what = "universe contexts of opaque proofs" in
-    access_table what univ_tables dp i
-  with Not_found -> None
-
 let indirect_accessor = {
   Opaqueproof.access_proof = access_opaque_table;
-  Opaqueproof.access_constraints = access_univ_table;
 }
 
 (************************************************************************)
@@ -329,7 +318,7 @@ let indirect_accessor = {
 type seg_sum = summary_disk
 type seg_lib = library_disk
 type seg_univ = (* true = vivo, false = vi *)
-  Univ.ContextSet.t option array * Univ.ContextSet.t * bool
+  Univ.ContextSet.t * bool
 type seg_discharge = Opaqueproof.cooking_info list array
 type seg_proofs = Constr.constr option array
 
@@ -363,11 +352,9 @@ let intern_from_file f =
   let open Safe_typing in
   match univs with
   | None -> mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty
-  | Some (utab,uall,true) ->
-      add_univ_table lsd.md_name (Fetched utab);
+  | Some (uall,true) ->
       mk_library lsd lmd (Dvivo (digest_lmd,digest_u)) uall
-  | Some (utab,_,false) ->
-      add_univ_table lsd.md_name (Fetched utab);
+  | Some (_,false) ->
       mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty
 
 module DPMap = Map.Make(DirPath)
@@ -547,7 +534,7 @@ let load_library_todo f =
   if tasks = None then user_err ~hdr:"restart" (str"not a .vio file");
   if s2 = None then user_err ~hdr:"restart" (str"not a .vio file");
   if s3 = None then user_err ~hdr:"restart" (str"not a .vio file");
-  if pi3 (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file");
+  if snd (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file");
   s0, s1, Option.get s2, Option.get s3, Option.get tasks, s5
 
 (************************************************************************)
@@ -591,7 +578,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 ~except otab in
+  let opaque_table, disch_table, f2t_map = Opaqueproof.dump ~except otab in
   let tasks, utab, dtab =
     match todo with
     | None -> None, None, None
@@ -602,7 +589,7 @@ let save_library_to ?todo ~output_native_objects dir f otab =
             with Not_found -> assert b; { r with uuid = -1 }, b)
           tasks in
         Some (tasks,rcbackup),
-        Some (univ_table,Univ.ContextSet.empty,false),
+        Some (Univ.ContextSet.empty,false),
         Some disch_table in
   let sd = {
     md_name = dir;
diff --git a/library/library.mli b/library/library.mli
index 2c0673c3b1..142206e2c5 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -33,8 +33,8 @@ val require_library_from_dirpath
 (** Segments of a library *)
 type seg_sum
 type seg_lib
-type seg_univ = (* cst, all_cst, finished? *)
-  Univ.ContextSet.t option array * Univ.ContextSet.t * bool
+type seg_univ = (* all_cst, finished? *)
+  Univ.ContextSet.t * bool
 type seg_discharge = Opaqueproof.cooking_info list array
 type seg_proofs = Constr.constr option array
 
diff --git a/stm/stm.ml b/stm/stm.ml
index e32b6c9f1c..21f5ece244 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1819,15 +1819,15 @@ end = struct (* {{{ *)
                       str (Printexc.to_string e)));
       if drop then `ERROR_ADMITTED else `ERROR
 
-  let finish_task name (u,cst,_) d p l i =
+  let finish_task name (cst,_) d p l i =
     let { Stateid.uuid = bucket }, drop = List.nth l i in
     let bucket_name =
       if bucket < 0 then (assert drop; ", no bucket")
       else Printf.sprintf ", bucket %d" bucket in
     match check_task_aux bucket_name name l i with
     | `ERROR -> exit 1
-    | `ERROR_ADMITTED -> u, cst, false
-    | `OK_ADMITTED -> u, cst, false
+    | `ERROR_ADMITTED -> cst, false
+    | `OK_ADMITTED -> cst, false
     | `OK (po,_) ->
         let discharge c = List.fold_right Cooking.cook_constr d.(bucket) c in
         let con =
@@ -1846,9 +1846,8 @@ end = struct (* {{{ *)
         let pr = map (Option.get (Global.body_of_constant_body Library.indirect_accessor c)) in
         let pr = discharge pr in
         let pr = Constr.hcons pr in
-        u.(bucket) <- Some uc;
         p.(bucket) <- Some pr;
-        u, Univ.ContextSet.union cst uc, false
+        Univ.ContextSet.union cst uc, false
 
   let check_task name l i =
     match check_task_aux "" name l i with
@@ -2851,8 +2850,8 @@ let finish_tasks name u d p (t,rcbackup as tasks) =
     VCS.restore vcs;
     u in
   try
-    let u, a, _ = List.fold_left finish_task u (info_tasks tasks) in
-    (u,a,true), p
+    let a, _ = List.fold_left finish_task u (info_tasks tasks) in
+    (a,true), p
   with e ->
     let e = CErrors.push e in
     msg_warning (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e);