From ab915f905ca81018521db63cdd0f3126b35c69c6 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 15 Oct 2017 19:21:00 +0200 Subject: [stm] First step to move interpretation of Undo commands out of the classifier. The vernacular classifier has a current special case for "Undo" like commands, as it needs access to the document structure in order to produce the proper "VtBack" classification, however the classifier is defined before the document is. We introduce a new delegation status `VtMeta` that allows us to interpreted such commands outside the classifier itself. --- API/API.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'API') diff --git a/API/API.mli b/API/API.mli index 879323a37d..e518cf583f 100644 --- a/API/API.mli +++ b/API/API.mli @@ -3714,6 +3714,7 @@ sig | VtProofMode of string | VtQuery of vernac_part_of_script * Feedback.route_id | VtBack of vernac_part_of_script * Stateid.t + | VtMeta | VtUnknown and vernac_qed_type = | VtKeep -- cgit v1.2.3 From d9704f80a4f4b565f77368dbf7c9650d301a233d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 16 Oct 2017 12:54:57 +0200 Subject: [stm] Remove VtBack from public classification. We interpret meta-commands directly, instead of going by an intermediate "classifier step". The code could still use some further refactoring, in particular, the `part_of_script` bit is a bit strange likely coming from some special treatment of `VtMeta` in the `query` call, and should go away. --- API/API.mli | 1 - 1 file changed, 1 deletion(-) (limited to 'API') diff --git a/API/API.mli b/API/API.mli index e518cf583f..535f6a29bb 100644 --- a/API/API.mli +++ b/API/API.mli @@ -3713,7 +3713,6 @@ sig | VtProofStep of proof_step | VtProofMode of string | VtQuery of vernac_part_of_script * Feedback.route_id - | VtBack of vernac_part_of_script * Stateid.t | VtMeta | VtUnknown and vernac_qed_type = -- cgit v1.2.3 From 19bbc3fd946555aa1fa1fc23d805a4eb3d13bc45 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 27 May 2017 23:22:04 +0200 Subject: [stm] Move interpretation state to Vernacentries We still don't thread the state there, but this is a start of the needed infrastructure. --- API/API.mli | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) (limited to 'API') diff --git a/API/API.mli b/API/API.mli index 535f6a29bb..d4f0872a39 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2060,6 +2060,8 @@ end module States : sig + type state + val with_state_protection_on_exception : ('a -> 'b) -> 'a -> 'b val with_state_protection : ('a -> 'b) -> 'a -> 'b end @@ -4512,6 +4514,9 @@ end module Proof_global : sig + + type state + type proof_mode = { name : string; set : unit -> unit ; @@ -5787,6 +5792,13 @@ end module Vernacentries : sig + + type interp_state = { (* TODO: inline records in OCaml 4.03 *) + system : States.state; (* summary + libstack *) + proof : Proof_global.state; (* proof state *) + shallow : bool (* is the state trimmed down (libstack) *) + } + val dump_global : Libnames.reference Misctypes.or_by_notation -> unit val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr -> Evd.evar_map * Redexpr.red_expr) Hook.t @@ -5814,11 +5826,11 @@ end module Stm : sig type doc - type state val get_doc : Feedback.doc_id -> doc + val state_of_id : doc:doc -> - Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ] + Stateid.t -> [ `Valid of Vernacentries.interp_state option | `Expired | `Error of exn ] end (************************************************************************) -- cgit v1.2.3 From 280be11cb4706e039cf4e9f68a5ae38b0aef9340 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 28 May 2017 00:35:57 +0200 Subject: [stm] Remove state-handling from Futures. We make Vernacentries.interp functional wrt state, and thus remove state-handling from `Future`. Now, a future needs a closure if it wants to preserve state. Consequently, `Vernacentries.interp` takes a state, and returns the new one. We don't explicitly thread the state in the STM yet, instead, we recover the state that was used before and pass it explicitly to `interp`. I have tested the commit with the files in interactive, but we aware that some new bugs may appear or old ones be made more apparent. However, I am confident that this step will improve our understanding of bugs. In some cases, we perform a bit more summary wrapping/unwrapping. This will go away in future commits; informal timings for a full make: - master: real 2m11,027s user 8m30,904s sys 1m0,000s - no_futures: real 2m8,474s user 8m34,380s sys 0m59,156s --- API/API.mli | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) (limited to 'API') diff --git a/API/API.mli b/API/API.mli index d4f0872a39..a41009fa2f 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1914,7 +1914,11 @@ module Summary : sig type frozen - type marshallable + + 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 *) type 'a summary_declaration = { freeze_function : marshallable -> 'a; @@ -2062,7 +2066,6 @@ module States : sig type state - val with_state_protection_on_exception : ('a -> 'b) -> 'a -> 'b val with_state_protection : ('a -> 'b) -> 'a -> 'b end @@ -5799,6 +5802,9 @@ sig shallow : bool (* is the state trimmed down (libstack) *) } + val freeze_interp_state : Summary.marshallable -> interp_state + val unfreeze_interp_state : interp_state -> unit + val dump_global : Libnames.reference Misctypes.or_by_notation -> unit val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr -> Evd.evar_map * Redexpr.red_expr) Hook.t -- cgit v1.2.3