Merge PR #10299: Lazy substitution of section contexts in opaque proofs

Reviewed-by: gares
Ack-by: maximedenes
Ack-by: ppedrot

2 files changed, 18 insertions, 21 deletions

diff --git a/library/library.ml b/library/library.ml
index e3b8511af1..1ac75d2fdc 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -276,11 +276,11 @@ let in_import_library : DirPath.t list * bool -> obj =
 (** Delayed / available tables of opaque terms *)
 
 type 'a table_status =
-  | ToFetch of 'a option array delayed
-  | Fetched of 'a option array
+  | ToFetch of 'a array delayed
+  | Fetched of 'a array
 
 let opaque_tables =
-  ref (LibraryMap.empty : (Constr.constr table_status) LibraryMap.t)
+  ref (LibraryMap.empty : ((Opaqueproof.cooking_info list * int * Constr.constr option) table_status) LibraryMap.t)
 
 let add_opaque_table dp st =
   opaque_tables := LibraryMap.add dp st !opaque_tables
@@ -306,10 +306,14 @@ let access_table what tables dp i =
 
 let access_opaque_table dp i =
   let what = "opaque proofs" in
-  access_table what opaque_tables dp i
+  let (info, n, c) = access_table what opaque_tables dp i in
+  match c with
+  | None -> None
+  | Some c -> Some (Cooking.cook_constr info n c)
 
 let indirect_accessor = {
   Opaqueproof.access_proof = access_opaque_table;
+  Opaqueproof.access_discharge = Cooking.cook_constr;
 }
 
 (************************************************************************)
@@ -319,8 +323,7 @@ type seg_sum = summary_disk
 type seg_lib = library_disk
 type seg_univ = (* true = vivo, false = vi *)
   Univ.ContextSet.t * bool
-type seg_discharge = Opaqueproof.cooking_info list array
-type seg_proofs = Constr.constr option array
+type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.t option) array
 
 let mk_library sd md digests univs =
   {
@@ -344,7 +347,6 @@ let intern_from_file f =
   let ((lmd : seg_lib delayed), digest_lmd) = in_delayed f ch in
   let (univs : seg_univ option), _, digest_u = System.marshal_in_segment f ch in
   let _ = System.skip_in_segment f ch in
-  let _ = System.skip_in_segment f ch in
   let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch in
   close_in ch;
   register_library_filename lsd.md_name f;
@@ -527,15 +529,13 @@ let load_library_todo f =
   let (s0 : seg_sum), _, _ = System.marshal_in_segment f ch in
   let (s1 : seg_lib), _, _ = System.marshal_in_segment f ch in
   let (s2 : seg_univ option), _, _ = System.marshal_in_segment f ch in
-  let (s3 : seg_discharge option), _, _ = System.marshal_in_segment f ch in
   let tasks, _, _ = System.marshal_in_segment f ch in
-  let (s5 : seg_proofs), _, _ = System.marshal_in_segment f ch in
+  let (s4 : seg_proofs), _, _ = System.marshal_in_segment f ch in
   close_in ch;
   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 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
+  s0, s1, Option.get s2, Option.get tasks, s4
 
 (************************************************************************)
 (*s [save_library dir] ends library [dir] and save it to the disk. *)
@@ -578,10 +578,10 @@ 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, disch_table, f2t_map = Opaqueproof.dump ~except otab in
-  let tasks, utab, dtab =
+  let opaque_table, f2t_map = Opaqueproof.dump ~except otab in
+  let tasks, utab =
     match todo with
-    | None -> None, None, None
+    | None -> None, None
     | Some (tasks, rcbackup) ->
         let tasks =
           List.map Stateid.(fun (r,b) ->
@@ -589,8 +589,8 @@ 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.ContextSet.empty,false),
-        Some disch_table in
+        Some (Univ.ContextSet.empty,false)
+  in
   let sd = {
     md_name = dir;
     md_deps = Array.of_list (current_deps ());
@@ -610,7 +610,6 @@ let save_library_to ?todo ~output_native_objects dir f otab =
     System.marshal_out_segment f' ch (sd           : seg_sum);
     System.marshal_out_segment f' ch (md           : seg_lib);
     System.marshal_out_segment f' ch (utab         : seg_univ option);
-    System.marshal_out_segment f' ch (dtab         : seg_discharge option);
     System.marshal_out_segment f' ch (tasks        : 'tasks option);
     System.marshal_out_segment f' ch (opaque_table : seg_proofs);
     close_out ch;
@@ -630,7 +629,6 @@ let save_library_raw f sum lib univs proofs =
   System.marshal_out_segment f ch (sum        : seg_sum);
   System.marshal_out_segment f ch (lib        : seg_lib);
   System.marshal_out_segment f ch (Some univs : seg_univ option);
-  System.marshal_out_segment f ch (None       : seg_discharge option);
   System.marshal_out_segment f ch (None       : 'tasks option);
   System.marshal_out_segment f ch (proofs     : seg_proofs);
   close_out ch
diff --git a/library/library.mli b/library/library.mli
index 142206e2c5..727eca10cf 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -35,8 +35,7 @@ type seg_sum
 type seg_lib
 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
+type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.t option) array
 
 (** Open a module (or a library); if the boolean is true then it's also
    an export otherwise just a simple import *)
@@ -51,7 +50,7 @@ val save_library_to :
 
 val load_library_todo
   :  CUnix.physical_path
-  -> seg_sum * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs
+  -> seg_sum * seg_lib * seg_univ * 'tasks * seg_proofs
 
 val save_library_raw : string -> seg_sum -> seg_lib -> seg_univ -> seg_proofs -> unit