aboutsummaryrefslogtreecommitdiff
path: root/stm
diff options
context:
space:
mode:
Diffstat (limited to 'stm')
-rw-r--r--stm/stm.ml97
-rw-r--r--stm/stm.mli36
-rw-r--r--stm/vernac_classifier.ml15
3 files changed, 61 insertions, 87 deletions
diff --git a/stm/stm.ml b/stm/stm.ml
index dbecbdae54..ba0a2017a3 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1072,7 +1072,7 @@ let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t
let is_filtered_command = function
| VernacResetName _ | VernacResetInitial | VernacBack _
| VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _
- | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true
+ | VernacAbortAll | VernacAbort _ -> true
| _ -> false
in
let aux_interp st expr =
@@ -1097,7 +1097,6 @@ let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t
module Backtrack : sig
val record : unit -> unit
- val backto : Stateid.t -> unit
(* we could navigate the dag, but this ways easy *)
val branches_of : Stateid.t -> backup
@@ -1122,14 +1121,6 @@ end = struct (* {{{ *)
info.vcs_backup <- backup, branches)
[VCS.current_branch (); VCS.Branch.master]
- let backto oid =
- let info = VCS.get_info oid in
- match info.vcs_backup with
- | None, _ ->
- anomaly Pp.(str"Backtrack.backto "++str(Stateid.to_string oid)++
- str": a state with no vcs_backup.")
- | Some vcs, _ -> VCS.restore vcs
-
let branches_of id =
let info = VCS.get_info id in
match info.vcs_backup with
@@ -1220,7 +1211,6 @@ end = struct (* {{{ *)
match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ())
() id in
oid, VtLater
- | VernacBacktrack (id,_,_)
| VernacBackTo id ->
Stateid.of_int id, VtNow
| _ -> anomaly Pp.(str "incorrect VtMeta classification")
@@ -2734,7 +2724,6 @@ let merge_proof_branch ~valid ?id qast keep brname =
(* When tty is true, this code also does some of the job of the user interface:
jump back to a state that is valid *)
let handle_failure (e, info) vcs =
- if e = CErrors.Drop then Exninfo.iraise (e, info) else
match Stateid.get info with
| None ->
VCS.restore vcs;
@@ -2758,9 +2747,7 @@ let snapshot_vio ~doc ldir long_f_dot_vo =
let reset_task_queue = Slaves.reset_task_queue
(* Document building *)
-let process_back_meta_command ~part_of_script ~newtip ~head oid aast w =
- match part_of_script, w with
- | true, w ->
+let process_back_meta_command ~newtip ~head oid aast 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
@@ -2780,16 +2767,7 @@ let process_back_meta_command ~part_of_script ~newtip ~head oid aast w =
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)
+let process_transaction ?(newtip=Stateid.fresh ())
({ verbose; loc; expr } as x) c =
stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x);
let vcs = VCS.backup () in
@@ -2803,22 +2781,10 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
(* Meta *)
| VtMeta, _ ->
let id, w = Backtrack.undo_vernac_classifier expr in
- (* Special case Backtrack, as it is never part of a script. See #6240 *)
- let part_of_script = begin match Vernacprop.under_control expr with
- | VernacBacktrack _ -> false
- | _ -> part_of_script
- end in
- process_back_meta_command ~part_of_script ~newtip ~head id x w
+ process_back_meta_command ~newtip ~head id x w
+
(* Query *)
- | VtQuery (false,route), VtNow ->
- let query_sid = VCS.cur_tip () in
- (try
- let st = Vernacstate.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 ->
+ | VtQuery, w ->
let id = VCS.new_node ~id:newtip () in
let queue =
if !cur_opt.async_proofs_full then `QueryQueue (ref false)
@@ -2830,9 +2796,6 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
VCS.commit id (mkTransCmd x [] false queue);
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.")
-
(* Proof *)
| VtStartProof (mode, guarantee, names), w ->
let id = VCS.new_node ~id:newtip () in
@@ -2885,23 +2848,22 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc);
rc
- (* Side effect on all branches *)
- | VtUnknown, _ when Vernacprop.under_control expr = VernacToplevelControl Drop ->
- let st = Vernacstate.freeze_interp_state `No in
- ignore(stm_vernac_interp (VCS.get_branch_pos head) st x);
- `Ok
-
+ (* Side effect in a (still open) proof is replayed on all branches*)
| VtSideff l, w ->
- let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in
let id = VCS.new_node ~id:newtip () in
- VCS.checkout VCS.Branch.master;
- VCS.commit id (mkTransCmd x l in_proof `MainQueue);
- (* We can't replay a Definition since universes may be differently
- * inferred. This holds in Coq >= 8.5 *)
- let action = match Vernacprop.under_control x.expr with
- | VernacDefinition(_, _, DefineBody _) -> CherryPickEnv
- | _ -> ReplayCommand x in
- VCS.propagate_sideff ~action;
+ begin match (VCS.get_branch head).VCS.kind with
+ | `Edit _ -> VCS.commit id (mkTransCmd x l true `MainQueue);
+ | `Master -> VCS.commit id (mkTransCmd x l false `MainQueue);
+ | `Proof _ ->
+ VCS.checkout VCS.Branch.master;
+ VCS.commit id (mkTransCmd x l true `MainQueue);
+ (* We can't replay a Definition since universes may be differently
+ * inferred. This holds in Coq >= 8.5 *)
+ let action = match Vernacprop.under_control x.expr with
+ | VernacDefinition(_, _, DefineBody _) -> CherryPickEnv
+ | _ -> ReplayCommand x in
+ VCS.propagate_sideff ~action;
+ end;
VCS.checkout_shallowest_proof_branch ();
Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
@@ -2930,9 +2892,14 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
VCS.branch bname (`Proof (proof_mode, VCS.proof_nesting () + 1));
Proof_global.activate_proof_mode proof_mode [@ocaml.warning "-3"];
end else begin
- VCS.commit id (mkTransCmd x [] in_proof `MainQueue);
- (* We hope it can be replayed, but we can't really know *)
- VCS.propagate_sideff ~action:(ReplayCommand x);
+ begin match (VCS.get_branch head).VCS.kind with
+ | `Edit _ -> VCS.commit id (mkTransCmd x [] in_proof `MainQueue);
+ | `Master -> VCS.commit id (mkTransCmd x [] in_proof `MainQueue);
+ | `Proof _ ->
+ VCS.commit id (mkTransCmd x [] in_proof `MainQueue);
+ (* We hope it can be replayed, but we can't really know *)
+ VCS.propagate_sideff ~action:(ReplayCommand x);
+ end;
VCS.checkout_shallowest_proof_branch ();
end in
State.define ~safe_id:head_id ~cache:`Yes step id;
@@ -3071,13 +3038,9 @@ let query ~doc ~at ~route s =
let { CAst.loc; v=ast } = parse_sentence ~doc at s in
let indentation, strlen = compute_indentation ?loc at in
CWarnings.set_current_loc loc;
- let clas = Vernac_classifier.classify_vernac ast in
+ let st = State.get_cached at in
let aast = { verbose = true; indentation; strlen; loc; expr = ast } in
- match clas with
- | VtMeta , _ -> (* TODO: can this still happen ? *)
- ignore(process_transaction ~part_of_script:false aast (VtMeta,VtNow))
- | _ ->
- ignore(process_transaction aast (VtQuery (false,route), VtNow))
+ ignore(stm_vernac_interp ~route at st aast)
done;
with
| End_of_input -> ()
diff --git a/stm/stm.mli b/stm/stm.mli
index a8eb10fb33..7a720aa72a 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -39,14 +39,25 @@ module AsyncOpts : sig
end
-(** The STM doc type determines some properties such as what
- uncompleted proofs are allowed and recording of aux files. *)
+(** The STM document type [stm_doc_type] determines some properties
+ such as what uncompleted proofs are allowed and what gets recorded
+ to aux files. *)
type stm_doc_type =
- | VoDoc of string
- | VioDoc of string
- | Interactive of DirPath.t
+ | VoDoc of string (* file path *)
+ | VioDoc of string (* file path *)
+ | Interactive of DirPath.t (* module path *)
-(* Main initalization routine *)
+(** Coq initalization options:
+
+ - [doc_type]: Type of document being created.
+
+ - [require_libs]: list of libraries/modules to be pre-loaded at
+ startup. A tuple [(modname,modfrom,import)] is equivalent to [From
+ modfrom Require modname]; [import] works similarly to
+ [Library.require_library_from_dirpath], [Some false] will import
+ the module, [Some true] will additionally export it.
+
+*)
type stm_init_options = {
(* The STM will set some internal flags differently depending on the
specified [doc_type]. This distinction should dissappear at some
@@ -72,12 +83,14 @@ type stm_init_options = {
(** The type of a STM document *)
type doc
+(** [init_core] performs some low-level initalization; should go away
+ in future releases. *)
val init_core : unit -> unit
-(* Starts a new document *)
+(** [new_doc opt] Creates a new document with options [opt] *)
val new_doc : stm_init_options -> doc * Stateid.t
-(* [parse_sentence sid pa] Reads a sentence from [pa] with parsing
+(** [parse_sentence sid pa] Reads a sentence from [pa] with parsing
state [sid] Returns [End_of_input] if the stream ends *)
val parse_sentence : doc:doc -> Stateid.t -> Pcoq.Gram.coq_parsable ->
Vernacexpr.vernac_control CAst.t
@@ -115,14 +128,15 @@ val query : doc:doc ->
type focus = { start : Stateid.t; stop : Stateid.t; tip : Stateid.t }
val edit_at : doc:doc -> Stateid.t -> doc * [ `NewTip | `Focus of focus ]
-(* Evaluates the tip of the current branch *)
+(* [observe doc sid]] Check / execute span [sid] *)
+val observe : doc:doc -> Stateid.t -> doc
+
+(* [finish doc] Fully checks a document up to the "current" tip. *)
val finish : doc:doc -> doc
(* Internal use (fake_ide) only, do not use *)
val wait : doc:doc -> doc
-val observe : doc:doc -> Stateid.t -> doc
-
val stop_worker : string -> unit
(* Joins the entire document. Implies finish, but also checks proofs *)
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index f68c8b326b..c08cc6e367 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -16,8 +16,6 @@ open Vernacexpr
let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"]
-let string_of_in_script b = if b then " (inside script)" else ""
-
let string_of_parallel = function
| `Yes (solve,abs) ->
"par" ^ if solve then "solve" else "" ^ if abs then "abs" else ""
@@ -34,7 +32,7 @@ let string_of_vernac_type = function
"ProofStep " ^ string_of_parallel parallel ^
Option.default "" proof_block_detection
| VtProofMode s -> "ProofMode " ^ s
- | VtQuery (b, route) -> "Query " ^ string_of_in_script b ^ " route " ^ string_of_int route
+ | VtQuery -> "Query"
| VtMeta -> "Meta "
let string_of_vernac_when = function
@@ -70,7 +68,7 @@ let classify_vernac e =
| VernacEndProof _ | VernacExactProof _ -> VtQed VtKeep, VtLater
(* Query *)
| VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _
- | VernacCheckMayEval _ -> VtQuery (true,Feedback.default_route), VtLater
+ | VernacCheckMayEval _ -> VtQuery, VtLater
(* ProofStep *)
| VernacProof _
| VernacFocus _ | VernacUnfocus
@@ -145,7 +143,7 @@ let classify_vernac e =
| VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _
| VernacChdir _
| VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _
- | VernacDeclareImplicits _ | VernacArguments _ | VernacArgumentsScope _
+ | VernacArguments _
| VernacReserve _
| VernacGeneralizable _
| VernacSetOpacity _ | VernacSetStrategy _
@@ -183,9 +181,8 @@ let classify_vernac e =
| VernacBack _ | VernacAbortAll
| VernacUndoTo _ | VernacUndo _
| VernacResetName _ | VernacResetInitial
- | VernacBacktrack _ | VernacBackTo _ | VernacRestart -> VtMeta, VtNow
+ | VernacBackTo _ | VernacRestart -> VtMeta, VtNow
(* What are these? *)
- | VernacToplevelControl _
| VernacRestoreState _
| VernacWriteState _ -> VtSideff [], VtNow
(* Plugins should classify their commands *)
@@ -206,7 +203,7 @@ let classify_vernac e =
static_control_classifier ~poly e
| VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
(match static_control_classifier ~poly e with
- | ( VtQuery _ | VtProofStep _ | VtSideff _
+ | ( VtQuery | VtProofStep _ | VtSideff _
| VtProofMode _ | VtMeta), _ as x -> x
| VtQed _, _ ->
VtProofStep { parallel = `No; proof_block_detection = None },
@@ -215,6 +212,6 @@ let classify_vernac e =
in
static_control_classifier ~poly:(Flags.is_universe_polymorphism ()) e
-let classify_as_query = VtQuery (true,Feedback.default_route), VtLater
+let classify_as_query = VtQuery, VtLater
let classify_as_sideeff = VtSideff [], VtLater
let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}, VtLater
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 06:44:26 +0000