From e7ffa1bfa25300a25c1e81583b77d2d7587bbb5d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 31 May 2019 14:27:36 +0200
Subject: Do not substitute opaque constants when discharging.

Instead we do that on a by-need basis by reusing the section info already
stored in the opaque proof.
---
 library/library.ml  | 10 +++++++---
 library/library.mli |  2 +-
 2 files changed, 8 insertions(+), 4 deletions(-)

(limited to 'library')

diff --git a/library/library.ml b/library/library.ml
index e3b8511af1..0a57a85c35 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -280,7 +280,7 @@ type 'a table_status =
   | Fetched of 'a option array
 
 let opaque_tables =
-  ref (LibraryMap.empty : (Constr.constr table_status) LibraryMap.t)
+  ref (LibraryMap.empty : ((Opaqueproof.cooking_info list * int * Constr.constr) 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 ans = access_table what opaque_tables dp i in
+  match ans with
+  | None -> None
+  | Some (info, n, c) -> Some (Cooking.cook_constr info n c)
 
 let indirect_accessor = {
   Opaqueproof.access_proof = access_opaque_table;
+  Opaqueproof.access_discharge = Cooking.cook_constr;
 }
 
 (************************************************************************)
@@ -320,7 +324,7 @@ 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 =
   {
diff --git a/library/library.mli b/library/library.mli
index 142206e2c5..0c5d6e33c1 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -36,7 +36,7 @@ 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 *)
-- 
cgit v1.2.3


From 0f54a91eac98baf076d8be8f52bccdb1de17ea46 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 4 Jun 2019 10:19:02 +0200
Subject: Slightly tweak the representation of dischargeable opaque proofs.

This will allow an easier removal of the discharge segment in a later
commit.
---
 library/library.ml  | 14 +++++++-------
 library/library.mli |  2 +-
 2 files changed, 8 insertions(+), 8 deletions(-)

(limited to 'library')

diff --git a/library/library.ml b/library/library.ml
index 0a57a85c35..8030b835be 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 : ((Opaqueproof.cooking_info list * int * 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,10 @@ let access_table what tables dp i =
 
 let access_opaque_table dp i =
   let what = "opaque proofs" in
-  let ans = access_table what opaque_tables dp i in
-  match ans with
+  let (info, n, c) = access_table what opaque_tables dp i in
+  match c with
   | None -> None
-  | Some (info, n, c) -> Some (Cooking.cook_constr info n c)
+  | Some c -> Some (Cooking.cook_constr info n c)
 
 let indirect_accessor = {
   Opaqueproof.access_proof = access_opaque_table;
@@ -324,7 +324,7 @@ 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 = (Opaqueproof.cooking_info list * int * Constr.t) option array
+type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.t option) array
 
 let mk_library sd md digests univs =
   {
diff --git a/library/library.mli b/library/library.mli
index 0c5d6e33c1..284c66db5b 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -36,7 +36,7 @@ type seg_lib
 type seg_univ = (* all_cst, finished? *)
   Univ.ContextSet.t * bool
 type seg_discharge = Opaqueproof.cooking_info list array
-type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.t) 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 *)
-- 
cgit v1.2.3


From 1cdfb1f9270e399a784b346c3f8d6abbc4477552 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 4 Jun 2019 10:35:14 +0200
Subject: Remove the discharge segment from vo files.

Since the introduction of delayed section substitution, the opaque table
was already containing the same information.
---
 library/library.ml  | 20 +++++++-------------
 library/library.mli |  3 +--
 2 files changed, 8 insertions(+), 15 deletions(-)

(limited to 'library')

diff --git a/library/library.ml b/library/library.ml
index 8030b835be..1ac75d2fdc 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -323,7 +323,6 @@ 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 = (Opaqueproof.cooking_info list * int * Constr.t option) array
 
 let mk_library sd md digests univs =
@@ -348,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;
@@ -531,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. *)
@@ -582,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) ->
@@ -593,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 ());
@@ -614,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;
@@ -634,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 284c66db5b..727eca10cf 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -35,7 +35,6 @@ 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 = (Opaqueproof.cooking_info list * int * Constr.t option) array
 
 (** Open a module (or a library); if the boolean is true then it's also
@@ -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
 
-- 
cgit v1.2.3