aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh6
-rw-r--r--interp/notation.ml4
-rw-r--r--library/declaremods.ml2
-rw-r--r--library/global.ml7
-rw-r--r--library/goptions.ml2
-rw-r--r--library/lib.ml27
-rw-r--r--library/lib.mli5
-rw-r--r--library/states.ml8
-rw-r--r--library/states.mli4
-rw-r--r--library/summary.ml16
-rw-r--r--library/summary.mli13
-rw-r--r--parsing/pcoq.ml4
-rw-r--r--plugins/funind/indfun_common.ml2
-rw-r--r--proofs/proof_global.ml7
-rw-r--r--proofs/proof_global.mli2
-rw-r--r--stm/stm.ml139
-rw-r--r--vernac/metasyntax.ml2
-rw-r--r--vernac/mltop.ml2
-rw-r--r--vernac/vernacentries.ml2
-rw-r--r--vernac/vernacstate.ml11
-rw-r--r--vernac/vernacstate.mli4
21 files changed, 140 insertions, 129 deletions
diff --git a/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh b/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh
new file mode 100644
index 0000000000..efcdd2e97f
--- /dev/null
+++ b/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "9220" ] || [ "$CI_BRANCH" = "stm-shallow-logic" ]; then
+
+ paramcoq_CI_REF=stm-shallow-logic
+ paramcoq_CI_GITURL=https://github.com/maximedenes/paramcoq
+
+fi
diff --git a/interp/notation.ml b/interp/notation.ml
index c866929234..b0854de4a3 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1902,7 +1902,7 @@ let pr_visibility prglob = function
(**********************************************************************)
(* Synchronisation with reset *)
-let freeze _ =
+let freeze ~marshallable =
(!scope_map, !scope_stack, !uninterp_scope_stack, !arguments_scope,
!delimiters_map, !notations_key_table, !scope_class_map,
!prim_token_interp_infos, !prim_token_uninterp_infos,
@@ -1939,7 +1939,7 @@ let _ =
Summary.init_function = init }
let with_notation_protection f x =
- let fs = freeze false in
+ let fs = freeze ~marshallable:false in
try let a = f x in unfreeze fs; a
with reraise ->
let reraise = CErrors.push reraise in
diff --git a/library/declaremods.ml b/library/declaremods.ml
index d20775a0d7..8699583cdf 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -845,7 +845,7 @@ end
(** {6 Module operations handling summary freeze/unfreeze} *)
let protect_summaries f =
- let fs = Summary.freeze_summaries ~marshallable:`No in
+ let fs = Summary.freeze_summaries ~marshallable:false in
try f fs
with reraise ->
(* Something wrong: undo the whole process *)
diff --git a/library/global.ml b/library/global.ml
index 67b00cf411..84d2a37170 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -36,10 +36,9 @@ let is_joined_environment () =
let global_env_summary_tag =
Summary.declare_summary_tag global_env_summary_name
- { Summary.freeze_function = (function
- | `Yes -> join_safe_environment (); !global_env
- | `No -> !global_env
- | `Shallow -> !global_env);
+ { Summary.freeze_function = (fun ~marshallable -> if marshallable then
+ (join_safe_environment (); !global_env)
+ else !global_env);
unfreeze_function = (fun fr -> global_env := fr);
init_function = (fun () -> global_env := Safe_typing.empty_environment) }
diff --git a/library/goptions.ml b/library/goptions.ml
index 340d74151b..1b907fd966 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -235,7 +235,7 @@ let declare_option cast uncast append ?(preprocess = fun x -> x)
let default = read() in
let change =
let _ = Summary.declare_summary (nickname key)
- { Summary.freeze_function = (fun _ -> read ());
+ { Summary.freeze_function = (fun ~marshallable -> read ());
Summary.unfreeze_function = write;
Summary.init_function = (fun () -> write default) } in
let cache_options (_,(l,m,v)) =
diff --git a/library/lib.ml b/library/lib.ml
index cce5feeb4a..d4381a6923 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -571,7 +571,7 @@ let open_section id =
let prefix = Nametab.{ obj_dir; obj_mp = opp.obj_mp; obj_sec = add_dirpath_suffix opp.obj_sec id } in
if Nametab.exists_section obj_dir then
user_err ~hdr:"open_section" (Id.print id ++ str " already exists.");
- let fs = Summary.freeze_summaries ~marshallable:`No in
+ let fs = Summary.freeze_summaries ~marshallable:false in
add_entry (make_foname id) (OpenedSection (prefix, fs));
(*Pushed for the lifetime of the section: removed by unfrozing the summary*)
Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirOpenSection prefix));
@@ -608,24 +608,21 @@ let close_section () =
type frozen = lib_state
-let freeze ~marshallable =
- match marshallable with
- | `Shallow ->
- (* TASSI: we should do something more sensible here *)
- let lib_stk =
- CList.map_filter (function
+let freeze ~marshallable = !lib_state
+
+let unfreeze st = lib_state := st
+
+let drop_objects st =
+ let lib_stk =
+ CList.map_filter (function
| _, Leaf _ -> None
| n, (CompilingLibrary _ as x) -> Some (n,x)
| n, OpenedModule (it,e,op,_) ->
- Some(n,OpenedModule(it,e,op,Summary.empty_frozen))
+ Some(n,OpenedModule(it,e,op,Summary.empty_frozen))
| n, OpenedSection (op, _) ->
- Some(n,OpenedSection(op,Summary.empty_frozen)))
- !lib_state.lib_stk in
- { !lib_state with lib_stk }
- | _ ->
- !lib_state
-
-let unfreeze st = lib_state := st
+ Some(n,OpenedSection(op,Summary.empty_frozen)))
+ st.lib_stk in
+ { st with lib_stk }
let init () =
unfreeze initial_lib_state;
diff --git a/library/lib.mli b/library/lib.mli
index d1b4977dd5..30569197bc 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -148,9 +148,12 @@ val close_section : unit -> unit
type frozen
-val freeze : marshallable:Summary.marshallable -> frozen
+val freeze : marshallable:bool -> frozen
val unfreeze : frozen -> unit
+(** Keep only the libobject structure, not the objects themselves *)
+val drop_objects : frozen -> frozen
+
val init : unit -> unit
(** {6 Section management for discharge } *)
diff --git a/library/states.ml b/library/states.ml
index ae45b18b9c..92bdc410a3 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -13,8 +13,10 @@ open System
type state = Lib.frozen * Summary.frozen
+let lib_of_state = fst
let summary_of_state = snd
-let replace_summary (lib,_) s = lib, s
+let replace_summary (lib,_) st = lib, st
+let replace_lib (_,st) lib = lib, st
let freeze ~marshallable =
(Lib.freeze ~marshallable, Summary.freeze_summaries ~marshallable)
@@ -24,7 +26,7 @@ let unfreeze (fl,fs) =
Summary.unfreeze_summaries fs
let extern_state s =
- System.extern_state Coq_config.state_magic_number s (freeze ~marshallable:`Yes)
+ System.extern_state Coq_config.state_magic_number s (freeze ~marshallable:true)
let intern_state s =
unfreeze (with_magic_number_check (System.intern_state Coq_config.state_magic_number) s);
@@ -33,7 +35,7 @@ let intern_state s =
(* Rollback. *)
let with_state_protection f x =
- let st = freeze ~marshallable:`No in
+ let st = freeze ~marshallable:false in
try
let a = f x in unfreeze st; a
with reraise ->
diff --git a/library/states.mli b/library/states.mli
index 1e0361ea4f..52feb95222 100644
--- a/library/states.mli
+++ b/library/states.mli
@@ -19,11 +19,13 @@ val intern_state : string -> unit
val extern_state : string -> unit
type state
-val freeze : marshallable:Summary.marshallable -> state
+val freeze : marshallable:bool -> state
val unfreeze : state -> unit
val summary_of_state : state -> Summary.frozen
+val lib_of_state : state -> Lib.frozen
val replace_summary : state -> Summary.frozen -> state
+val replace_lib : state -> Lib.frozen -> state
(** {6 Rollback } *)
diff --git a/library/summary.ml b/library/summary.ml
index b68f1fb01b..8fbca44353 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -14,10 +14,8 @@ open Util
module Dyn = Dyn.Make ()
-type marshallable = [ `Yes | `No | `Shallow ]
-
type 'a summary_declaration = {
- freeze_function : marshallable -> 'a;
+ freeze_function : marshallable:bool -> 'a;
unfreeze_function : 'a -> unit;
init_function : unit -> unit }
@@ -31,7 +29,7 @@ let ml_modules = "ML-MODULES"
let internal_declare_summary fadd sumname sdecl =
let infun, outfun, tag = Dyn.Easy.make_dyn_tag (mangle sumname) in
- let dyn_freeze b = infun (sdecl.freeze_function b)
+ let dyn_freeze ~marshallable = infun (sdecl.freeze_function ~marshallable)
and dyn_unfreeze sum = sdecl.unfreeze_function (outfun sum)
and dyn_init = sdecl.init_function in
let ddecl = {
@@ -70,9 +68,9 @@ type frozen = {
let empty_frozen = { summaries = String.Map.empty; ml_module = None }
let freeze_summaries ~marshallable : frozen =
- let smap decl = decl.freeze_function marshallable in
+ let smap decl = decl.freeze_function ~marshallable in
{ summaries = String.Map.map smap !sum_map;
- ml_module = Option.map (fun decl -> decl.freeze_function marshallable) !sum_mod;
+ ml_module = Option.map (fun decl -> decl.freeze_function ~marshallable) !sum_mod;
}
let warn_summary_out_of_scope =
@@ -130,10 +128,10 @@ let remove_from_summary st tag =
(** All-in-one reference declaration + registration *)
-let ref_tag ?(freeze=fun _ r -> r) ~name x =
+let ref_tag ?(freeze=fun ~marshallable r -> r) ~name x =
let r = ref x in
let tag = declare_summary_tag name
- { freeze_function = (fun b -> freeze b !r);
+ { freeze_function = (fun ~marshallable -> freeze ~marshallable !r);
unfreeze_function = ((:=) r);
init_function = (fun () -> r := x) } in
r, tag
@@ -157,7 +155,7 @@ let (!) r =
let ref ?(freeze=fun x -> x) ~name init =
let r = Pervasives.ref (CEphemeron.create init, name) in
declare_summary name
- { freeze_function = (fun _ -> freeze !r);
+ { freeze_function = (fun ~marshallable -> freeze !r);
unfreeze_function = ((:=) r);
init_function = (fun () -> r := init) };
r
diff --git a/library/summary.mli b/library/summary.mli
index 64222761ba..0d77d725ac 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -11,15 +11,10 @@
(** This module registers the declaration of global tables, which will be kept
in synchronization during the various backtracks of the system. *)
-type marshallable =
- [ `Yes (* Full data will be marshalled to disk *)
- | `No (* Full data will be store in memory, e.g. for Undo *)
- | `Shallow ] (* Only part of the data will be marshalled to a slave process *)
-
(** Types of global Coq states. The ['a] type should be pure and marshallable by
the standard OCaml marshalling function. *)
type 'a summary_declaration = {
- freeze_function : marshallable -> 'a;
+ freeze_function : marshallable:bool -> 'a;
(** freeze_function [true] is for marshalling to disk.
* e.g. lazy must be forced *)
unfreeze_function : 'a -> unit;
@@ -50,8 +45,8 @@ val declare_summary_tag : string -> 'a summary_declaration -> 'a Dyn.tag
The [init_function] restores the reference to its initial value.
The [freeze_function] can be overridden *)
-val ref : ?freeze:(marshallable -> 'a -> 'a) -> name:string -> 'a -> 'a ref
-val ref_tag : ?freeze:(marshallable -> 'a -> 'a) -> name:string -> 'a -> 'a ref * 'a Dyn.tag
+val ref : ?freeze:(marshallable:bool -> 'a -> 'a) -> name:string -> 'a -> 'a ref
+val ref_tag : ?freeze:(marshallable:bool -> 'a -> 'a) -> name:string -> 'a -> 'a ref * 'a Dyn.tag
(* As [ref] but the value is local to a process, i.e. not sent to, say, proof
* workers. It is useful to implement a local cache for example. *)
@@ -81,7 +76,7 @@ val nop : unit -> unit
type frozen
val empty_frozen : frozen
-val freeze_summaries : marshallable:marshallable -> frozen
+val freeze_summaries : marshallable:bool -> frozen
val unfreeze_summaries : ?partial:bool -> frozen -> unit
val init_summaries : unit -> unit
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 923147ba2e..19ae97da77 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -553,7 +553,7 @@ type frozen_t =
(grammar_entry * GramState.t) list *
CLexer.keyword_state
-let freeze _ : frozen_t =
+let freeze ~marshallable : frozen_t =
(!grammar_stack, CLexer.get_keyword_state ())
(* We compare the current state of the grammar and the state to unfreeze,
@@ -586,7 +586,7 @@ let parser_summary_tag =
Summary.init_function = Summary.nop }
let with_grammar_rule_protection f x =
- let fs = freeze false in
+ let fs = freeze ~marshallable:false in
try let a = f x in unfreeze fs; a
with reraise ->
let reraise = CErrors.push reraise in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 5d0d17ee6b..f9938c0356 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -492,7 +492,7 @@ type tcc_lemma_value =
(* We only "purify" on exceptions. XXX: What is this doing here? *)
let funind_purify f x =
- let st = Vernacstate.freeze_interp_state `No in
+ let st = Vernacstate.freeze_interp_state ~marshallable:false in
try f x
with e ->
let e = CErrors.push e in
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 2027ad4e21..8077da8807 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -462,11 +462,8 @@ module V82 = struct
end
let freeze ~marshallable =
- match marshallable with
- | `Yes ->
- CErrors.anomaly (Pp.str"full marshalling of proof state not supported.")
- | `Shallow -> !pstates
- | `No -> !pstates
+ if marshallable then CErrors.anomaly (Pp.str"full marshalling of proof state not supported.")
+ else !pstates
let unfreeze s = pstates := s; update_proof_mode ()
let proof_of_state = function { proof }::_ -> proof | _ -> raise NoCurrentProof
let copy_terminators ~src ~tgt =
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index d9c32cf9d5..9e904c57aa 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -135,7 +135,7 @@ module V82 : sig
Decl_kinds.goal_kind)
end
-val freeze : marshallable:[`Yes | `No | `Shallow] -> t
+val freeze : marshallable:bool -> t
val unfreeze : t -> unit
val proof_of_state : t -> Proof.t
val copy_terminators : src:t -> tgt:t -> t
diff --git a/stm/stm.ml b/stm/stm.ml
index 77fb49625c..ffd13fcb73 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -78,7 +78,7 @@ let async_proofs_is_master opt =
(* Protect against state changes *)
let stm_purify f x =
- let st = Vernacstate.freeze_interp_state `No in
+ let st = Vernacstate.freeze_interp_state ~marshallable:false in
try
let res = f x in
Vernacstate.unfreeze_interp_state st;
@@ -343,7 +343,7 @@ module VCS : sig
val set_ldir : Names.DirPath.t -> unit
val get_ldir : unit -> Names.DirPath.t
- val is_interactive : unit -> [`Yes | `No | `Shallow]
+ val is_interactive : unit -> bool
val is_vio_doc : unit -> bool
val current_branch : unit -> Branch.t
@@ -543,8 +543,8 @@ end = struct (* {{{ *)
let is_interactive () =
match !doc_type with
- | Interactive _ -> `Yes
- | _ -> `No
+ | Interactive _ -> true
+ | _ -> false
let is_vio_doc () =
match !doc_type with
@@ -632,13 +632,20 @@ end = struct (* {{{ *)
" to "^Stateid.to_string block_stop^"."))
in aux block_stop
+ (* [slice] copies a slice of the DAG, keeping only the last known valid state.
+ When it copies a state, it drops the libobjects and keeps only the structure. *)
let slice ~block_start ~block_stop =
let l = nodes_in_slice ~block_start ~block_stop in
let copy_info v id =
Vcs_.set_info v id
{ (get_info id) with state = Empty; vcs_backup = None,None } in
+ let make_shallow = function
+ | Valid st -> Valid (Vernacstate.make_shallow st)
+ | x -> x
+ in
let copy_info_w_state v id =
- Vcs_.set_info v id { (get_info id) with vcs_backup = None,None } in
+ let info = get_info id in
+ Vcs_.set_info v id { info with state = make_shallow info.state; vcs_backup = None,None } in
let copy_proof_blockes v =
let nodes = Vcs_.Dag.all_nodes (Vcs_.dag v) in
let props =
@@ -776,14 +783,14 @@ module State : sig
val define :
doc:doc ->
?safe_id:Stateid.t ->
- ?redefine:bool -> ?cache:Summary.marshallable ->
+ ?redefine:bool -> ?cache:bool ->
?feedback_processed:bool -> (unit -> unit) -> Stateid.t -> unit
val fix_exn_ref : (Exninfo.iexn -> Exninfo.iexn) ref
val install_cached : Stateid.t -> unit
- val is_cached : ?cache:Summary.marshallable -> Stateid.t -> bool
- val is_cached_and_valid : ?cache:Summary.marshallable -> Stateid.t -> bool
+ val is_cached : ?cache:bool -> Stateid.t -> bool
+ val is_cached_and_valid : ?cache:bool -> Stateid.t -> bool
val exn_on : Stateid.t -> valid:Stateid.t -> Exninfo.iexn -> Exninfo.iexn
@@ -832,16 +839,15 @@ end = struct (* {{{ *)
Summary.project_from_summary st Util.(pi2 summary_pstate),
Summary.project_from_summary st Util.(pi3 summary_pstate)
- let freeze marshallable id =
- VCS.set_state id (Valid (Vernacstate.freeze_interp_state marshallable))
+ let freeze ~marshallable id =
+ VCS.set_state id (Valid (Vernacstate.freeze_interp_state ~marshallable))
let freeze_invalid id iexn = VCS.set_state id (Error iexn)
- let is_cached ?(cache=`No) id only_valid =
+ let is_cached ?(cache=false) id only_valid =
if Stateid.equal id !cur_id then
try match VCS.get_info id with
- | { state = Empty } when cache = `Yes -> freeze `No id; true
- | { state = Empty } when cache = `Shallow -> freeze `Shallow id; true
+ | { state = Empty } when cache -> freeze ~marshallable:false id; true
| _ -> true
with VCS.Expired -> false
else
@@ -866,7 +872,7 @@ end = struct (* {{{ *)
| _ ->
(* coqc has a 1 slot cache and only for valid states *)
- if VCS.is_interactive () = `No && Stateid.equal id !cur_id then ()
+ if not (VCS.is_interactive ()) && Stateid.equal id !cur_id then ()
else anomaly Pp.(str "installing a non cached state.")
let get_cached id =
@@ -924,7 +930,7 @@ end = struct (* {{{ *)
let e2 = Summary.project_from_summary s2 Global.global_env_summary_tag in
e1 == e2
- let define ~doc ?safe_id ?(redefine=false) ?(cache=`No) ?(feedback_processed=true)
+ let define ~doc ?safe_id ?(redefine=false) ?(cache=false) ?(feedback_processed=true)
f id
=
feedback ~id:id (ProcessingIn !Flags.async_proofs_worker_id);
@@ -933,13 +939,12 @@ end = struct (* {{{ *)
anomaly Pp.(str"defining state "++str str_id++str" twice.");
try
stm_prerr_endline (fun () -> "defining "^str_id^" (cache="^
- if cache = `Yes then "Y)" else if cache = `Shallow then "S)" else "N)");
+ if cache then "Y)" else "N)");
let good_id = match safe_id with None -> !cur_id | Some id -> id in
fix_exn_ref := exn_on id ~valid:good_id;
f ();
fix_exn_ref := (fun x -> x);
- if cache = `Yes then freeze `No id
- else if cache = `Shallow then freeze `Shallow id;
+ if cache then freeze ~marshallable:false id;
stm_prerr_endline (fun () -> "setting cur id to "^str_id);
cur_id := id;
if feedback_processed then
@@ -958,14 +963,14 @@ end = struct (* {{{ *)
| None, Some good_id -> (exn_on id ~valid:good_id (e, info))
| Some _, None -> (e, info)
| Some (_,at), Some id -> (e, Stateid.add info ~valid:id at) in
- if cache = `Yes || cache = `Shallow then freeze_invalid id ie;
+ if cache then freeze_invalid id ie;
Hooks.(call unreachable_state ~doc id ie);
Exninfo.iraise ie
let init_state = ref None
let register_root_state () =
- init_state := Some (Vernacstate.freeze_interp_state `No)
+ init_state := Some (Vernacstate.freeze_interp_state ~marshallable:false)
let restore_root_state () =
cur_id := Stateid.dummy;
@@ -1178,7 +1183,7 @@ end = struct (* {{{ *)
| _ -> None
let undo_vernac_classifier v ~doc =
- if VCS.is_interactive () = `No && !cur_opt.async_proofs_cache <> Some Force
+ if not (VCS.is_interactive ()) && !cur_opt.async_proofs_cache <> Some Force
then undo_costly_in_batch_mode v;
try
match Vernacprop.under_control v with
@@ -1508,9 +1513,7 @@ end = struct (* {{{ *)
let build_proof_here ~doc ?loc ~drop_pt (id,valid) eop =
Future.create (State.exn_on id ~valid) (fun () ->
let wall_clock1 = Unix.gettimeofday () in
- if VCS.is_interactive () = `No
- then Reach.known_state ~doc ~cache:`No eop
- else Reach.known_state ~doc ~cache:`Shallow eop;
+ Reach.known_state ~doc ~cache:(VCS.is_interactive ()) eop;
let wall_clock2 = Unix.gettimeofday () in
Aux_file.record_in_aux_at ?loc "proof_build_time"
(Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
@@ -1532,7 +1535,7 @@ end = struct (* {{{ *)
* a bad fixpoint *)
let fix_exn = Future.fix_exn_of future_proof in
(* STATE: We use the current installed imperative state *)
- let st = Vernacstate.freeze_interp_state `No in
+ let st = Vernacstate.freeze_interp_state ~marshallable:false in
if not drop then begin
let checked_proof = Future.chain future_proof (fun p ->
let opaque = Proof_global.Opaque in
@@ -1545,7 +1548,7 @@ end = struct (* {{{ *)
let terminator = (* The one sent by master is an InvalidKey *)
Lemmas.(standard_proof_terminator []) in
- let st = Vernacstate.freeze_interp_state `No in
+ let st = Vernacstate.freeze_interp_state ~marshallable:false in
stm_vernac_interp stop
~proof:(pobject, terminator) st
{ verbose = false; loc; indentation = 0; strlen = 0;
@@ -1676,7 +1679,7 @@ end = struct (* {{{ *)
with VCS.Expired -> cur in
aux stop in
try
- Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:`No stop;
+ Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:false stop;
if drop then
let _proof = Proof_global.return_proof ~allow_partial:true () in
`OK_ADMITTED
@@ -1689,14 +1692,14 @@ end = struct (* {{{ *)
Proof_global.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in
(* We jump at the beginning since the kernel handles side effects by also
* looking at the ones that happen to be present in the current env *)
- Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:`No start;
+ Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:false start;
(* STATE SPEC:
* - start: First non-expired state! [This looks very fishy]
* - end : start + qed
* => takes nothing from the itermediate states.
*)
(* STATE We use the state resulting from reaching start. *)
- let st = Vernacstate.freeze_interp_state `No in
+ let st = Vernacstate.freeze_interp_state ~marshallable:false in
ignore(stm_vernac_interp stop ~proof st
{ verbose = false; loc; indentation = 0; strlen = 0;
expr = VernacExpr ([], VernacEndProof (Proved (opaque,None))) });
@@ -1934,7 +1937,7 @@ end = struct (* {{{ *)
let perform { r_state = id; r_state_fb; r_document = vcs; r_ast; r_goal } =
Option.iter VCS.restore vcs;
try
- Reach.known_state ~doc:dummy_doc (* XXX should be vcs *) ~cache:`No id;
+ Reach.known_state ~doc:dummy_doc (* XXX should be vcs *) ~cache:false id;
stm_purify (fun () ->
let Proof.{sigma=sigma0} = Proof.data (Proof_global.give_me_the_proof ()) in
let g = Evd.find sigma0 r_goal in
@@ -1955,7 +1958,7 @@ end = struct (* {{{ *)
* => captures state id in a future closure, which will
discard execution state but for the proof + univs.
*)
- let st = Vernacstate.freeze_interp_state `No in
+ let st = Vernacstate.freeze_interp_state ~marshallable:false in
ignore(stm_vernac_interp r_state_fb st ast);
let Proof.{sigma} = Proof.data (Proof_global.give_me_the_proof ()) in
match Evd.(evar_body (find sigma r_goal)) with
@@ -1994,7 +1997,7 @@ end = struct (* {{{ *)
| VernacFail e -> find ~time ~batch ~fail:true e
| e -> e, time, batch, fail in
find ~time:false ~batch:false ~fail:false e in
- let st = Vernacstate.freeze_interp_state `No in
+ let st = Vernacstate.freeze_interp_state ~marshallable:false in
Vernacentries.with_fail st fail (fun () ->
(if time then System.with_time ~batch else (fun x -> x)) (fun () ->
ignore(TaskQueue.with_n_workers nworkers (fun queue ->
@@ -2089,9 +2092,9 @@ end = struct (* {{{ *)
let perform { r_where; r_doc; r_what; r_for } =
VCS.restore r_doc;
VCS.print ();
- Reach.known_state ~doc:dummy_doc (* XXX should be r_doc *) ~cache:`No r_where;
+ Reach.known_state ~doc:dummy_doc (* XXX should be r_doc *) ~cache:false r_where;
(* STATE *)
- let st = Vernacstate.freeze_interp_state `No in
+ let st = Vernacstate.freeze_interp_state ~marshallable:false in
try
(* STATE SPEC:
* - start: r_where
@@ -2133,14 +2136,14 @@ end (* }}} *)
and Reach : sig
val known_state :
- doc:doc -> ?redefine_qed:bool -> cache:Summary.marshallable ->
+ doc:doc -> ?redefine_qed:bool -> cache:bool ->
Stateid.t -> unit
end = struct (* {{{ *)
let async_policy () =
- if Attributes.is_universe_polymorphism () then false
- else if VCS.is_interactive () = `Yes then
+ if Attributes.is_universe_polymorphism () then false (* FIXME this makes no sense, it is the default value of the attribute *)
+ else if VCS.is_interactive () then
(async_proofs_is_master !cur_opt || !cur_opt.async_proofs_mode = APonLazy)
else
(VCS.is_vio_doc () || !cur_opt.async_proofs_mode <> APoff)
@@ -2322,7 +2325,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
* - end : maybe after recovery command.
*)
(* STATE: We use an updated state with proof *)
- let st = Vernacstate.freeze_interp_state `No in
+ let st = Vernacstate.freeze_interp_state ~marshallable:false in
Option.iter (fun expr -> ignore(stm_vernac_interp id st {
verbose = true; loc = None; expr; indentation = 0;
strlen = 0 } ))
@@ -2358,11 +2361,11 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
(* ugly functions to process nested lemmas, i.e. hard to reproduce
* side effects *)
let cherry_pick_non_pstate () =
- let st = Summary.freeze_summaries ~marshallable:`No in
+ let st = Summary.freeze_summaries ~marshallable:false in
let st = Summary.remove_from_summary st Util.(pi1 summary_pstate) in
let st = Summary.remove_from_summary st Util.(pi2 summary_pstate) in
let st = Summary.remove_from_summary st Util.(pi3 summary_pstate) in
- st, Lib.freeze ~marshallable:`No in
+ st, Lib.freeze ~marshallable:false in
let inject_non_pstate (s,l) =
Summary.unfreeze_summaries ~partial:true s; Lib.unfreeze l; update_global_env ()
@@ -2393,7 +2396,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
| `Cmd { cast = x; cqueue = `TacQueue (solve,abstract,cancel_switch); cblock } ->
(fun () ->
resilient_tactic id cblock (fun () ->
- reach ~cache:`Shallow view.next;
+ reach ~cache:true view.next;
Partac.vernac_interp ~solve ~abstract ~cancel_switch
!cur_opt.async_proofs_n_tacworkers view.next id x)
), cache, true
@@ -2406,39 +2409,39 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
resilient_tactic id cblock (fun () ->
reach view.next;
(* State resulting from reach *)
- let st = Vernacstate.freeze_interp_state `No in
+ let st = Vernacstate.freeze_interp_state ~marshallable:false in
ignore(stm_vernac_interp id st x)
);
if eff then update_global_env ()
- ), (if eff then `Yes else cache), true
+ ), eff || cache, true
| `Cmd { cast = x; ceff = eff } -> (fun () ->
(match !cur_opt.async_proofs_mode with
| APon | APonLazy ->
resilient_command reach view.next
| APoff -> reach view.next);
- let st = Vernacstate.freeze_interp_state `No in
+ let st = Vernacstate.freeze_interp_state ~marshallable:false in
ignore(stm_vernac_interp id st x);
if eff then update_global_env ()
- ), (if eff then `Yes else cache), true
+ ), eff || cache, true
| `Fork ((x,_,_,_), None) -> (fun () ->
resilient_command reach view.next;
- let st = Vernacstate.freeze_interp_state `No in
+ let st = Vernacstate.freeze_interp_state ~marshallable:false in
ignore(stm_vernac_interp id st x);
wall_clock_last_fork := Unix.gettimeofday ()
- ), `Yes, true
+ ), true, true
| `Fork ((x,_,_,_), Some prev) -> (fun () -> (* nested proof *)
- reach ~cache:`Shallow prev;
+ reach ~cache:true prev;
reach view.next;
(try
- let st = Vernacstate.freeze_interp_state `No in
+ let st = Vernacstate.freeze_interp_state ~marshallable:false in
ignore(stm_vernac_interp id st x);
with e when CErrors.noncritical e ->
let (e, info) = CErrors.push e in
let info = Stateid.add info ~valid:prev id in
Exninfo.iraise (e, info));
wall_clock_last_fork := Unix.gettimeofday ()
- ), `Yes, true
+ ), true, true
| `Qed ({ qast = x; keep; brinfo; brname } as qed, eop) ->
let rec aux = function
| `ASync (block_start, nodes, name, delegate) -> (fun () ->
@@ -2468,7 +2471,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
State.install_cached id
| { VCS.kind = `Proof _ }, Some _ -> assert false
| { VCS.kind = `Proof _ }, None ->
- reach ~cache:`Shallow block_start;
+ reach ~cache:true block_start;
let fp, cancel =
if delegate then
Slaves.build_proof ~doc
@@ -2487,19 +2490,19 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
Proof_global.close_future_proof ~opaque ~feedback_id:id fp in
if not delegate then ignore(Future.compute fp);
reach view.next;
- let st = Vernacstate.freeze_interp_state `No in
+ let st = Vernacstate.freeze_interp_state ~marshallable:false in
ignore(stm_vernac_interp id ~proof st x);
feedback ~id:id Incomplete
| { VCS.kind = `Master }, _ -> assert false
end;
Proof_global.discard_all ()
- ), (if redefine_qed then `No else `Yes), true
+ ), not redefine_qed, true
| `Sync (name, `Immediate) -> (fun () ->
reach eop;
- let st = Vernacstate.freeze_interp_state `No in
+ let st = Vernacstate.freeze_interp_state ~marshallable:false in
ignore(stm_vernac_interp id st x);
Proof_global.discard_all ()
- ), `Yes, true
+ ), true, true
| `Sync (name, reason) -> (fun () ->
log_processing_sync id name reason;
reach eop;
@@ -2523,25 +2526,25 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
if keep <> VtKeep VtKeepAxiom then
reach view.next;
let wall_clock2 = Unix.gettimeofday () in
- let st = Vernacstate.freeze_interp_state `No in
+ let st = Vernacstate.freeze_interp_state ~marshallable:false in
ignore(stm_vernac_interp id ?proof st x);
let wall_clock3 = Unix.gettimeofday () in
Aux_file.record_in_aux_at ?loc:x.loc "proof_check_time"
(Printf.sprintf "%.3f" (wall_clock3 -. wall_clock2));
Proof_global.discard_all ()
- ), `Yes, true
+ ), true, true
| `MaybeASync (start, nodes, name, delegate) -> (fun () ->
- reach ~cache:`Shallow start;
+ reach ~cache:true start;
(* no sections *)
if CList.is_empty (Environ.named_context (Global.env ()))
then Util.pi1 (aux (`ASync (start, nodes, name, delegate))) ()
else Util.pi1 (aux (`Sync (name, `NoPU_NoHint_NoES))) ()
- ), (if redefine_qed then `No else `Yes), true
+ ), not redefine_qed, true
in
aux (collect_proof keep (view.next, x) brname brinfo eop)
| `Sideff (ReplayCommand x,_) -> (fun () ->
reach view.next;
- let st = Vernacstate.freeze_interp_state `No in
+ let st = Vernacstate.freeze_interp_state ~marshallable:false in
ignore(stm_vernac_interp id st x);
update_global_env ()
), cache, true
@@ -2551,8 +2554,8 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
), cache, true
in
let cache_step =
- if !cur_opt.async_proofs_cache = Some Force then `Yes
- else cache_step in
+ !cur_opt.async_proofs_cache = Some Force || cache_step
+ in
State.define ~doc ?safe_id
~cache:cache_step ~redefine:redefine_qed ~feedback_processed step id;
stm_prerr_endline (fun () -> "reached: "^ Stateid.to_string id) in
@@ -2671,7 +2674,7 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } =
load_objs require_libs;
(* We record the state at this point! *)
- State.define ~doc ~cache:`Yes ~redefine:true (fun () -> ()) Stateid.initial;
+ State.define ~doc ~cache:true ~redefine:true (fun () -> ()) Stateid.initial;
Backtrack.record ();
Slaves.init ();
if async_proofs_is_master !cur_opt then begin
@@ -2785,7 +2788,7 @@ let merge_proof_branch ~valid ?id qast keep brname =
VCS.rewrite_merge qed_id ~ours:(Qed (qed ofp)) ~at:master_id brname;
VCS.delete_branch brname;
VCS.gc ();
- let _st : unit = Reach.known_state ~doc:dummy_doc (* XXX should be taken in input *) ~redefine_qed:true ~cache:`No qed_id in
+ let _st : unit = Reach.known_state ~doc:dummy_doc (* XXX should be taken in input *) ~redefine_qed:true ~cache:false qed_id in
VCS.checkout VCS.Branch.master;
`Unfocus qed_id
| { VCS.kind = `Master } ->
@@ -2957,12 +2960,12 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in
let id = VCS.new_node ~id:newtip () in
let head_id = VCS.get_branch_pos head in
- let _st : unit = Reach.known_state ~doc ~cache:`Yes head_id in (* ensure it is ok *)
+ let _st : unit = Reach.known_state ~doc ~cache:true head_id in (* ensure it is ok *)
let step () =
VCS.checkout VCS.Branch.master;
let mid = VCS.get_branch_pos VCS.Branch.master in
let _st' : unit = Reach.known_state ~doc ~cache:(VCS.is_interactive ()) mid in
- let st = Vernacstate.freeze_interp_state `No in
+ let st = Vernacstate.freeze_interp_state ~marshallable:false in
ignore(stm_vernac_interp id st x);
(* Vernac x may or may not start a proof *)
if not in_proof && Proof_global.there_are_pending_proofs () then
@@ -2987,7 +2990,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
end;
VCS.checkout_shallowest_proof_branch ();
end in
- State.define ~doc ~safe_id:head_id ~cache:`Yes step id;
+ State.define ~doc ~safe_id:head_id ~cache:true step id;
Backtrack.record (); `Ok
| VtUnknown, VtLater ->
@@ -3116,7 +3119,7 @@ type focus = {
let query ~doc ~at ~route s =
stm_purify (fun s ->
if Stateid.equal at Stateid.dummy then ignore(finish ~doc:dummy_doc)
- else Reach.known_state ~doc ~cache:`Yes at;
+ else Reach.known_state ~doc ~cache:true at;
try
while true do
let { CAst.loc; v=ast } = parse_sentence ~doc at s in
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 790b62c9d0..4e79b50b79 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1359,7 +1359,7 @@ let inNotation : notation_obj -> obj =
(**********************************************************************)
let with_lib_stk_protection f x =
- let fs = Lib.freeze ~marshallable:`No in
+ let fs = Lib.freeze ~marshallable:false in
try let a = f x in Lib.unfreeze fs; a
with reraise ->
let reraise = CErrors.push reraise in
diff --git a/vernac/mltop.ml b/vernac/mltop.ml
index 3620e177fe..8d6268753e 100644
--- a/vernac/mltop.ml
+++ b/vernac/mltop.ml
@@ -394,7 +394,7 @@ let unfreeze_ml_modules x =
let _ =
Summary.declare_ml_modules_summary
- { Summary.freeze_function = (fun _ -> get_loaded_modules ());
+ { Summary.freeze_function = (fun ~marshallable -> get_loaded_modules ());
Summary.unfreeze_function = unfreeze_ml_modules;
Summary.init_function = reset_loaded_modules }
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index ecfe39de09..e6e3db4beb 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2436,7 +2436,7 @@ let interp ?verbosely ?proof ~st cmd =
Vernacstate.unfreeze_interp_state st;
try
interp ?verbosely ?proof ~st cmd;
- Vernacstate.freeze_interp_state `No
+ Vernacstate.freeze_interp_state ~marshallable:false
with exn ->
let exn = CErrors.push exn in
Vernacstate.invalidate_cache ();
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index aa8bcdc328..b40bccf27e 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -33,11 +33,18 @@ let do_if_not_cached rf f v =
| Some _ ->
()
-let freeze_interp_state marshallable =
+let freeze_interp_state ~marshallable =
{ system = update_cache s_cache (States.freeze ~marshallable);
proof = update_cache s_proof (Proof_global.freeze ~marshallable);
- shallow = marshallable = `Shallow }
+ shallow = marshallable }
let unfreeze_interp_state { system; proof } =
do_if_not_cached s_cache States.unfreeze system;
do_if_not_cached s_proof Proof_global.unfreeze proof
+
+let make_shallow st =
+ let lib = States.lib_of_state st.system in
+ { st with
+ system = States.replace_lib st.system @@ Lib.drop_objects lib;
+ shallow = true;
+ }
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index b4d478d12d..ed20cb935a 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -14,8 +14,10 @@ type t = {
shallow : bool (* is the state trimmed down (libstack) *)
}
-val freeze_interp_state : Summary.marshallable -> t
+val freeze_interp_state : marshallable:bool -> t
val unfreeze_interp_state : t -> unit
+val make_shallow : t -> t
+
(* WARNING: Do not use, it will go away in future releases *)
val invalidate_cache : unit -> unit
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:01:50 +0000