aboutsummaryrefslogtreecommitdiff
path: root/stm
diff options
context:
space:
mode:
Diffstat (limited to 'stm')
-rw-r--r--stm/asyncTaskQueue.ml8
-rw-r--r--stm/asyncTaskQueue.mli4
-rw-r--r--stm/proofBlockDelimiter.ml24
-rw-r--r--stm/proofBlockDelimiter.mli2
-rw-r--r--stm/proofworkertop.ml4
-rw-r--r--stm/queryworkertop.ml4
-rw-r--r--stm/stm.ml606
-rw-r--r--stm/stm.mli87
-rw-r--r--stm/tacworkertop.ml4
-rw-r--r--stm/vernac_classifier.ml9
-rw-r--r--stm/vernac_classifier.mli3
-rw-r--r--stm/vio_checking.ml2
12 files changed, 466 insertions, 291 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 5d9b595d36..a356f32e9d 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -49,7 +49,7 @@ end
type expiration = bool ref
-module Make(T : Task) = struct
+module Make(T : Task) () = struct
exception Die
type response =
@@ -107,7 +107,7 @@ module Make(T : Task) = struct
let open Feedback in
feedback ~id:Stateid.initial (WorkerStatus(id, s))
- module Worker = Spawn.Sync(struct end)
+ module Worker = Spawn.Sync ()
module Model = struct
@@ -354,5 +354,5 @@ module Make(T : Task) = struct
end
-module MakeQueue(T : Task) = struct include Make(T) end
-module MakeWorker(T : Task) = struct include Make(T) end
+module MakeQueue(T : Task) () = struct include Make(T) () end
+module MakeWorker(T : Task) () = struct include Make(T) () end
diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli
index a80918e933..1044e668b6 100644
--- a/stm/asyncTaskQueue.mli
+++ b/stm/asyncTaskQueue.mli
@@ -41,7 +41,7 @@ end
type expiration = bool ref
-module MakeQueue(T : Task) : sig
+module MakeQueue(T : Task) () : sig
type queue
@@ -76,7 +76,7 @@ module MakeQueue(T : Task) : sig
end
-module MakeWorker(T : Task) : sig
+module MakeWorker(T : Task) () : sig
val main_loop : unit -> unit
val init_stdout : unit -> unit
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index a4b35ad60f..01b75e4964 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -11,7 +11,7 @@ open Stm
module Util : sig
val simple_goal : Evd.evar_map -> Goal.goal -> Goal.goal list -> bool
-val is_focused_goal_simple : Stateid.t -> [ `Simple of Goal.goal list | `Not ]
+val is_focused_goal_simple : doc:Stm.doc -> Stateid.t -> [ `Simple of Goal.goal list | `Not ]
type 'a until = [ `Stop | `Found of static_block_declaration | `Cont of 'a ]
@@ -43,10 +43,10 @@ let simple_goal sigma g gs =
Set.is_empty (evars_of_filtered_evar_info (nf_evar_info sigma evi)) &&
not (List.exists (Proofview.depends_on sigma g) gs)
-let is_focused_goal_simple id =
- match state_of_id id with
+let is_focused_goal_simple ~doc id =
+ match state_of_id ~doc id with
| `Expired | `Error _ | `Valid None -> `Not
- | `Valid (Some { proof }) ->
+ | `Valid (Some { Vernacentries.proof }) ->
let proof = Proof_global.proof_of_state proof in
let focused, r1, r2, r3, sigma = Proof.proof proof in
let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in
@@ -88,8 +88,8 @@ let static_bullet ({ entry_point; prev_node } as view) =
| _ -> `Stop) entry_point
| _ -> assert false
-let dynamic_bullet { dynamic_switch = id; carry_on_data = b } =
- match is_focused_goal_simple id with
+let dynamic_bullet doc { dynamic_switch = id; carry_on_data = b } =
+ match is_focused_goal_simple ~doc id with
| `Simple focused ->
`ValidBlock {
base_state = id;
@@ -116,8 +116,8 @@ let static_curly_brace ({ entry_point; prev_node } as view) =
`Cont (nesting + 1,node)
| _ -> `Cont (nesting,node)) (-1, entry_point)
-let dynamic_curly_brace { dynamic_switch = id } =
- match is_focused_goal_simple id with
+let dynamic_curly_brace doc { dynamic_switch = id } =
+ match is_focused_goal_simple ~doc id with
| `Simple focused ->
`ValidBlock {
base_state = id;
@@ -138,8 +138,8 @@ let static_par { entry_point; prev_node } =
Some { block_stop = entry_point.id; block_start = pid;
dynamic_switch = pid; carry_on_data = unit_val }
-let dynamic_par { dynamic_switch = id } =
- match is_focused_goal_simple id with
+let dynamic_par doc { dynamic_switch = id } =
+ match is_focused_goal_simple ~doc id with
| `Simple focused ->
`ValidBlock {
base_state = id;
@@ -167,9 +167,9 @@ let static_indent ({ entry_point; prev_node } as view) =
carry_on_data = of_vernac_expr_val entry_point.ast }
) last_tac
-let dynamic_indent { dynamic_switch = id; carry_on_data = e } =
+let dynamic_indent doc { dynamic_switch = id; carry_on_data = e } =
Printf.eprintf "%s\n" (Stateid.to_string id);
- match is_focused_goal_simple id with
+ match is_focused_goal_simple ~doc id with
| `Simple [] -> `Leaks
| `Simple focused ->
let but_last = List.tl (List.rev focused) in
diff --git a/stm/proofBlockDelimiter.mli b/stm/proofBlockDelimiter.mli
index e23a1d1c18..5cff0a8a72 100644
--- a/stm/proofBlockDelimiter.mli
+++ b/stm/proofBlockDelimiter.mli
@@ -21,7 +21,7 @@
type). `Simple carries the list of focused goals.
*)
val simple_goal : Evd.evar_map -> Goal.goal -> Goal.goal list -> bool
-val is_focused_goal_simple : Stateid.t -> [ `Simple of Goal.goal list | `Not ]
+val is_focused_goal_simple : doc:Stm.doc -> Stateid.t -> [ `Simple of Goal.goal list | `Not ]
type 'a until = [ `Stop | `Found of Stm.static_block_declaration | `Cont of 'a ]
diff --git a/stm/proofworkertop.ml b/stm/proofworkertop.ml
index 95012d984e..10b42f7e91 100644
--- a/stm/proofworkertop.ml
+++ b/stm/proofworkertop.ml
@@ -6,9 +6,9 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-module W = AsyncTaskQueue.MakeWorker(Stm.ProofTask)
+module W = AsyncTaskQueue.MakeWorker(Stm.ProofTask) ()
let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
-let () = Coqtop.toploop_run := W.main_loop
+let () = Coqtop.toploop_run := (fun _ -> W.main_loop ())
diff --git a/stm/queryworkertop.ml b/stm/queryworkertop.ml
index 85f0e6bfc1..a1fe50c63e 100644
--- a/stm/queryworkertop.ml
+++ b/stm/queryworkertop.ml
@@ -6,9 +6,9 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-module W = AsyncTaskQueue.MakeWorker(Stm.QueryTask)
+module W = AsyncTaskQueue.MakeWorker(Stm.QueryTask) ()
let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
-let () = Coqtop.toploop_run := W.main_loop
+let () = Coqtop.toploop_run := (fun _ -> W.main_loop ())
diff --git a/stm/stm.ml b/stm/stm.ml
index 984a874296..3cac3b6095 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -22,7 +22,18 @@ open Pp
open CErrors
open Feedback
open Vernacexpr
-open Vernac_classifier
+
+(* Protect against state changes *)
+let stm_purify f x =
+ let st = Vernacentries.freeze_interp_state `No in
+ try
+ let res = f x in
+ Vernacentries.unfreeze_interp_state st;
+ res
+ with e ->
+ let e = CErrors.push e in
+ Vernacentries.unfreeze_interp_state st;
+ Exninfo.iraise e
let execution_error ?loc state_id msg =
feedback ~id:state_id
@@ -40,8 +51,8 @@ let state_ready, state_ready_hook = Hook.make
let forward_feedback, forward_feedback_hook =
let m = Mutex.create () in
Hook.make ~default:(function
- | { id = id; route; contents } ->
- try Mutex.lock m; feedback ~id:id ~route contents; Mutex.unlock m
+ | { doc_id = did; span_id = id; route; contents } ->
+ try Mutex.lock m; feedback ~did ~id ~route contents; Mutex.unlock m
with e -> Mutex.unlock m; raise e) ()
let unreachable_state, unreachable_state_hook = Hook.make
@@ -64,11 +75,6 @@ let call_process_error_once =
end
-(* During interactive use we cache more states so that Undoing is fast *)
-let interactive () =
- if !Flags.ide_slave || not !Flags.batch_mode then `Yes
- else `No
-
let async_proofs_workers_extra_env = ref [||]
type aast = {
@@ -143,10 +149,12 @@ type step =
| `Qed of qed_t * Stateid.t
| `Sideff of seff_t * Stateid.t
| `Alias of alias_t ]
+
type visit = { step : step; next : Stateid.t }
let mkTransTac cast cblock cqueue =
Cmd { ctac = true; cast; cblock; cqueue; cids = []; ceff = false }
+
let mkTransCmd cast cids ceff cqueue =
Cmd { ctac = false; cast; cblock = None; cqueue; cids; ceff }
@@ -157,14 +165,11 @@ let summary_pstate = [ Evarutil.meta_counter_summary_name;
type cached_state =
| Empty
| Error of Exninfo.iexn
- | Valid of state
-and 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) *)
-}
+ | Valid of Vernacentries.interp_state
+
type branch = Vcs_.Branch.t * branch_type Vcs_.branch_info
type backup = { mine : branch; others : branch list }
+
type 'vcs state_info = { (* TODO: Make this record private to VCS *)
mutable n_reached : int; (* debug cache: how many times was computed *)
mutable n_goals : int; (* open goals: indentation *)
@@ -174,7 +179,7 @@ type 'vcs state_info = { (* TODO: Make this record private to VCS *)
let default_info () =
{ n_reached = 0; n_goals = 0; state = Empty; vcs_backup = None,None }
-module DynBlockData : Dyn.S = Dyn.Make(struct end)
+module DynBlockData : Dyn.S = Dyn.Make ()
(* Clusters of nodes implemented as Dag properties. While Dag and Vcs impose
* no constraint on properties, here we impose boxes to be non overlapping.
@@ -253,6 +258,16 @@ end (* }}} *)
(*************************** THE DOCUMENT *************************************)
(******************************************************************************)
+(* The main document type associated to a VCS *)
+type stm_doc_type =
+ | VoDoc of string
+ | VioDoc of string
+ | Interactive of Names.DirPath.t
+
+(* Dummy until we land the functional interp patch + fixed start_library *)
+type doc = int
+let dummy_doc : doc = 0
+
(* Imperative wrap around VCS to obtain _the_ VCS that is the
* representation of the document Coq is currently processing *)
module VCS : sig
@@ -269,7 +284,13 @@ module VCS : sig
type vcs = (branch_type, transaction, vcs state_info, box) Vcs_.t
- val init : id -> unit
+ val init : stm_doc_type -> id -> doc
+ (* val get_type : unit -> stm_doc_type *)
+ val set_ldir : Names.DirPath.t -> unit
+ val get_ldir : unit -> Names.DirPath.t
+
+ val is_interactive : unit -> [`Yes | `No | `Shallow]
+ val is_vio_doc : unit -> bool
val current_branch : unit -> Branch.t
val checkout : Branch.t -> unit
@@ -451,9 +472,30 @@ end = struct (* {{{ *)
type vcs = (branch_type, transaction, vcs state_info, box) t
let vcs : vcs ref = ref (empty Stateid.dummy)
- let init id =
+ let doc_type = ref (Interactive (Names.DirPath.make []))
+ let ldir = ref Names.DirPath.empty
+
+ let init dt id =
+ doc_type := dt;
vcs := empty id;
- vcs := set_info !vcs id (default_info ())
+ vcs := set_info !vcs id (default_info ());
+ dummy_doc
+
+ let set_ldir ld =
+ ldir := ld
+
+ let get_ldir () = !ldir
+ (* let get_type () = !doc_type *)
+
+ let is_interactive () =
+ match !doc_type with
+ | Interactive _ -> `Yes
+ | _ -> `No
+
+ let is_vio_doc () =
+ match !doc_type with
+ | VioDoc _ -> true
+ | _ -> false
let current_branch () = current_branch !vcs
@@ -663,7 +705,7 @@ end = struct (* {{{ *)
end (* }}} *)
-let state_of_id id =
+let state_of_id ~doc id =
try match (VCS.get_info id).state with
| Valid s -> `Valid (Some s)
| Error (e,_) -> `Error e
@@ -673,7 +715,7 @@ let state_of_id id =
(****** A cache: fills in the nodes of the VCS document with their value ******)
module State : sig
-
+
(** The function is from unit, so it uses the current state to define
a new one. I.e. one may been to install the right state before
defining a new one.
@@ -683,61 +725,59 @@ module State : sig
?safe_id:Stateid.t ->
?redefine:bool -> ?cache:Summary.marshallable ->
?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 exn_on : Stateid.t -> valid:Stateid.t -> Exninfo.iexn -> Exninfo.iexn
+
(* to send states across worker/master *)
- type frozen_state
- val get_cached : Stateid.t -> frozen_state
- val same_env : frozen_state -> frozen_state -> bool
+ val get_cached : Stateid.t -> Vernacentries.interp_state
+ val same_env : Vernacentries.interp_state -> Vernacentries.interp_state -> bool
type proof_part
+
type partial_state =
- [ `Full of frozen_state
- | `Proof of Stateid.t * proof_part ]
- val proof_part_of_frozen : frozen_state -> proof_part
+ [ `Full of Vernacentries.interp_state
+ | `ProofOnly of Stateid.t * proof_part ]
+
+ val proof_part_of_frozen : Vernacentries.interp_state -> proof_part
val assign : Stateid.t -> partial_state -> unit
+ (* Handlers for initial state, prior to document creation. *)
+ val register_root_state : unit -> unit
+ val restore_root_state : unit -> unit
+
(* Only for internal use to catch problems in parse_sentence, should
be removed in the state handling refactoring. *)
val cur_id : Stateid.t ref
+
end = struct (* {{{ *)
+ open Vernacentries
+
(* cur_id holds Stateid.dummy in case the last attempt to define a state
* failed, so the global state may contain garbage *)
let cur_id = ref Stateid.dummy
let fix_exn_ref = ref (fun x -> x)
- (* helpers *)
- let freeze_global_state marshallable =
- { system = States.freeze ~marshallable;
- proof = Proof_global.freeze ~marshallable;
- shallow = (marshallable = `Shallow) }
- let unfreeze_global_state { system; proof } =
- States.unfreeze system; Proof_global.unfreeze proof
-
- (* hack to make futures functional *)
- let () = Future.set_freeze
- (fun () -> Obj.magic (freeze_global_state `No, !cur_id))
- (fun t -> let s,i = Obj.magic t in unfreeze_global_state s; cur_id := i)
-
- type frozen_state = state
type proof_part =
Proof_global.state * Summary.frozen_bits (* only meta counters *)
+
type partial_state =
- [ `Full of frozen_state
- | `Proof of Stateid.t * proof_part ]
- let proof_part_of_frozen { proof; system } =
+ [ `Full of Vernacentries.interp_state
+ | `ProofOnly of Stateid.t * proof_part ]
+
+ let proof_part_of_frozen { Vernacentries.proof; system } =
proof,
Summary.project_summary (States.summary_of_state system) summary_pstate
let freeze marshallable id =
- VCS.set_state id (Valid (freeze_global_state marshallable))
+ VCS.set_state id (Valid (Vernacentries.freeze_interp_state marshallable))
+
let freeze_invalid id iexn = VCS.set_state id (Error iexn)
let is_cached ?(cache=`No) id only_valid =
@@ -760,12 +800,16 @@ end = struct (* {{{ *)
let install_cached id =
match VCS.get_info id with
| { state = Valid s } ->
- if Stateid.equal id !cur_id then () (* optimization *)
- else begin unfreeze_global_state s; cur_id := id end
- | { state = Error ie } -> cur_id := id; Exninfo.iraise ie
+ Vernacentries.unfreeze_interp_state s;
+ cur_id := id
+
+ | { state = Error ie } ->
+ cur_id := id;
+ Exninfo.iraise ie
+
| _ ->
(* coqc has a 1 slot cache and only for valid states *)
- if interactive () = `No && Stateid.equal id !cur_id then ()
+ if VCS.is_interactive () = `No && Stateid.equal id !cur_id then ()
else anomaly Pp.(str "installing a non cached state.")
let get_cached id =
@@ -782,13 +826,13 @@ end = struct (* {{{ *)
try
let prev = (VCS.visit id).next in
if is_cached_and_valid prev
- then { s with proof =
+ then { s with Vernacentries.proof =
Proof_global.copy_terminators
~src:(get_cached prev).proof ~tgt:s.proof }
else s
with VCS.Expired -> s in
VCS.set_state id (Valid s)
- | `Proof(ontop,(pstate,counters)) ->
+ | `ProofOnly(ontop,(pstate,counters)) ->
if is_cached_and_valid ontop then
let s = get_cached ontop in
let s = { s with proof =
@@ -855,6 +899,15 @@ end = struct (* {{{ *)
Hooks.(call unreachable_state id ie);
Exninfo.iraise ie
+ let init_state = ref None
+
+ let register_root_state () =
+ init_state := Some (Vernacentries.freeze_interp_state `No)
+
+ let restore_root_state () =
+ cur_id := Stateid.dummy;
+ Vernacentries.unfreeze_interp_state (Option.get !init_state);
+
end (* }}} *)
(* indentation code for Show Script, initially contributed
@@ -948,11 +1001,11 @@ end
(* Wrapper for Vernacentries.interp to set the feedback id *)
(* It is currently called 19 times, this number should be certainly
reduced... *)
-let stm_vernac_interp ?proof id ?route { verbose; loc; expr } =
+let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacentries.interp_state =
(* The Stm will gain the capability to interpret commmads affecting
the whole document state, such as backtrack, etc... so we start
to design the stm command interpreter now *)
- set_id_for_feedback ?route id;
+ set_id_for_feedback ?route dummy_doc id;
Aux_file.record_in_aux_set_at ?loc ();
(* We need to check if a command should be filtered from
* vernac_entries, as it cannot handle it. This should go away in
@@ -965,18 +1018,18 @@ let stm_vernac_interp ?proof id ?route { verbose; loc; expr } =
| VernacTime (_,e) | VernacTimeout (_,e) | VernacRedirect (_,(_,e)) -> is_filtered_command e
| _ -> false
in
- let aux_interp cmd =
+ let aux_interp st cmd =
if is_filtered_command cmd then
- stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr)
+ (stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st)
else match cmd with
- | VernacShow ShowScript -> ShowScript.show_script ()
+ | VernacShow ShowScript -> ShowScript.show_script (); st
| expr ->
stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr);
- try Vernacentries.interp ?verbosely:(Some verbose) ?proof (Loc.tag ?loc expr)
+ try Vernacentries.interp ?verbosely:(Some verbose) ?proof st (Loc.tag ?loc expr)
with e ->
let e = CErrors.push e in
Exninfo.iraise Hooks.(call_process_error_once e)
- in aux_interp expr
+ in aux_interp st expr
(****************************** CRUFT *****************************************)
(******************************************************************************)
@@ -990,8 +1043,8 @@ module Backtrack : sig
(* we could navigate the dag, but this ways easy *)
val branches_of : Stateid.t -> backup
- (* To be installed during initialization *)
- val undo_vernac_classifier : vernac_expr -> vernac_classification
+ (* Returns the state that the command should backtract to *)
+ val undo_vernac_classifier : vernac_expr -> Stateid.t * vernac_when
end = struct (* {{{ *)
@@ -1054,12 +1107,12 @@ end = struct (* {{{ *)
" the \"-async-proofs-cache force\" option to Coq."))
let undo_vernac_classifier v =
- if !Flags.batch_mode && !Flags.async_proofs_cache <> Some Flags.Force
+ if VCS.is_interactive () = `No && !Flags.async_proofs_cache <> Some Flags.Force
then undo_costly_in_batch_mode v;
try
match v with
| VernacResetInitial ->
- VtBack (true, Stateid.initial), VtNow
+ Stateid.initial, VtNow
| VernacResetName (_,name) ->
let id = VCS.get_branch_pos (VCS.current_branch ()) in
(try
@@ -1067,20 +1120,20 @@ end = struct (* {{{ *)
fold_until (fun b (id,_,label,_,_) ->
if b then `Stop id else `Cont (List.mem name label))
false id in
- VtBack (true, oid), VtNow
+ oid, VtNow
with Not_found ->
- VtBack (true, id), VtNow)
+ id, VtNow)
| VernacBack n ->
let id = VCS.get_branch_pos (VCS.current_branch ()) in
let oid = fold_until (fun n (id,_,_,_,_) ->
if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in
- VtBack (true, oid), VtNow
+ oid, VtNow
| VernacUndo n ->
let id = VCS.get_branch_pos (VCS.current_branch ()) in
let oid = fold_until (fun n (id,_,_,tactic,undo) ->
let value = (if tactic then 1 else 0) - undo in
if Int.equal n 0 then `Stop id else `Cont (n-value)) n id in
- VtBack (true, oid), VtLater
+ oid, VtLater
| VernacUndoTo _
| VernacRestart as e ->
let m = match e with VernacUndoTo m -> m | _ -> 0 in
@@ -1097,17 +1150,17 @@ end = struct (* {{{ *)
0 id in
let oid = fold_until (fun n (id,_,_,_,_) ->
if Int.equal n 0 then `Stop id else `Cont (n-1)) (n-m-1) id in
- VtBack (true, oid), VtLater
+ oid, VtLater
| VernacAbortAll ->
let id = VCS.get_branch_pos (VCS.current_branch ()) in
let oid = fold_until (fun () (id,vcs,_,_,_) ->
match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ())
() id in
- VtBack (true, oid), VtLater
+ oid, VtLater
| VernacBacktrack (id,_,_)
| VernacBackTo id ->
- VtBack (not !Flags.batch_mode, Stateid.of_int id), VtNow
- | _ -> VtUnknown, VtNow
+ Stateid.of_int id, VtNow
+ | _ -> anomaly Pp.(str "incorrect VtMeta classification")
with
| Not_found ->
CErrors.user_err ~hdr:"undo_vernac_classifier"
@@ -1118,18 +1171,15 @@ end (* }}} *)
let hints = ref Aux_file.empty_aux_file
let set_compilation_hints file =
hints := Aux_file.load_aux_file_for file
+
let get_hint_ctx loc =
let s = Aux_file.get ?loc !hints "context_used" in
- match Str.split (Str.regexp ";") s with
- | ids :: _ ->
- let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") ids) in
- let ids = List.map (fun id -> Loc.tag id) ids in
- begin match ids with
- | [] -> SsEmpty
- | x :: xs ->
- List.fold_left (fun a x -> SsUnion (SsSingl x,a)) (SsSingl x) xs
- end
- | _ -> raise Not_found
+ let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") s) in
+ let ids = List.map (fun id -> Loc.tag id) ids in
+ match ids with
+ | [] -> SsEmpty
+ | x :: xs ->
+ List.fold_left (fun a x -> SsUnion (SsSingl x,a)) (SsSingl x) xs
let get_hint_bp_time proof_name =
try float_of_string (Aux_file.get !hints proof_name)
@@ -1172,7 +1222,7 @@ type recovery_action = {
}
type dynamic_block_error_recovery =
- static_block_declaration -> [ `ValidBlock of recovery_action | `Leaks ]
+ doc -> static_block_declaration -> [ `ValidBlock of recovery_action | `Leaks ]
let proof_block_delimiters = ref []
@@ -1364,7 +1414,7 @@ end = struct (* {{{ *)
let build_proof_here ?loc ~drop_pt (id,valid) eop =
Future.create (State.exn_on id ~valid) (fun () ->
let wall_clock1 = Unix.gettimeofday () in
- if !Flags.batch_mode then Reach.known_state ~cache:`No eop
+ if VCS.is_interactive () = `No then Reach.known_state ~cache:`No eop
else Reach.known_state ~cache:`Shallow eop;
let wall_clock2 = Unix.gettimeofday () in
Aux_file.record_in_aux_at ?loc "proof_build_time"
@@ -1386,18 +1436,28 @@ end = struct (* {{{ *)
* the few errors tactics don't catch, like the "fix" tactic building
* a bad fixpoint *)
let fix_exn = Future.fix_exn_of future_proof in
+ (* STATE: We use the current installed imperative state *)
+ let st = Vernacentries.freeze_interp_state `No in
if not drop then begin
- let checked_proof = Future.chain ~pure:false future_proof (fun p ->
+ let checked_proof = Future.chain future_proof (fun p ->
+
+ (* Unfortunately close_future_proof and friends are not pure so we need
+ to set the state manually here *)
+ Vernacentries.unfreeze_interp_state st;
let pobject, _ =
Proof_global.close_future_proof ~feedback_id:stop (Future.from_val ~fix_exn p) in
let terminator = (* The one sent by master is an InvalidKey *)
Lemmas.(standard_proof_terminator [] (mk_hook (fun _ _ -> ()))) in
+
+ let st = Vernacentries.freeze_interp_state `No in
stm_vernac_interp stop
- ~proof:(pobject, terminator)
+ ~proof:(pobject, terminator) st
{ verbose = false; loc; indentation = 0; strlen = 0;
expr = (VernacEndProof (Proved (Opaque,None))) }) in
ignore(Future.join checked_proof);
end;
+ (* STATE: Restore the state XXX: handle exn *)
+ Vernacentries.unfreeze_interp_state st;
RespBuiltProof(proof,time)
with
| e when CErrors.noncritical e || e = Stack_overflow ->
@@ -1414,7 +1474,7 @@ end = struct (* {{{ *)
let perform_states query =
if query = [] then [] else
- let is_tac e = match classify_vernac e with
+ let is_tac e = match Vernac_classifier.classify_vernac e with
| VtProofStep _, _ -> true
| _ -> false
in
@@ -1437,7 +1497,7 @@ end = struct (* {{{ *)
| _, None -> None
| Some (prev, o, `Cmd { cast = { expr }}), Some n
when is_tac expr && State.same_env o n -> (* A pure tactic *)
- Some (id, `Proof (prev, State.proof_part_of_frozen n))
+ Some (id, `ProofOnly (prev, State.proof_part_of_frozen n))
| Some _, Some s ->
msg_debug (Pp.str "STM: sending back a fat state");
Some (id, `Full s)
@@ -1498,10 +1558,9 @@ and Slaves : sig
end = struct (* {{{ *)
- module TaskQueue = AsyncTaskQueue.MakeQueue(ProofTask)
+ module TaskQueue = AsyncTaskQueue.MakeQueue(ProofTask) ()
let queue = ref None
-
let init () =
if Flags.async_proofs_is_master () then
queue := Some (TaskQueue.create !Flags.async_proofs_n_workers)
@@ -1533,9 +1592,16 @@ end = struct (* {{{ *)
(* 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 ~cache:`No start;
- stm_vernac_interp stop ~proof
+ (* 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 = Vernacentries.freeze_interp_state `No in
+ ignore(stm_vernac_interp stop ~proof st
{ verbose = false; loc; indentation = 0; strlen = 0;
- expr = (VernacEndProof (Proved (Opaque,None))) };
+ expr = (VernacEndProof (Proved (Opaque,None))) });
`OK proof
end
with e ->
@@ -1591,10 +1657,9 @@ end = struct (* {{{ *)
let pr =
Future.from_val (map (Option.get (Global.body_of_constant_body c))) in
let uc =
- Future.chain
- ~pure:true uc Univ.hcons_universe_context_set in
- let pr = Future.chain ~pure:true pr discharge in
- let pr = Future.chain ~pure:true pr Constr.hcons in
+ Future.chain uc Univ.hcons_universe_context_set in
+ let pr = Future.chain pr discharge in
+ let pr = Future.chain pr Constr.hcons in
Future.sink pr;
let extra = Future.join uc in
u.(bucket) <- uc;
@@ -1637,7 +1702,7 @@ end = struct (* {{{ *)
let id, valid as t_exn_info = exn_info in
let cancel_switch = ref false in
if TaskQueue.n_workers (Option.get !queue) = 0 then
- if !Flags.compilation_mode = Flags.BuildVio then begin
+ if VCS.is_vio_doc () then begin
let f,assign =
Future.create_delegate ~blocking:true ~name:pname (State.exn_on id ~valid) in
let t_uuid = Future.uuid f in
@@ -1770,7 +1835,7 @@ end = struct (* {{{ *)
Option.iter VCS.restore vcs;
try
Reach.known_state ~cache:`No id;
- Future.purify (fun () ->
+ stm_purify (fun () ->
let _,_,_,_,sigma0 = Proof.proof (Proof_global.give_me_the_proof ()) in
let g = Evd.find sigma0 r_goal in
let is_ground c = Evarutil.is_ground_term sigma0 (EConstr.of_constr c) in
@@ -1784,7 +1849,14 @@ end = struct (* {{{ *)
else begin
let (i, ast) = r_ast in
Proof_global.simple_with_current_proof (fun _ p -> Proof.focus focus_cond () i p);
- stm_vernac_interp r_state_fb ast;
+ (* STATE SPEC:
+ * - start : id
+ * - return: id
+ * => captures state id in a future closure, which will
+ discard execution state but for the proof + univs.
+ *)
+ let st = Vernacentries.freeze_interp_state `No in
+ ignore(stm_vernac_interp r_state_fb st ast);
let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in
match Evd.(evar_body (find sigma r_goal)) with
| Evd.Evar_empty -> RespNoProgress
@@ -1812,7 +1884,7 @@ and Partac : sig
end = struct (* {{{ *)
- module TaskQueue = AsyncTaskQueue.MakeQueue(TacTask)
+ module TaskQueue = AsyncTaskQueue.MakeQueue(TacTask) ()
let vernac_interp ~solve ~abstract cancel nworkers safe_id id
{ indentation; verbose; loc; expr = e; strlen }
@@ -1823,7 +1895,8 @@ end = struct (* {{{ *)
| VernacRedirect (_,(_,e)) -> find ~time ~fail e
| VernacFail e -> find ~time ~fail:true e
| e -> e, time, fail in find ~time:false ~fail:false e in
- Vernacentries.with_fail fail (fun () ->
+ let st = Vernacentries.freeze_interp_state `No in
+ Vernacentries.with_fail st fail (fun () ->
(if time then System.with_time !Flags.time else (fun x -> x)) (fun () ->
ignore(TaskQueue.with_n_workers nworkers (fun queue ->
Proof_global.with_current_proof (fun _ p ->
@@ -1915,8 +1988,14 @@ end = struct (* {{{ *)
VCS.restore r_doc;
VCS.print ();
Reach.known_state ~cache:`No r_where;
+ (* STATE *)
+ let st = Vernacentries.freeze_interp_state `No in
try
- stm_vernac_interp r_for { r_what with verbose = true };
+ (* STATE SPEC:
+ * - start: r_where
+ * - end : after execution of r_what
+ *)
+ ignore(stm_vernac_interp r_for st { r_what with verbose = true });
feedback ~id:r_for Processed
with e when CErrors.noncritical e ->
let e = CErrors.push e in
@@ -1935,7 +2014,7 @@ and Query : sig
end = struct (* {{{ *)
- module TaskQueue = AsyncTaskQueue.MakeQueue(QueryTask)
+ module TaskQueue = AsyncTaskQueue.MakeQueue(QueryTask) ()
let queue = ref None
@@ -1962,14 +2041,14 @@ let pstate = summary_pstate
let async_policy () =
let open Flags in
if is_universe_polymorphism () then false
- else if interactive () = `Yes then
+ else if VCS.is_interactive () = `Yes then
(async_proofs_is_master () || !async_proofs_mode = APonLazy)
else
- (!compilation_mode = BuildVio || !async_proofs_mode <> APoff)
+ (VCS.is_vio_doc () || !async_proofs_mode <> APoff)
let delegate name =
get_hint_bp_time name >= !Flags.async_proofs_delegation_threshold
- || !Flags.compilation_mode = Flags.BuildVio
+ || VCS.is_vio_doc ()
|| !Flags.async_proofs_full
let warn_deprecated_nested_proofs =
@@ -2030,7 +2109,7 @@ let collect_proof keep cur hd brkind id =
`ASync (parent last,accn,name,delegate name)
| `Fork((_, hd', GuaranteesOpacity, ids), _) when
has_proof_no_using last && not (State.is_cached_and_valid (parent last)) &&
- !Flags.compilation_mode = Flags.BuildVio ->
+ VCS.is_vio_doc () ->
assert (VCS.Branch.equal hd hd'||VCS.Branch.equal hd VCS.edit_branch);
(try
let name, hint = name ids, get_hint_ctx loc in
@@ -2114,7 +2193,7 @@ let known_state ?(redefine_qed=false) ~cache id =
let decl, name = List.hd valid_boxes in
try
let _, dynamic_check = List.assoc name !proof_block_delimiters in
- match dynamic_check decl with
+ match dynamic_check dummy_doc decl with
| `Leaks -> Exninfo.iraise exn
| `ValidBlock { base_state; goals_to_admit; recovery_command } -> begin
let tac =
@@ -2124,14 +2203,20 @@ let known_state ?(redefine_qed=false) ~cache id =
Proofview.give_up else Proofview.tclUNIT ()
end in
match (VCS.get_info base_state).state with
- | Valid { proof } ->
+ | Valid { Vernacentries.proof } ->
Proof_global.unfreeze proof;
Proof_global.with_current_proof (fun _ p ->
feedback ~id:id Feedback.AddedAxiom;
fst (Pfedit.solve Vernacexpr.SelectAll None tac p), ());
- Option.iter (fun expr -> stm_vernac_interp id {
+ (* STATE SPEC:
+ * - start: Modifies the input state adding a proof.
+ * - end : maybe after recovery command.
+ *)
+ (* STATE: We use an updated state with proof *)
+ let st = Vernacentries.freeze_interp_state `No in
+ Option.iter (fun expr -> ignore(stm_vernac_interp id st {
verbose = true; loc = None; expr; indentation = 0;
- strlen = 0 })
+ strlen = 0 } ))
recovery_command
| _ -> assert false
end
@@ -2169,10 +2254,12 @@ let known_state ?(redefine_qed=false) ~cache id =
let inject_non_pstate (s,l) =
Summary.unfreeze_summary s; Lib.unfreeze l; update_global_env ()
in
- let rec pure_cherry_pick_non_pstate safe_id id = Future.purify (fun id ->
- stm_prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id);
- reach ~safe_id id;
- cherry_pick_non_pstate ()) id
+ let rec pure_cherry_pick_non_pstate safe_id id =
+ stm_purify (fun id ->
+ stm_prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id);
+ reach ~safe_id id;
+ cherry_pick_non_pstate ())
+ id
(* traverses the dag backward from nodes being already calculated *)
and reach ?safe_id ?(redefine_qed=false) ?(cache=cache) id =
@@ -2205,7 +2292,10 @@ let known_state ?(redefine_qed=false) ~cache id =
| `Cmd { cast = x; ceff = eff; ctac = true; cblock } -> (fun () ->
resilient_tactic id cblock (fun () ->
reach view.next;
- stm_vernac_interp id x);
+ (* State resulting from reach *)
+ let st = Vernacentries.freeze_interp_state `No in
+ ignore(stm_vernac_interp id st x)
+ );
if eff then update_global_env ()
), (if eff then `Yes else cache), true
| `Cmd { cast = x; ceff = eff } -> (fun () ->
@@ -2213,18 +2303,23 @@ let known_state ?(redefine_qed=false) ~cache id =
| Flags.APon | Flags.APonLazy ->
resilient_command reach view.next
| Flags.APoff -> reach view.next);
- stm_vernac_interp id x;
+ let st = Vernacentries.freeze_interp_state `No in
+ ignore(stm_vernac_interp id st x);
if eff then update_global_env ()
), (if eff then `Yes else cache), true
| `Fork ((x,_,_,_), None) -> (fun () ->
resilient_command reach view.next;
- stm_vernac_interp id x;
+ let st = Vernacentries.freeze_interp_state `No in
+ ignore(stm_vernac_interp id st x);
wall_clock_last_fork := Unix.gettimeofday ()
), `Yes, true
| `Fork ((x,_,_,_), Some prev) -> (fun () -> (* nested proof *)
reach ~cache:`Shallow prev;
reach view.next;
- (try stm_vernac_interp id x;
+
+ (try
+ let st = Vernacentries.freeze_interp_state `No 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
@@ -2274,14 +2369,18 @@ let known_state ?(redefine_qed=false) ~cache id =
Proof_global.close_future_proof ~feedback_id:id fp in
if not delegate then ignore(Future.compute fp);
reach view.next;
- stm_vernac_interp id ~proof x;
+ let st = Vernacentries.freeze_interp_state `No 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
| `Sync (name, `Immediate) -> (fun () ->
- reach eop; stm_vernac_interp id x; Proof_global.discard_all ()
+ reach eop;
+ let st = Vernacentries.freeze_interp_state `No in
+ ignore(stm_vernac_interp id st x);
+ Proof_global.discard_all ()
), `Yes, true
| `Sync (name, reason) -> (fun () ->
log_processing_sync id name reason;
@@ -2302,7 +2401,8 @@ let known_state ?(redefine_qed=false) ~cache id =
if keep != VtKeepAsAxiom then
reach view.next;
let wall_clock2 = Unix.gettimeofday () in
- stm_vernac_interp id ?proof x;
+ let st = Vernacentries.freeze_interp_state `No 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));
@@ -2318,7 +2418,10 @@ let known_state ?(redefine_qed=false) ~cache id =
in
aux (collect_proof keep (view.next, x) brname brinfo eop)
| `Sideff (ReplayCommand x,_) -> (fun () ->
- reach view.next; stm_vernac_interp id x; update_global_env ()
+ reach view.next;
+ let st = Vernacentries.freeze_interp_state `No in
+ ignore(stm_vernac_interp id st x);
+ update_global_env ()
), cache, true
| `Sideff (CherryPickEnv, origin) -> (fun () ->
reach view.next;
@@ -2339,10 +2442,56 @@ end (* }}} *)
(********************************* STM API ************************************)
(******************************************************************************)
-let init () =
- VCS.init Stateid.initial;
- set_undo_classifier Backtrack.undo_vernac_classifier;
- State.define ~cache:`Yes (fun () -> ()) Stateid.initial;
+type stm_init_options = {
+ doc_type : stm_doc_type;
+ require_libs : (string * string option * bool option) list;
+(*
+ fb_handler : Feedback.feedback -> unit;
+ iload_path : (string list * string * bool) list;
+ implicit_std : bool;
+*)
+}
+
+(*
+let doc_type_module_name (std : stm_doc_type) =
+ match std with
+ | VoDoc mn | VioDoc mn | Vio2Vo mn -> mn
+ | Interactive mn -> Names.DirPath.to_string mn
+*)
+
+let init_core () =
+ State.register_root_state ()
+
+let new_doc { doc_type ; require_libs } =
+ let load_objs libs =
+ let rq_file (dir, from, exp) =
+ let mp = Libnames.(Qualid (Loc.tag @@ qualid_of_string dir)) in
+ let mfrom = Option.map (fun fr -> Libnames.(Qualid (Loc.tag @@ qualid_of_string fr))) from in
+ Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in
+ List.(iter rq_file (rev libs))
+ in
+
+ (* We must reset the whole state before creating a document! *)
+ State.restore_root_state ();
+
+ let doc = VCS.init doc_type Stateid.initial in
+
+ begin match doc_type with
+ | Interactive ln ->
+ Declaremods.start_library ln
+ | VoDoc ln ->
+ let ldir = Flags.verbosely Library.start_library ln in
+ VCS.set_ldir ldir;
+ set_compilation_hints ln
+ | VioDoc ln ->
+ let ldir = Flags.verbosely Library.start_library ln in
+ VCS.set_ldir ldir;
+ set_compilation_hints ln
+ end;
+ load_objs require_libs;
+
+ (* We record the state here! *)
+ State.define ~cache:`Yes ~redefine:true (fun () -> ()) Stateid.initial;
Backtrack.record ();
Slaves.init ();
if Flags.async_proofs_is_master () then begin
@@ -2357,35 +2506,39 @@ let init () =
async_proofs_workers_extra_env := Array.of_list
(Str.split_delim (Str.regexp ";") (Str.replace_first env_opt "" env))
with Not_found -> () end;
- end
+ end;
+ doc, VCS.cur_tip ()
-let observe id =
+let observe ~doc id =
let vcs = VCS.backup () in
try
- Reach.known_state ~cache:(interactive ()) id;
- VCS.print ()
+ Reach.known_state ~cache:(VCS.is_interactive ()) id;
+ VCS.print ();
+ doc
with e ->
let e = CErrors.push e in
VCS.print ();
VCS.restore vcs;
Exninfo.iraise e
-let finish () =
+let finish ~doc =
let head = VCS.current_branch () in
- observe (VCS.get_branch_pos head);
+ let doc =observe ~doc (VCS.get_branch_pos head) in
VCS.print ();
(* EJGA: Setting here the proof state looks really wrong, and it
hides true bugs cf bug #5363. Also, what happens with observe? *)
(* Some commands may by side effect change the proof mode *)
- match VCS.get_branch head with
+ (match VCS.get_branch head with
| { VCS.kind = `Edit (mode,_,_,_,_) } -> Proof_global.activate_proof_mode mode [@ocaml.warning "-3"]
| { VCS.kind = `Proof (mode, _) } -> Proof_global.activate_proof_mode mode [@ocaml.warning "-3"]
| _ -> ()
+ ); doc
-let wait () =
- finish ();
+let wait ~doc =
+ let doc = finish ~doc in
Slaves.wait_all_done ();
- VCS.print ()
+ VCS.print ();
+ doc
let rec join_admitted_proofs id =
if Stateid.equal id Stateid.initial then () else
@@ -2396,32 +2549,33 @@ let rec join_admitted_proofs id =
join_admitted_proofs view.next
| _ -> join_admitted_proofs view.next
-let join () =
- wait ();
+let join ~doc =
+ let doc = wait ~doc in
stm_prerr_endline (fun () -> "Joining the environment");
Global.join_safe_environment ();
stm_prerr_endline (fun () -> "Joining Admitted proofs");
join_admitted_proofs (VCS.get_branch_pos (VCS.current_branch ()));
VCS.print ();
- VCS.print ()
+ doc
let dump_snapshot () = Slaves.dump_snapshot (), RemoteCounter.snapshot ()
-type document = VCS.vcs
+
type tasks = int Slaves.tasks * RemoteCounter.remote_counters_status
let check_task name (tasks,rcbackup) i =
RemoteCounter.restore rcbackup;
let vcs = VCS.backup () in
try
- let rc = Future.purify (Slaves.check_task name tasks) i in
+ let rc = stm_purify (Slaves.check_task name tasks) i in
VCS.restore vcs;
rc
with e when CErrors.noncritical e -> VCS.restore vcs; false
let info_tasks (tasks,_) = Slaves.info_tasks tasks
+
let finish_tasks name u d p (t,rcbackup as tasks) =
RemoteCounter.restore rcbackup;
let finish_task u (_,_,i) =
let vcs = VCS.backup () in
- let u = Future.purify (Slaves.finish_task name u d p t) i in
+ let u = stm_purify (Slaves.finish_task name u d p t) i in
VCS.restore vcs;
u in
try
@@ -2451,7 +2605,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 ();
- Reach.known_state ~redefine_qed:true ~cache:`No qed_id;
+ let _st = Reach.known_state ~redefine_qed:true ~cache:`No qed_id in
VCS.checkout VCS.Branch.master;
`Unfocus qed_id
| { VCS.kind = `Master } ->
@@ -2473,17 +2627,49 @@ let handle_failure (e, info) vcs =
VCS.print ();
Exninfo.iraise (e, info)
-let snapshot_vio ldir long_f_dot_vo =
- finish ();
+let snapshot_vio ~doc ldir long_f_dot_vo =
+ let doc = finish ~doc in
if List.length (VCS.branches ()) > 1 then
CErrors.user_err ~hdr:"stm" (str"Cannot dump a vio with open proofs");
Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_vo
- (Global.opaque_tables ())
+ (Global.opaque_tables ());
+ doc
let reset_task_queue = Slaves.reset_task_queue
(* Document building *)
-let process_transaction ?(newtip=Stateid.fresh ())
+let process_back_meta_command ~part_of_script ~newtip ~head oid aast w =
+ match part_of_script, w with
+ | true, w ->
+ let id = VCS.new_node ~id:newtip () in
+ let { mine; others } = Backtrack.branches_of oid in
+ let valid = VCS.get_branch_pos head in
+ List.iter (fun branch ->
+ if not (List.mem_assoc branch (mine::others)) then
+ ignore(merge_proof_branch ~valid aast VtDrop branch))
+ (VCS.branches ());
+ VCS.checkout_shallowest_proof_branch ();
+ let head = VCS.current_branch () in
+ List.iter (fun b ->
+ if not(VCS.Branch.equal b head) then begin
+ VCS.checkout b;
+ VCS.commit (VCS.new_node ()) (Alias (oid,aast));
+ end)
+ (VCS.branches ());
+ VCS.checkout_shallowest_proof_branch ();
+ VCS.commit id (Alias (oid,aast));
+ Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
+
+ | false, VtNow ->
+ stm_prerr_endline (fun () -> "undo to state " ^ Stateid.to_string oid);
+ Backtrack.backto oid;
+ VCS.checkout_shallowest_proof_branch ();
+ Reach.known_state ~cache:(VCS.is_interactive ()) oid; `Ok
+
+ | false, VtLater ->
+ anomaly(str"undo classifier: VtMeta + VtLater must imply part_of_script.")
+
+let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
({ verbose; loc; expr } as x) c =
stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x);
let vcs = VCS.backup () in
@@ -2492,57 +2678,32 @@ let process_transaction ?(newtip=Stateid.fresh ())
VCS.checkout head;
let rc = begin
stm_prerr_endline (fun () ->
- " classified as: " ^ string_of_vernac_classification c);
+ " classified as: " ^ Vernac_classifier.string_of_vernac_classification c);
match c with
- (* Back *)
- | VtBack (true, oid), w ->
- let id = VCS.new_node ~id:newtip () in
- let { mine; others } = Backtrack.branches_of oid in
- let valid = VCS.get_branch_pos head in
- List.iter (fun branch ->
- if not (List.mem_assoc branch (mine::others)) then
- ignore(merge_proof_branch ~valid x VtDrop branch))
- (VCS.branches ());
- VCS.checkout_shallowest_proof_branch ();
- let head = VCS.current_branch () in
- List.iter (fun b ->
- if not(VCS.Branch.equal b head) then begin
- VCS.checkout b;
- VCS.commit (VCS.new_node ()) (Alias (oid,x));
- end)
- (VCS.branches ());
- VCS.checkout_shallowest_proof_branch ();
- VCS.commit id (Alias (oid,x));
- Backtrack.record (); if w == VtNow then finish (); `Ok
- | VtBack (false, id), VtNow ->
- stm_prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id);
- Backtrack.backto id;
- VCS.checkout_shallowest_proof_branch ();
- Reach.known_state ~cache:(interactive ()) id; `Ok
- | VtBack (false, id), VtLater ->
- anomaly(str"classifier: VtBack + VtLater must imply part_of_script.")
-
+ (* Meta *)
+ | VtMeta, _ ->
+ let id, w = Backtrack.undo_vernac_classifier expr in
+ process_back_meta_command ~part_of_script ~newtip ~head id x w
(* Query *)
- | VtQuery (false, route), VtNow ->
- begin
- let query_sid = VCS.cur_tip () in
- try stm_vernac_interp ~route (VCS.cur_tip ()) x
- with e ->
- let e = CErrors.push e in
- Exninfo.iraise (State.exn_on ~valid:Stateid.dummy query_sid e)
- end; `Ok
- (* Part of the script commands don't set the query route *)
- | VtQuery (true, _route), w ->
+ | VtQuery (false,route), VtNow ->
+ let query_sid = VCS.cur_tip () in
+ (try
+ let st = Vernacentries.freeze_interp_state `No in
+ ignore(stm_vernac_interp ~route query_sid st x)
+ with e ->
+ let e = CErrors.push e in
+ Exninfo.iraise (State.exn_on ~valid:Stateid.dummy query_sid e)); `Ok
+ | VtQuery (true, route), w ->
let id = VCS.new_node ~id:newtip () in
let queue =
if !Flags.async_proofs_full then `QueryQueue (ref false)
- else if Flags.(!compilation_mode = BuildVio) &&
+ else if VCS.is_vio_doc () &&
VCS.((get_branch head).kind = `Master) &&
may_pierce_opaque x
then `SkipQueue
else `MainQueue in
VCS.commit id (mkTransCmd x [] false queue);
- Backtrack.record (); if w == VtNow then finish (); `Ok
+ Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
| VtQuery (false,_), VtLater ->
anomaly(str"classifier: VtQuery + VtLater must imply part_of_script.")
@@ -2560,7 +2721,7 @@ let process_transaction ?(newtip=Stateid.fresh ())
VCS.merge id ~ours:(Fork (x, bname, guarantee, names)) head
end;
Proof_global.activate_proof_mode mode [@ocaml.warning "-3"];
- Backtrack.record (); if w == VtNow then finish (); `Ok
+ Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
| VtProofMode _, VtLater ->
anomaly(str"VtProofMode must be executed VtNow.")
| VtProofMode mode, VtNow ->
@@ -2578,7 +2739,7 @@ let process_transaction ?(newtip=Stateid.fresh ())
(VCS.branches ());
VCS.checkout_shallowest_proof_branch ();
Backtrack.record ();
- finish ();
+ ignore(finish ~doc:dummy_doc);
`Ok
| VtProofStep { parallel; proof_block_detection = cblock }, w ->
let id = VCS.new_node ~id:newtip () in
@@ -2591,17 +2752,19 @@ let process_transaction ?(newtip=Stateid.fresh ())
If/when and UI will make something useful with this piece of info,
detection should occur here.
detect_proof_block id cblock; *)
- Backtrack.record (); if w == VtNow then finish (); `Ok
+ Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
| VtQed keep, w ->
let valid = VCS.get_branch_pos head in
let rc = merge_proof_branch ~valid ~id:newtip x keep head in
VCS.checkout_shallowest_proof_branch ();
- Backtrack.record (); if w == VtNow then finish ();
+ Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc);
rc
-
+
(* Side effect on all branches *)
| VtUnknown, _ when expr = VernacToplevelControl Drop ->
- stm_vernac_interp (VCS.get_branch_pos head) x; `Ok
+ let st = Vernacentries.freeze_interp_state `No in
+ ignore(stm_vernac_interp (VCS.get_branch_pos head) st x);
+ `Ok
| VtSideff l, w ->
let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in
@@ -2615,19 +2778,20 @@ let process_transaction ?(newtip=Stateid.fresh ())
| _ -> ReplayCommand x in
VCS.propagate_sideff ~action;
VCS.checkout_shallowest_proof_branch ();
- Backtrack.record (); if w == VtNow then finish (); `Ok
+ Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
(* Unknown: we execute it, check for open goals and propagate sideeff *)
| VtUnknown, VtNow ->
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
- Reach.known_state ~cache:`Yes head_id; (* ensure it is ok *)
+ let _st = Reach.known_state ~cache:`Yes head_id in (* ensure it is ok *)
let step () =
VCS.checkout VCS.Branch.master;
let mid = VCS.get_branch_pos VCS.Branch.master in
- Reach.known_state ~cache:(interactive ()) mid;
- stm_vernac_interp id x;
+ let _st' = Reach.known_state ~cache:(VCS.is_interactive ()) mid in
+ let st = Vernacentries.freeze_interp_state `No 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
begin
@@ -2664,7 +2828,7 @@ let process_transaction ?(newtip=Stateid.fresh ())
let e = CErrors.push e in
handle_failure e vcs
-let get_ast id =
+let get_ast ~doc id =
match VCS.visit id with
| { step = `Cmd { cast = { loc; expr } } }
| { step = `Fork (({ loc; expr }, _, _, _), _) }
@@ -2685,7 +2849,7 @@ let stop_worker n = Slaves.cancel_worker n
*)
exception End_of_input
-let parse_sentence sid pa =
+let parse_sentence ~doc sid pa =
(* XXX: Should this restore the previous state?
Using reach here to try to really get to the
proper state makes the error resilience code fail *)
@@ -2749,7 +2913,7 @@ let compute_indentation ?loc sid = Option.cata (fun loc ->
eff_indent, len
) (0, 0) loc
-let add ~ontop ?newtip verb (loc, ast) =
+let add ~doc ~ontop ?newtip verb (loc, ast) =
let cur_tip = VCS.cur_tip () in
if not (Stateid.equal ontop cur_tip) then
user_err ?loc ~hdr:"Stm.add"
@@ -2759,13 +2923,13 @@ let add ~ontop ?newtip verb (loc, ast) =
let indentation, strlen = compute_indentation ?loc ontop in
CWarnings.set_current_loc loc;
(* XXX: Classifiy vernac should be moved inside process transaction *)
- let clas = classify_vernac ast in
+ let clas = Vernac_classifier.classify_vernac ast in
let aast = { verbose = verb; indentation; strlen; loc; expr = ast } in
match process_transaction ?newtip aast clas with
- | `Ok -> VCS.cur_tip (), `NewTip
- | `Unfocus qed_id -> qed_id, `Unfocus (VCS.cur_tip ())
+ | `Ok -> doc, VCS.cur_tip (), `NewTip
+ | `Unfocus qed_id -> doc, qed_id, `Unfocus (VCS.cur_tip ())
-let set_perspective id_list = Slaves.set_perspective id_list
+let set_perspective ~doc id_list = Slaves.set_perspective id_list
type focus = {
start : Stateid.t;
@@ -2773,23 +2937,23 @@ type focus = {
tip : Stateid.t
}
-let query ~at ~route s =
- Future.purify (fun s ->
- if Stateid.equal at Stateid.dummy then finish ()
+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 ~cache:`Yes at;
- let loc, ast = parse_sentence at s in
+ let loc, ast = parse_sentence ~doc at s in
let indentation, strlen = compute_indentation ?loc at in
CWarnings.set_current_loc loc;
- let clas = classify_vernac ast in
+ let clas = Vernac_classifier.classify_vernac ast in
let aast = { verbose = true; indentation; strlen; loc; expr = ast } in
match clas with
- | VtBack (_,id), _ -> (* TODO: can this still happen ? *)
- ignore(process_transaction aast (VtBack (false,id), VtNow))
+ | VtMeta , _ -> (* TODO: can this still happen ? *)
+ ignore(process_transaction ~part_of_script:false aast (VtMeta,VtNow))
| _ ->
ignore(process_transaction aast (VtQuery (false, route), VtNow)))
s
-let edit_at id =
+let edit_at ~doc id =
if Stateid.equal id Stateid.dummy then anomaly(str"edit_at dummy.") else
let vcs = VCS.backup () in
let on_cur_branch id =
@@ -2834,7 +2998,7 @@ let edit_at id =
VCS.edit_branch (`Edit (mode, qed_id, master_id, keep, old_branch));
VCS.delete_boxes_of id;
cancel_switch := true;
- Reach.known_state ~cache:(interactive ()) id;
+ Reach.known_state ~cache:(VCS.is_interactive ()) id;
VCS.checkout_shallowest_proof_branch ();
`Focus { stop = qed_id; start = master_id; tip } in
let no_edit = function
@@ -2857,7 +3021,7 @@ let edit_at id =
VCS.gc ();
VCS.print ();
if not !Flags.async_proofs_full then
- Reach.known_state ~cache:(interactive ()) id;
+ Reach.known_state ~cache:(VCS.is_interactive ()) id;
VCS.checkout_shallowest_proof_branch ();
`NewTip in
try
@@ -2886,7 +3050,7 @@ let edit_at id =
| true, None, _ ->
if on_cur_branch id then begin
VCS.reset_branch (VCS.current_branch ()) id;
- Reach.known_state ~cache:(interactive ()) id;
+ Reach.known_state ~cache:(VCS.is_interactive ()) id;
VCS.checkout_shallowest_proof_branch ();
`NewTip
end else if is_ancestor_of_cur_branch id then begin
@@ -2898,7 +3062,7 @@ let edit_at id =
| false, None, None -> backto id None
in
VCS.print ();
- rc
+ doc, rc
with e ->
let (e, info) = CErrors.push e in
match Stateid.get info with
@@ -2912,15 +3076,15 @@ let edit_at id =
VCS.print ();
Exninfo.iraise (e, info)
-let backup () = VCS.backup ()
-let restore d = VCS.restore d
+let get_current_state ~doc = VCS.cur_tip ()
+let get_ldir ~doc = VCS.get_ldir ()
-let get_current_state () = VCS.cur_tip ()
+let get_doc did = dummy_doc
(*********************** TTY API (PG, coqtop, coqc) ***************************)
(******************************************************************************)
-let current_proof_depth () =
+let current_proof_depth ~doc =
let head = VCS.current_branch () in
match VCS.get_branch head with
| { VCS.kind = `Master } -> 0
@@ -2939,7 +3103,7 @@ let proofname b = match VCS.get_branch b with
| { VCS.kind = (`Proof _| `Edit _) } -> Some b
| _ -> None
-let get_all_proof_names () =
+let get_all_proof_names ~doc =
List.map unmangle (CList.map_filter proofname (VCS.branches ()))
(* Export hooks *)
diff --git a/stm/stm.mli b/stm/stm.mli
index 3f01fca013..31f4599d36 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -10,9 +10,35 @@ open Names
(** state-transaction-machine interface *)
+(** The STM doc type determines some properties such as what
+ uncompleted proofs are allowed and recording of aux files. *)
+type stm_doc_type =
+ | VoDoc of string
+ | VioDoc of string
+ | Interactive of DirPath.t
+
+(* Main initalization routine *)
+type stm_init_options = {
+ doc_type : stm_doc_type;
+ require_libs : (string * string option * bool option) list;
+(*
+ fb_handler : Feedback.feedback -> unit;
+ iload_path : (string list * string * bool) list;
+ implicit_std : bool;
+*)
+}
+
+(** The type of a STM document *)
+type doc
+
+val init_core : unit -> unit
+
+(* Starts a new document *)
+val new_doc : stm_init_options -> doc * Stateid.t
+
(* [parse_sentence sid pa] Reads a sentence from [pa] with parsing
state [sid] Returns [End_of_input] if the stream ends *)
-val parse_sentence : Stateid.t -> Pcoq.Gram.coq_parsable ->
+val parse_sentence : doc:doc -> Stateid.t -> Pcoq.Gram.coq_parsable ->
Vernacexpr.vernac_expr Loc.located
(* Reminder: A parsable [pa] is constructed using
@@ -26,14 +52,14 @@ exception End_of_input
sync, but it will eventually call edit_at on the fly if needed.
If [newtip] is provided, then the returned state id is guaranteed
to be [newtip] *)
-val add : ontop:Stateid.t -> ?newtip:Stateid.t ->
+val add : doc:doc -> ontop:Stateid.t -> ?newtip:Stateid.t ->
bool -> Vernacexpr.vernac_expr Loc.located ->
- Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]
+ doc * Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]
(* [query at ?report_with cmd] Executes [cmd] at a given state [at],
throwing away side effects except messages. Feedback will
be sent with [report_with], which defaults to the dummy state id *)
-val query :
+val query : doc:doc ->
at:Stateid.t -> route:Feedback.route_id -> Pcoq.Gram.coq_parsable -> unit
(* [edit_at id] is issued to change the editing zone. [`NewTip] is returned if
@@ -46,27 +72,27 @@ val query :
If Flags.async_proofs_full is set, then [id] is not [observe]d, else it is.
*)
type focus = { start : Stateid.t; stop : Stateid.t; tip : Stateid.t }
-val edit_at : Stateid.t -> [ `NewTip | `Focus of focus ]
+val edit_at : doc:doc -> Stateid.t -> doc * [ `NewTip | `Focus of focus ]
(* Evaluates the tip of the current branch *)
-val finish : unit -> unit
+val finish : doc:doc -> doc
(* Internal use (fake_ide) only, do not use *)
-val wait : unit -> unit
+val wait : doc:doc -> doc
-val observe : Stateid.t -> unit
+val observe : doc:doc -> Stateid.t -> doc
val stop_worker : string -> unit
(* Joins the entire document. Implies finish, but also checks proofs *)
-val join : unit -> unit
+val join : doc:doc -> doc
(* Saves on the disk a .vio corresponding to the current status:
- if the worker pool is empty, all tasks are saved
- if the worker proof is not empty, then it waits until all workers
are done with their current jobs and then dumps (or fails if one
of the completed tasks is a failure) *)
-val snapshot_vio : DirPath.t -> string -> unit
+val snapshot_vio : doc:doc -> DirPath.t -> string -> doc
(* Empties the task queue, can be used only if the worker pool is empty (E.g.
* after having built a .vio in batch mode *)
@@ -81,23 +107,17 @@ val finish_tasks : string ->
tasks -> Library.seg_univ * Library.seg_proofs
(* Id of the tip of the current branch *)
-val get_current_state : unit -> Stateid.t
-
-(* Misc *)
-val init : unit -> unit
+val get_current_state : doc:doc -> Stateid.t
+val get_ldir : doc:doc -> Names.DirPath.t
(* This returns the node at that position *)
-val get_ast : Stateid.t -> (Vernacexpr.vernac_expr Loc.located) option
+val get_ast : doc:doc -> Stateid.t -> (Vernacexpr.vernac_expr Loc.located) option
(* Filename *)
val set_compilation_hints : string -> unit
(* Reorders the task queue putting forward what is in the perspective *)
-val set_perspective : Stateid.t list -> unit
-
-type document
-val backup : unit -> document
-val restore : document -> unit
+val set_perspective : doc:doc -> Stateid.t list -> unit
(** workers **************************************************************** **)
@@ -112,20 +132,20 @@ module QueryTask : AsyncTaskQueue.Task
While checking a proof, if an error occurs in a (valid) block then
processing can skip the entire block and go on to give feedback
on the rest of the proof.
-
+
static_block_detection and dynamic_block_validation are run when
the closing block marker is parsed/executed respectively.
-
+
static_block_detection is for example called when "}" is parsed and
declares a block containing all proof steps between it and the matching
"{".
-
+
dynamic_block_validation is called when an error "crosses" the "}" statement.
Depending on the nature of the goal focused by "{" the block may absorb the
error or not. For example if the focused goal occurs in the type of
another goal, then the block is leaky.
Note that one can design proof commands that need no dynamic validation.
-
+
Example of document:
.. { tac1. tac2. } ..
@@ -133,7 +153,7 @@ module QueryTask : AsyncTaskQueue.Task
Corresponding DAG:
.. (3) <-- { -- (4) <-- tac1 -- (5) <-- tac2 -- (6) <-- } -- (7) ..
-
+
Declaration of block [-------------------------------------------]
start = 5 the first state_id that could fail in the block
@@ -173,7 +193,7 @@ type recovery_action = {
}
type dynamic_block_error_recovery =
- static_block_declaration -> [ `ValidBlock of recovery_action | `Leaks ]
+ doc -> static_block_declaration -> [ `ValidBlock of recovery_action | `Leaks ]
val register_proof_block_delimiter :
Vernacexpr.proof_block_name ->
@@ -197,14 +217,11 @@ val state_ready_hook : (Stateid.t -> unit) Hook.t
(* Messages from the workers to the master *)
val forward_feedback_hook : (Feedback.feedback -> unit) Hook.t
-type state = {
- system : States.state;
- proof : Proof_global.state;
- shallow : bool
-}
-val state_of_id :
- Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ]
+val get_doc : Feedback.doc_id -> doc
+
+val state_of_id : doc:doc ->
+ Stateid.t -> [ `Valid of Vernacentries.interp_state option | `Expired | `Error of exn ]
(* Queries for backward compatibility *)
-val current_proof_depth : unit -> int
-val get_all_proof_names : unit -> Id.t list
+val current_proof_depth : doc:doc -> int
+val get_all_proof_names : doc:doc -> Id.t list
diff --git a/stm/tacworkertop.ml b/stm/tacworkertop.ml
index 186c8f8b7c..17f90b7b15 100644
--- a/stm/tacworkertop.ml
+++ b/stm/tacworkertop.ml
@@ -6,9 +6,9 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-module W = AsyncTaskQueue.MakeWorker(Stm.TacTask)
+module W = AsyncTaskQueue.MakeWorker(Stm.TacTask) ()
let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
-let () = Coqtop.toploop_run := W.main_loop
+let () = Coqtop.toploop_run := (fun _ -> W.main_loop ())
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 158ad90846..3aa2cd707e 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -31,7 +31,7 @@ let string_of_vernac_type = function
Option.default "" proof_block_detection
| VtProofMode s -> "ProofMode " ^ s
| VtQuery (b, route) -> "Query " ^ string_of_in_script b ^ " route " ^ string_of_int route
- | VtBack (b, _) -> "Stm Back " ^ string_of_in_script b
+ | VtMeta -> "Meta "
let string_of_vernac_when = function
| VtLater -> "Later"
@@ -53,9 +53,6 @@ let make_polymorphic (a, b as x) =
VtStartProof (x, Doesn'tGuaranteeOpacity, ids), b
| _ -> x
-let undo_classifier = ref (fun _ -> assert false)
-let set_undo_classifier f = undo_classifier := f
-
let rec classify_vernac e =
let static_classifier e = match e with
(* Univ poly compatibility: we run it now, so that we can just
@@ -75,7 +72,7 @@ let rec classify_vernac e =
| VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
(match classify_vernac e with
| ( VtQuery _ | VtProofStep _ | VtSideff _
- | VtBack _ | VtProofMode _ ), _ as x -> x
+ | VtProofMode _ | VtMeta), _ as x -> x
| VtQed _, _ ->
VtProofStep { parallel = `No; proof_block_detection = None },
VtNow
@@ -191,7 +188,7 @@ let rec classify_vernac e =
| VernacBack _ | VernacAbortAll
| VernacUndoTo _ | VernacUndo _
| VernacResetName _ | VernacResetInitial
- | VernacBacktrack _ | VernacBackTo _ | VernacRestart -> !undo_classifier e
+ | VernacBacktrack _ | VernacBackTo _ | VernacRestart -> VtMeta, VtNow
(* What are these? *)
| VernacToplevelControl _
| VernacRestoreState _
diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli
index 2fa1e0b8dc..fe42a03a3d 100644
--- a/stm/vernac_classifier.mli
+++ b/stm/vernac_classifier.mli
@@ -18,9 +18,6 @@ val classify_vernac : vernac_expr -> vernac_classification
val declare_vernac_classifier :
Vernacexpr.extend_name -> (raw_generic_argument list -> unit -> vernac_classification) -> unit
-(** Set by Stm *)
-val set_undo_classifier : (vernac_expr -> vernac_classification) -> unit
-
(** Standard constant classifiers *)
val classify_as_query : vernac_classification
val classify_as_sideeff : vernac_classification
diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml
index 9507e90ba7..da6a095ab7 100644
--- a/stm/vio_checking.ml
+++ b/stm/vio_checking.ml
@@ -14,7 +14,7 @@ let check_vio (ts,f) =
Stm.set_compilation_hints long_f_dot_v;
List.fold_left (fun acc ids -> Stm.check_task f tasks ids && acc) true ts
-module Worker = Spawn.Sync(struct end)
+module Worker = Spawn.Sync ()
module IntOT = struct
type t = int
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 12:41:10 +0000