aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/notation.ml4
-rw-r--r--kernel/conv_oracle.ml2
-rw-r--r--kernel/conv_oracle.mli2
-rw-r--r--library/declaremods.ml3
-rw-r--r--library/goptions.ml2
-rw-r--r--library/lib.ml7
-rw-r--r--library/lib.mli2
-rw-r--r--library/nametab.ml2
-rw-r--r--library/states.ml12
-rw-r--r--library/states.mli2
-rw-r--r--library/summary.ml20
-rw-r--r--library/summary.mli11
-rw-r--r--parsing/egramcoq.ml4
-rw-r--r--plugins/funind/invfun.ml2
-rw-r--r--pretyping/classops.ml2
-rw-r--r--tactics/auto.ml2
-rw-r--r--toplevel/coqtop.ml2
-rw-r--r--toplevel/metasyntax.ml2
-rw-r--r--toplevel/mltop.ml2
-rw-r--r--toplevel/vernac.ml2
20 files changed, 50 insertions, 37 deletions
diff --git a/interp/notation.ml b/interp/notation.ml
index 81ef06f6f..d0b4651ec 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -891,7 +891,7 @@ let find_notation_printing_rule ntn =
(**********************************************************************)
(* Synchronisation with reset *)
-let freeze () =
+let freeze _ =
(!scope_map, !notation_level_map, !scope_stack, !arguments_scope,
!delimiters_map, !notations_key_table, !printing_rules,
!scope_class_map)
@@ -925,7 +925,7 @@ let _ =
Summary.init_function = init }
let with_notation_protection f x =
- let fs = freeze () in
+ let fs = freeze false in
try let a = f x in unfreeze fs; a
with reraise ->
let reraise = Errors.push reraise in
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index 758bf821f..0a96821a3 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -29,7 +29,7 @@ let var_opacity = ref Id.Map.empty
let cst_opacity = ref Cmap.empty
(* summary operations *)
-let freeze () = (!var_opacity, !cst_opacity)
+let freeze _ = (!var_opacity, !cst_opacity)
let unfreeze (vo,co) = (cst_opacity := co; var_opacity := vo)
let get_strategy = function
diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli
index 4d8779664..822c3ea70 100644
--- a/kernel/conv_oracle.mli
+++ b/kernel/conv_oracle.mli
@@ -36,5 +36,5 @@ val get_transp_state : unit -> transparent_state
(****************************
Summary operations *)
type oracle
-val freeze : unit -> oracle
+val freeze : bool -> oracle
val unfreeze : oracle -> unit
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 5866d612e..894445de1 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -111,7 +111,6 @@ let openmod_info = Summary.ref default_module_info ~name:"MODULE-INFO-3"
substituted modules object during "reloading" of libraries *)
let library_cache = Summary.ref Dirmap.empty ~name:"MODULE-INFO-4"
-
(* auxiliary functions to transform full_path and kernel_name given
by Lib into module_path and DirPath.t needed for modules *)
@@ -887,7 +886,7 @@ let declare_include_ interp_struct me_asts =
of summaries *)
let protect_summaries f =
- let fs = Summary.freeze_summaries () in
+ let fs = Summary.freeze_summaries ~marshallable:false in
try f fs
with reraise ->
(* Something wrong: undo the whole process *)
diff --git a/library/goptions.ml b/library/goptions.ml
index bdc6ab89d..597c23b7d 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -240,7 +240,7 @@ let declare_option cast uncast
load_function = (fun _ (_,v) -> write v)}
in
let _ = Summary.declare_summary (nickname key)
- { Summary.freeze_function = read;
+ { Summary.freeze_function = (fun _ -> read ());
Summary.unfreeze_function = write;
Summary.init_function = (fun () -> write default) }
in
diff --git a/library/lib.ml b/library/lib.ml
index e33bf5b15..0ba9fd919 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -249,7 +249,8 @@ let add_anonymous_leaf obj =
add_entry oname (Leaf obj)
let add_frozen_state () =
- add_anonymous_entry (FrozenState (Summary.freeze_summaries()))
+ add_anonymous_entry
+ (FrozenState (Summary.freeze_summaries ~marshallable:false))
(* Modules. *)
@@ -487,7 +488,7 @@ let open_section id =
let name = make_path id, make_kn id (* this makes little sense however *) in
if Nametab.exists_section dir then
errorlabstrm "open_section" (pr_id id ++ str " already exists.");
- let fs = Summary.freeze_summaries() in
+ let fs = Summary.freeze_summaries ~marshallable:false in
add_entry name (OpenedSection (prefix, fs));
(*Pushed for the lifetime of the section: removed by unfrozing the summary*)
Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix);
@@ -608,7 +609,7 @@ let label_before_name (loc,id) =
type frozen = Names.DirPath.t option * library_segment
-let freeze () = (!comp_name, !lib_stk)
+let freeze ~marshallable:_ = (!comp_name, !lib_stk)
let unfreeze (mn,stk) =
comp_name := mn;
diff --git a/library/lib.mli b/library/lib.mli
index ce57721fb..8ab98f775 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -172,7 +172,7 @@ val label_before_name : Names.Id.t Loc.located -> int
type frozen
-val freeze : unit -> frozen
+val freeze : marshallable:bool -> frozen
val unfreeze : frozen -> unit
val init : unit -> unit
diff --git a/library/nametab.ml b/library/nametab.ml
index 1d43725f6..12cad7f55 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -543,7 +543,7 @@ let global_inductive r =
type frozen = ccitab * dirtab * mptab * kntab
* globrevtab * mprevtab * mptrevtab * knrevtab
-let freeze () : frozen =
+let freeze _ : frozen =
!the_ccitab,
!the_dirtab,
!the_modtypetab,
diff --git a/library/states.ml b/library/states.ml
index 8b8193981..1fd3fa2e5 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -10,8 +10,8 @@ open System
type state = Lib.frozen * Summary.frozen
-let freeze () =
- (Lib.freeze(), Summary.freeze_summaries())
+let freeze ~marshallable =
+ (Lib.freeze ~marshallable, Summary.freeze_summaries ~marshallable)
let unfreeze (fl,fs) =
Lib.unfreeze fl;
@@ -23,7 +23,7 @@ let (extern_state,intern_state) =
extern_intern Coq_config.state_magic_number in
(fun s ->
let s = ensure_suffix s in
- raw_extern s (freeze())),
+ raw_extern s (freeze ~marshallable:true)),
(fun s ->
let s = ensure_suffix s in
let paths = Loadpath.get_paths () in
@@ -33,7 +33,7 @@ let (extern_state,intern_state) =
(* Rollback. *)
let with_heavy_rollback f h x =
- let st = freeze () in
+ let st = freeze ~marshallable:false in
try
f x
with reraise ->
@@ -44,8 +44,10 @@ let without_rollback f h x =
with reraise -> raise (h reraise)
let with_state_protection f x =
- let st = freeze () in
+ let st = freeze ~marshallable:false in
try
let a = f x in unfreeze st; a
with reraise ->
(unfreeze st; raise reraise)
+
+
diff --git a/library/states.mli b/library/states.mli
index 26dec09e5..d186bf1c8 100644
--- a/library/states.mli
+++ b/library/states.mli
@@ -17,7 +17,7 @@ val intern_state : string -> unit
val extern_state : string -> unit
type state
-val freeze : unit -> state
+val freeze : marshallable:bool -> state
val unfreeze : state -> unit
(** {6 Rollback } *)
diff --git a/library/summary.ml b/library/summary.ml
index 056acd41c..53e9f7002 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -11,7 +11,7 @@ open Errors
open Util
type 'a summary_declaration = {
- freeze_function : unit -> 'a;
+ freeze_function : bool -> 'a;
unfreeze_function : 'a -> unit;
init_function : unit -> unit }
@@ -20,7 +20,7 @@ let summaries =
let internal_declare_summary sumname sdecl =
let (infun,outfun) = Dyn.create sumname in
- let dyn_freeze () = infun (sdecl.freeze_function())
+ let dyn_freeze b = infun (sdecl.freeze_function b)
and dyn_unfreeze sum = sdecl.unfreeze_function (outfun sum)
and dyn_init = sdecl.init_function in
let ddecl = {
@@ -43,10 +43,18 @@ let declare_summary sumname decl =
type frozen = Dyn.t String.Map.t
-let freeze_summaries () =
+let freeze_summaries ~marshallable =
let m = ref String.Map.empty in
Hashtbl.iter
- (fun id decl -> m := String.Map.add id (decl.freeze_function()) !m)
+ (fun id decl ->
+ (* to debug missing Lazy.force
+ if marshallable then begin
+ prerr_endline ("begin marshalling " ^ id);
+ ignore(Marshal.to_string (decl.freeze_function marshallable) []);
+ prerr_endline ("end marshalling " ^ id);
+ end;
+ /debug *)
+ m := String.Map.add id (decl.freeze_function marshallable) !m)
summaries;
!m
@@ -92,10 +100,10 @@ let unfreeze_summary datas =
(** All-in-one reference declaration + registration *)
-let ref ~name x =
+let ref ?(freeze=fun _ r -> r) ~name x =
let r = ref x in
declare_summary name
- { freeze_function = (fun () -> !r);
+ { freeze_function = (fun b -> freeze b !r);
unfreeze_function = ((:=) r);
init_function = (fun () -> r := x) };
r
diff --git a/library/summary.mli b/library/summary.mli
index 36e265ddf..698034ad6 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -10,7 +10,9 @@
in synchronization during the various backtracks of the system. *)
type 'a summary_declaration = {
- freeze_function : unit -> 'a;
+ (** freeze_function [true] is for marshalling to disk.
+ * e.g. lazy must be forced *)
+ freeze_function : bool -> 'a;
unfreeze_function : 'a -> unit;
init_function : unit -> unit }
@@ -30,9 +32,10 @@ val declare_summary : string -> 'a summary_declaration -> unit
(** All-in-one reference declaration + summary registration.
It behaves just as OCaml's standard [ref] function, except
that a [declare_summary] is done, with [name] as string.
- The [init_function] restores the reference to its initial value. *)
+ The [init_function] restores the reference to its initial value.
+ The [freeze_function] can be overridden *)
-val ref : name:string -> 'a -> 'a ref
+val ref : ?freeze:(bool -> 'a -> 'a) -> name:string -> 'a -> 'a ref
(** For global tables registered statically before the end of coqtop
launch, the following empty [init_function] could be used. *)
@@ -44,7 +47,7 @@ val nop : unit -> unit
type frozen
-val freeze_summaries : unit -> frozen
+val freeze_summaries : marshallable:bool -> frozen
val unfreeze_summaries : frozen -> unit
val init_summaries : unit -> unit
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index c10516839..9905a5ad4 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -306,7 +306,7 @@ let recover_notation_grammar ntn prec =
grammar rules. *)
type frozen_t = (int * all_grammar_command) list * Lexer.frozen_t
-let freeze () : frozen_t = (!grammar_state, Lexer.freeze ())
+let freeze _ : frozen_t = (!grammar_state, Lexer.freeze ())
(* We compare the current state of the grammar and the state to unfreeze,
by computing the longest common suffixes *)
@@ -337,7 +337,7 @@ let _ =
Summary.init_function = Summary.nop }
let with_grammar_rule_protection f x =
- let fs = freeze () in
+ let fs = freeze false in
try let a = f x in unfreeze fs; a
with reraise ->
let reraise = Errors.push reraise in
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index e46c1a15a..fd074386e 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1013,7 +1013,7 @@ let do_save () = Lemmas.save_named false
*)
let derive_correctness make_scheme functional_induction (funs: constant list) (graphs:inductive list) =
- let previous_state = States.freeze () in
+ let previous_state = States.freeze ~marshallable:false in
let funs = Array.of_list funs and graphs = Array.of_list graphs in
let funs_constr = Array.map mkConst funs in
try
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 907034d47..a9a65b8d1 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -102,7 +102,7 @@ let coercion_tab =
let inheritance_graph =
ref (Gmap.empty : (cl_index * cl_index, inheritance_path) Gmap.t)
-let freeze () = (!class_tab, !coercion_tab, !inheritance_graph)
+let freeze _ = (!class_tab, !coercion_tab, !inheritance_graph)
let unfreeze (fcl,fco,fig) =
class_tab:=fcl;
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 470d2e6cf..5aab5f252 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -463,7 +463,7 @@ let add_auto_init f =
auto_init := (fun () -> init (); f ())
let init () = searchtable := Hintdbmap.empty; !auto_init ()
-let freeze () = !searchtable
+let freeze _ = !searchtable
let unfreeze fs = searchtable := fs
let _ = Summary.declare_summary "search"
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 9ec843441..cb587a6ef 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -128,7 +128,7 @@ let compile_files () =
| [] -> ()
| [vf] -> compile_file vf (* One compilation : no need to save init state *)
| l ->
- let init_state = States.freeze() in
+ let init_state = States.freeze ~marshallable:false in
let coqdoc_init_state = Lexer.location_table () in
List.iter
(fun vf ->
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index e58b5f8e4..0c95201d2 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -1072,7 +1072,7 @@ let inNotation : notation_obj -> obj =
(**********************************************************************)
let with_lib_stk_protection f x =
- let fs = Lib.freeze () in
+ let fs = Lib.freeze false in
try let a = f x in Lib.unfreeze fs; a
with reraise ->
let reraise = Errors.push reraise in
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index 4ad1940cc..266397de8 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -319,7 +319,7 @@ let unfreeze_ml_modules x =
let _ =
Summary.declare_summary "ML-MODULES"
- { Summary.freeze_function = get_loaded_modules;
+ { Summary.freeze_function = (fun _ -> get_loaded_modules ());
Summary.unfreeze_function = unfreeze_ml_modules;
Summary.init_function = reset_loaded_modules }
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 84acc9bfa..14e4b8eb7 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -234,7 +234,7 @@ let set_formatter_translator() =
let pr_new_syntax loc ocom =
let loc = Loc.unloc loc in
if !beautify_file then set_formatter_translator();
- let fs = States.freeze () in
+ let fs = States.freeze ~marshallable:false in
let com = match ocom with
| Some VernacNop -> mt()
| Some com -> Ppvernac.pr_vernac com
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 22:08:55 +0000