summaryrefslogtreecommitdiff
path: root/stm/stm.ml
diff options
context:
space:
mode:
Diffstat (limited to 'stm/stm.ml')
-rw-r--r--stm/stm.ml234
1 files changed, 116 insertions, 118 deletions
diff --git a/stm/stm.ml b/stm/stm.ml
index e1b90bd2..ada7e3e3 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -92,11 +92,11 @@ let execution_error ?loc state_id msg =
module Hooks = struct
let state_computed, state_computed_hook = Hook.make
- ~default:(fun state_id ~in_cache ->
+ ~default:(fun ~doc:_ state_id ~in_cache ->
feedback ~id:state_id Processed) ()
let state_ready, state_ready_hook = Hook.make
- ~default:(fun state_id -> ()) ()
+ ~default:(fun ~doc:_ state_id -> ()) ()
let forward_feedback, forward_feedback_hook =
let m = Mutex.create () in
@@ -106,7 +106,7 @@ let forward_feedback, forward_feedback_hook =
with e -> Mutex.unlock m; raise e) ()
let unreachable_state, unreachable_state_hook = Hook.make
- ~default:(fun _ _ -> ()) ()
+ ~default:(fun ~doc:_ _ _ -> ()) ()
include Hook
@@ -578,7 +578,7 @@ end = struct (* {{{ *)
| None -> raise Vcs_aux.Expired
let set_state id s =
(get_info id).state <- s;
- if async_proofs_is_master !cur_opt then Hooks.(call state_ready id)
+ if async_proofs_is_master !cur_opt then Hooks.(call state_ready ~doc:dummy_doc (* XXX should be taken in input *) id)
let get_state id = (get_info id).state
let reached id =
let info = get_info id in
@@ -770,6 +770,7 @@ module State : sig
Warning: an optimization in installed_cached requires that state
modifying functions are always executed using this wrapper. *)
val define :
+ doc:doc ->
?safe_id:Stateid.t ->
?redefine:bool -> ?cache:Summary.marshallable ->
?feedback_processed:bool -> (unit -> unit) -> Stateid.t -> unit
@@ -919,7 +920,7 @@ end = struct (* {{{ *)
let e2 = Summary.project_from_summary s2 Global.global_env_summary_tag in
e1 == e2
- let define ?safe_id ?(redefine=false) ?(cache=`No) ?(feedback_processed=true)
+ let define ~doc ?safe_id ?(redefine=false) ?(cache=`No) ?(feedback_processed=true)
f id
=
feedback ~id:id (ProcessingIn !Flags.async_proofs_worker_id);
@@ -938,7 +939,7 @@ end = struct (* {{{ *)
stm_prerr_endline (fun () -> "setting cur id to "^str_id);
cur_id := id;
if feedback_processed then
- Hooks.(call state_computed id ~in_cache:false);
+ Hooks.(call state_computed ~doc id ~in_cache:false);
VCS.reached id;
if Proof_global.there_are_pending_proofs () then
VCS.goals id (Proof_global.get_open_goals ())
@@ -954,7 +955,7 @@ end = struct (* {{{ *)
| 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;
- Hooks.(call unreachable_state id ie);
+ Hooks.(call unreachable_state ~doc id ie);
Exninfo.iraise ie
let init_state = ref None
@@ -1072,7 +1073,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,13 +1098,13 @@ 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
(* Returns the state that the command should backtract to *)
- val undo_vernac_classifier : vernac_control -> Stateid.t * vernac_when
+ val undo_vernac_classifier : vernac_control -> doc:doc -> Stateid.t * vernac_when
+ val get_prev_proof : doc:doc -> Stateid.t -> Proof.t option
end = struct (* {{{ *)
@@ -1122,14 +1123,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
@@ -1169,7 +1162,17 @@ end = struct (* {{{ *)
" If your use is intentional, you may want to disable this warning and pass" ^
" the \"-async-proofs-cache force\" option to Coq."))
- let undo_vernac_classifier v =
+ let back_tactic 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)
+
+ let get_proof ~doc id =
+ let open Vernacstate in
+ match state_of_id ~doc id with
+ | `Valid (Some vstate) -> Some (Proof_global.proof_of_state vstate.proof)
+ | _ -> None
+
+ let undo_vernac_classifier v ~doc =
if VCS.is_interactive () = `No && !cur_opt.async_proofs_cache <> Some Force
then undo_costly_in_batch_mode v;
try
@@ -1193,9 +1196,7 @@ end = struct (* {{{ *)
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
+ let oid = fold_until back_tactic n id in
oid, VtLater
| VernacUndoTo _
| VernacRestart as e ->
@@ -1220,7 +1221,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")
@@ -1229,8 +1229,29 @@ end = struct (* {{{ *)
CErrors.user_err ~hdr:"undo_vernac_classifier"
Pp.(str "Cannot undo")
+ let get_prev_proof ~doc id =
+ try
+ let np = get_proof ~doc id in
+ match np with
+ | None -> None
+ | Some cp ->
+ let did = ref id in
+ let rv = ref np in
+ let done_ = ref false in
+ while not !done_ do
+ did := fold_until back_tactic 1 !did;
+ rv := get_proof ~doc !did;
+ done_ := match !rv with
+ | Some rv -> not (Goal.Set.equal (Proof.all_goals rv) (Proof.all_goals cp))
+ | None -> true
+ done;
+ !rv
+ with Not_found | Proof_global.NoCurrentProof -> None
+
end (* }}} *)
+let get_prev_proof = Backtrack.get_prev_proof
+
let hints = ref Aux_file.empty_aux_file
let set_compilation_hints file =
hints := Aux_file.load_aux_file_for file
@@ -1343,7 +1364,7 @@ module rec ProofTask : sig
t_stop : Stateid.t;
t_drop : bool;
t_states : competence;
- t_assign : Proof_global.closed_proof_output Future.assignement -> unit;
+ t_assign : Proof_global.closed_proof_output Future.assignment -> unit;
t_loc : Loc.t option;
t_uuid : Future.UUID.t;
t_name : string }
@@ -1362,6 +1383,7 @@ module rec ProofTask : sig
and type request := request
val build_proof_here :
+ doc:doc ->
?loc:Loc.t ->
drop_pt:bool ->
Stateid.t * Stateid.t -> Stateid.t ->
@@ -1381,7 +1403,7 @@ end = struct (* {{{ *)
t_stop : Stateid.t;
t_drop : bool;
t_states : competence;
- t_assign : Proof_global.closed_proof_output Future.assignement -> unit;
+ t_assign : Proof_global.closed_proof_output Future.assignment -> unit;
t_loc : Loc.t option;
t_uuid : Future.UUID.t;
t_name : string }
@@ -1476,11 +1498,12 @@ end = struct (* {{{ *)
execution_error start (Pp.strbrk s);
feedback (InProgress ~-1)
- let build_proof_here ?loc ~drop_pt (id,valid) eop =
+ 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 ~cache:`No eop
- else Reach.known_state ~cache:`Shallow eop;
+ if VCS.is_interactive () = `No
+ then Reach.known_state ~doc ~cache:`No eop
+ else Reach.known_state ~doc ~cache:`Shallow eop;
let wall_clock2 = Unix.gettimeofday () in
Aux_file.record_in_aux_at ?loc "proof_build_time"
(Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
@@ -1494,7 +1517,7 @@ end = struct (* {{{ *)
VCS.print ();
let proof, future_proof, time =
let wall_clock = Unix.gettimeofday () in
- let fp = build_proof_here ?loc ~drop_pt:drop exn_info stop in
+ let fp = build_proof_here ~doc:dummy_doc (* XXX should be document *) ?loc ~drop_pt:drop exn_info stop in
let proof = Future.force fp in
proof, fp, Unix.gettimeofday () -. wall_clock in
(* We typecheck the proof with the kernel (in the worker) to spot
@@ -1518,7 +1541,7 @@ end = struct (* {{{ *)
stm_vernac_interp stop
~proof:(pobject, terminator) st
{ verbose = false; loc; indentation = 0; strlen = 0;
- expr = VernacExpr ([], VernacEndProof (Proved (Opaque,None))) }) in
+ expr = VernacExpr ([], VernacEndProof (Proved (Proof_global.Opaque,None))) }) in
ignore(Future.join checked_proof);
end;
(* STATE: Restore the state XXX: handle exn *)
@@ -1587,7 +1610,7 @@ end = struct (* {{{ *)
msg_warning Pp.(strbrk("Marshalling error: "^s^". "^
"The system state could not be sent to the worker process. "^
"Falling back to local, lazy, evaluation."));
- t_assign(`Comp(build_proof_here ?loc:t_loc ~drop_pt t_exn_info t_stop));
+ t_assign(`Comp(build_proof_here ~doc:dummy_doc (* XXX should be stored in a closure, it is the same doc that was used to generate the task *) ?loc:t_loc ~drop_pt t_exn_info t_stop));
feedback (InProgress ~-1)
end (* }}} *)
@@ -1597,6 +1620,7 @@ and Slaves : sig
(* (eventually) remote calls *)
val build_proof :
+ doc:doc ->
?loc:Loc.t -> drop_pt:bool ->
exn_info:(Stateid.t * Stateid.t) -> block_start:Stateid.t -> block_stop:Stateid.t ->
name:string -> future_proof * AsyncTaskQueue.cancel_switch
@@ -1644,7 +1668,7 @@ end = struct (* {{{ *)
with VCS.Expired -> cur in
aux stop in
try
- Reach.known_state ~cache:`No stop;
+ Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:`No stop;
if drop then
let _proof = Proof_global.return_proof ~allow_partial:true () in
`OK_ADMITTED
@@ -1657,7 +1681,7 @@ end = struct (* {{{ *)
Proof_global.close_proof ~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 ~cache:`No start;
+ Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:`No start;
(* STATE SPEC:
* - start: First non-expired state! [This looks very fishy]
* - end : start + qed
@@ -1667,7 +1691,7 @@ end = struct (* {{{ *)
let st = Vernacstate.freeze_interp_state `No in
ignore(stm_vernac_interp stop ~proof st
{ verbose = false; loc; indentation = 0; strlen = 0;
- expr = VernacExpr ([], VernacEndProof (Proved (Opaque,None))) });
+ expr = VernacExpr ([], VernacEndProof (Proved (Proof_global.Opaque,None))) });
`OK proof
end
with e ->
@@ -1764,7 +1788,7 @@ end = struct (* {{{ *)
BuildProof { t_states = s2 } -> overlap_rel s1 s2
| _ -> 0)
- let build_proof ?loc ~drop_pt ~exn_info ~block_start ~block_stop ~name:pname =
+ let build_proof ~doc ?loc ~drop_pt ~exn_info ~block_start ~block_stop ~name:pname =
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
@@ -1779,7 +1803,7 @@ end = struct (* {{{ *)
TaskQueue.enqueue_task (Option.get !queue) task ~cancel_switch;
f, cancel_switch
end else
- ProofTask.build_proof_here ?loc ~drop_pt t_exn_info block_stop, cancel_switch
+ ProofTask.build_proof_here ~doc ?loc ~drop_pt t_exn_info block_stop, cancel_switch
else
let f, t_assign = Future.create_delegate ~name:pname (State.exn_on id ~valid) in
let t_uuid = Future.uuid f in
@@ -1819,7 +1843,7 @@ and TacTask : sig
type task = {
t_state : Stateid.t;
t_state_fb : Stateid.t;
- t_assign : output Future.assignement -> unit;
+ t_assign : output Future.assignment -> unit;
t_ast : int * aast;
t_goal : Goal.goal;
t_kill : unit -> unit;
@@ -1836,7 +1860,7 @@ end = struct (* {{{ *)
type task = {
t_state : Stateid.t;
t_state_fb : Stateid.t;
- t_assign : output Future.assignement -> unit;
+ t_assign : output Future.assignment -> unit;
t_ast : int * aast;
t_goal : Goal.goal;
t_kill : unit -> unit;
@@ -1855,7 +1879,7 @@ end = struct (* {{{ *)
| RespError of Pp.t
| RespNoProgress
- let name = ref "tacworker"
+ let name = ref "tacticworker"
let extra_env () = [||]
type competence = unit
type worker_status = Fresh | Old of competence
@@ -1902,11 +1926,11 @@ 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 ~cache:`No id;
+ Reach.known_state ~doc:dummy_doc (* XXX should be vcs *) ~cache:`No id;
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
+ let is_ground c = Evarutil.is_ground_term sigma0 c in
if not (
is_ground Evd.(evar_concl g) &&
List.for_all (Context.Named.Declaration.for_all is_ground)
@@ -1929,7 +1953,6 @@ end = struct (* {{{ *)
match Evd.(evar_body (find sigma r_goal)) with
| Evd.Evar_empty -> RespNoProgress
| Evd.Evar_defined t ->
- let t = EConstr.of_constr t in
let t = Evarutil.nf_evar sigma t in
if Evarutil.is_ground_term sigma t then
let t = EConstr.Unsafe.to_constr t in
@@ -2058,7 +2081,7 @@ end = struct (* {{{ *)
let perform { r_where; r_doc; r_what; r_for } =
VCS.restore r_doc;
VCS.print ();
- Reach.known_state ~cache:`No r_where;
+ Reach.known_state ~doc:dummy_doc (* XXX should be r_doc *) ~cache:`No r_where;
(* STATE *)
let st = Vernacstate.freeze_interp_state `No in
try
@@ -2103,7 +2126,8 @@ end (* }}} *)
and Reach : sig
val known_state :
- ?redefine_qed:bool -> cache:Summary.marshallable -> Stateid.t -> unit
+ doc:doc -> ?redefine_qed:bool -> cache:Summary.marshallable ->
+ Stateid.t -> unit
end = struct (* {{{ *)
@@ -2119,12 +2143,6 @@ let delegate name =
|| VCS.is_vio_doc ()
|| !cur_opt.async_proofs_full
-let warn_deprecated_nested_proofs =
- CWarnings.create ~name:"deprecated-nested-proofs" ~category:"deprecated"
- (fun () ->
- strbrk ("Nested proofs are deprecated and will "^
- "stop working in a future Coq version"))
-
let collect_proof keep cur hd brkind id =
stm_prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id);
let no_name = "" in
@@ -2133,7 +2151,7 @@ let collect_proof keep cur hd brkind id =
| id :: _ -> Names.Id.to_string id in
let loc = (snd cur).loc in
let is_defined_expr = function
- | VernacEndProof (Proved (Transparent,_)) -> true
+ | VernacEndProof (Proved (Proof_global.Transparent,_)) -> true
| _ -> false in
let is_defined = function
| _, { expr = e } -> is_defined_expr (Vernacprop.under_control e)
@@ -2206,8 +2224,7 @@ let collect_proof keep cur hd brkind id =
assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
let name = name ids in
`MaybeASync (parent last, accn, name, delegate name)
- | `Sideff _ ->
- warn_deprecated_nested_proofs ();
+ | `Sideff (CherryPickEnv,_) ->
`Sync (no_name,`NestedProof)
| _ -> `Sync (no_name,`Unknown) in
let make_sync why = function
@@ -2261,7 +2278,7 @@ let log_processing_sync id name reason = log_string Printf.(sprintf
let wall_clock_last_fork = ref 0.0
-let known_state ?(redefine_qed=false) ~cache id =
+let known_state ~doc ?(redefine_qed=false) ~cache id =
let error_absorbing_tactic id blockname exn =
(* We keep the static/dynamic part of block detection separate, since
@@ -2294,7 +2311,7 @@ let known_state ?(redefine_qed=false) ~cache id =
Proof_global.unfreeze proof;
Proof_global.with_current_proof (fun _ p ->
feedback ~id:id Feedback.AddedAxiom;
- fst (Pfedit.solve Vernacexpr.SelectAll None tac p), ());
+ fst (Pfedit.solve Goal_select.SelectAll None tac p), ());
(* STATE SPEC:
* - start: Modifies the input state adding a proof.
* - end : maybe after recovery command.
@@ -2356,7 +2373,7 @@ let known_state ?(redefine_qed=false) ~cache id =
and reach ?safe_id ?(redefine_qed=false) ?(cache=cache) id =
stm_prerr_endline (fun () -> "reaching: " ^ Stateid.to_string id);
if not redefine_qed && State.is_cached ~cache id then begin
- Hooks.(call state_computed id ~in_cache:true);
+ Hooks.(call state_computed ~doc id ~in_cache:true);
stm_prerr_endline (fun () -> "reached (cache)");
State.install_cached id
end else
@@ -2437,7 +2454,7 @@ let known_state ?(redefine_qed=false) ~cache id =
^" proof. Reprocess the command declaring "
^"the proof's statement to avoid that."));
let fp, cancel =
- Slaves.build_proof
+ Slaves.build_proof ~doc
?loc ~drop_pt ~exn_info ~block_start ~block_stop ~name in
Future.replace ofp fp;
qed.fproof <- Some (fp, cancel);
@@ -2449,10 +2466,10 @@ let known_state ?(redefine_qed=false) ~cache id =
reach ~cache:`Shallow block_start;
let fp, cancel =
if delegate then
- Slaves.build_proof
+ Slaves.build_proof ~doc
?loc ~drop_pt ~exn_info ~block_start ~block_stop ~name
else
- ProofTask.build_proof_here ?loc
+ ProofTask.build_proof_here ~doc ?loc
~drop_pt exn_info block_stop, ref false
in
qed.fproof <- Some (fp, cancel);
@@ -2522,7 +2539,7 @@ let known_state ?(redefine_qed=false) ~cache id =
let cache_step =
if !cur_opt.async_proofs_cache = Some Force then `Yes
else cache_step in
- State.define ?safe_id
+ 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
reach ~redefine_qed id
@@ -2571,8 +2588,8 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } =
let load_objs libs =
let rq_file (dir, from, exp) =
- let mp = CAst.make @@ Libnames.(Qualid (qualid_of_string dir)) in
- let mfrom = Option.map (fun fr -> CAst.make @@ Libnames.(Qualid (qualid_of_string fr))) from in
+ let mp = Libnames.qualid_of_string dir in
+ let mfrom = Option.map Libnames.qualid_of_string from in
Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in
List.(iter rq_file (rev libs))
in
@@ -2611,7 +2628,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 ~cache:`Yes ~redefine:true (fun () -> ()) Stateid.initial;
+ State.define ~doc ~cache:`Yes ~redefine:true (fun () -> ()) Stateid.initial;
Backtrack.record ();
Slaves.init ();
if async_proofs_is_master !cur_opt then begin
@@ -2632,7 +2649,7 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } =
let observe ~doc id =
let vcs = VCS.backup () in
try
- Reach.known_state ~cache:(VCS.is_interactive ()) id;
+ Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id;
VCS.print ();
doc
with e ->
@@ -2725,7 +2742,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 = Reach.known_state ~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:`No qed_id in
VCS.checkout VCS.Branch.master;
`Unfocus qed_id
| { VCS.kind = `Master } ->
@@ -2734,7 +2751,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 +2774,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 +2794,15 @@ 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 allow_nested_proofs = ref false
+let _ = Goptions.declare_bool_option
+ { Goptions.optdepr = false;
+ Goptions.optname = "Nested Proofs Allowed";
+ Goptions.optkey = Vernac_classifier.stm_allow_nested_proofs_option_name;
+ Goptions.optread = (fun () -> !allow_nested_proofs);
+ Goptions.optwrite = (fun b -> allow_nested_proofs := b) }
-let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
+let process_transaction ~doc ?(newtip=Stateid.fresh ())
({ verbose; loc; expr } as x) c =
stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x);
let vcs = VCS.backup () in
@@ -2802,23 +2815,11 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
match c with
(* 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
+ let id, w = Backtrack.undo_vernac_classifier expr ~doc in
+ 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,11 +2831,17 @@ 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 ->
+
+ if not !allow_nested_proofs && VCS.proof_nesting () > 0 then
+ "Nested proofs are not allowed unless you turn option Nested Proofs Allowed on."
+ |> Pp.str
+ |> (fun s -> (UserError (None, s), Exninfo.null))
+ |> State.exn_on ~valid:Stateid.dummy Stateid.dummy
+ |> Exninfo.iraise
+ else
+
let id = VCS.new_node ~id:newtip () in
let bname = VCS.mk_branch_name x in
VCS.checkout VCS.Branch.master;
@@ -2885,12 +2892,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc);
rc
- (* Side effect in a (still open) proof is replayed 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 id = VCS.new_node ~id:newtip () in
begin match (VCS.get_branch head).VCS.kind with
@@ -2914,11 +2916,11 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
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 = Reach.known_state ~cache:`Yes head_id in (* ensure it is ok *)
+ let _st : unit = Reach.known_state ~doc ~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
- let _st' = Reach.known_state ~cache:(VCS.is_interactive ()) mid in
+ let _st' : unit = Reach.known_state ~doc ~cache:(VCS.is_interactive ()) mid in
let st = Vernacstate.freeze_interp_state `No in
ignore(stm_vernac_interp id st x);
(* Vernac x may or may not start a proof *)
@@ -2944,7 +2946,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
end;
VCS.checkout_shallowest_proof_branch ();
end in
- State.define ~safe_id:head_id ~cache:`Yes step id;
+ State.define ~doc ~safe_id:head_id ~cache:`Yes step id;
Backtrack.record (); `Ok
| VtUnknown, VtLater ->
@@ -3004,7 +3006,7 @@ let parse_sentence ~doc sid pa =
str "All is good if not parsing changes occur between the two states, however if they do, a problem might occur.");
Flags.with_option Flags.we_are_parsing (fun () ->
try
- match Pcoq.Gram.entry_parse Pcoq.main_entry pa with
+ match Pcoq.Entry.parse Pvernac.main_entry pa with
| None -> raise End_of_input
| Some (loc, cmd) -> CAst.make ~loc cmd
with e when CErrors.noncritical e ->
@@ -3058,7 +3060,7 @@ let add ~doc ~ontop ?newtip verb { CAst.loc; v=ast } =
(* XXX: Classifiy vernac should be moved inside process transaction *)
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
+ match process_transaction ~doc ?newtip aast clas with
| `Ok -> doc, VCS.cur_tip (), `NewTip
| `Unfocus qed_id -> doc, qed_id, `Unfocus (VCS.cur_tip ())
@@ -3073,18 +3075,14 @@ 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 ~cache:`Yes at;
+ else Reach.known_state ~doc ~cache:`Yes at;
try
while true do
let { CAst.loc; v=ast } = parse_sentence ~doc at s in
let indentation, strlen = compute_indentation ?loc at in
- 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 -> ()
@@ -3139,7 +3137,7 @@ let edit_at ~doc 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:(VCS.is_interactive ()) id;
+ Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id;
VCS.checkout_shallowest_proof_branch ();
`Focus { stop = qed_id; start = master_id; tip } in
let no_edit = function
@@ -3162,7 +3160,7 @@ let edit_at ~doc id =
VCS.gc ();
VCS.print ();
if not !cur_opt.async_proofs_full then
- Reach.known_state ~cache:(VCS.is_interactive ()) id;
+ Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id;
VCS.checkout_shallowest_proof_branch ();
`NewTip in
try
@@ -3191,7 +3189,7 @@ let edit_at ~doc id =
| true, None, _ ->
if on_cur_branch id then begin
VCS.reset_branch (VCS.current_branch ()) id;
- Reach.known_state ~cache:(VCS.is_interactive ()) id;
+ Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id;
VCS.checkout_shallowest_proof_branch ();
`NewTip
end else if is_ancestor_of_cur_branch id then begin
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-03 00:44:07 +0000