aboutsummaryrefslogtreecommitdiff
path: root/stm
diff options
context:
space:
mode:
Diffstat (limited to 'stm')
-rw-r--r--stm/asyncTaskQueue.ml41
-rw-r--r--stm/lemmas.ml555
-rw-r--r--stm/lemmas.mli69
-rw-r--r--stm/proofworkertop.ml6
-rw-r--r--stm/queryworkertop.ml6
-rw-r--r--stm/spawned.ml4
-rw-r--r--stm/stm.ml995
-rw-r--r--stm/stm.mli69
-rw-r--r--stm/stm.mllib2
-rw-r--r--stm/tQueue.ml2
-rw-r--r--stm/tacworkertop.ml6
-rw-r--r--stm/vcs.ml4
-rw-r--r--stm/vernac_classifier.ml42
-rw-r--r--stm/vio_checking.ml6
-rw-r--r--stm/workerLoop.ml19
-rw-r--r--stm/workerLoop.mli9
16 files changed, 579 insertions, 1256 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 0c28e6318e..25f9d7c187 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -10,9 +10,9 @@ open CErrors
open Pp
open Util
-let pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr
+let stm_pr_err pp = Format.eprintf "%s] @[%a@]%!\n" (System.process_id ()) Pp.pp_with pp
-let prerr_endline s = if !Flags.debug then begin pr_err s end else ()
+let stm_prerr_endline s = if !Flags.debug then begin stm_pr_err (str s) end else ()
type 'a worker_status = [ `Fresh | `Old of 'a ]
@@ -105,7 +105,7 @@ module Make(T : Task) = struct
let report_status ?(id = !Flags.async_proofs_worker_id) s =
let open Feedback in
- feedback ~id:(State Stateid.initial) (WorkerStatus(id, s))
+ feedback ~id:Stateid.initial (WorkerStatus(id, s))
module Worker = Spawn.Sync(struct end)
@@ -147,23 +147,23 @@ module Make(T : Task) = struct
let stop_waiting = ref false in
let expiration_date = ref (ref false) in
let pick_task () =
- prerr_endline "waiting for a task";
+ stm_prerr_endline "waiting for a task";
let pick age (t, c) = not !c && T.task_match age t in
let task, task_expiration =
TQueue.pop ~picky:(pick !worker_age) ~destroy:stop_waiting queue in
expiration_date := task_expiration;
last_task := Some task;
- prerr_endline ("got task: "^T.name_of_task task);
+ stm_prerr_endline ("got task: " ^ T.name_of_task task);
task in
let add_tasks l =
List.iter (fun t -> TQueue.push queue (t,!expiration_date)) l in
let get_exec_token () =
ignore(CoqworkmgrApi.get 1);
got_token := true;
- prerr_endline ("got execution token") in
+ stm_prerr_endline ("got execution token") in
let kill proc =
Worker.kill proc;
- prerr_endline ("Worker exited: " ^
+ stm_prerr_endline ("Worker exited: " ^
match Worker.wait proc with
| Unix.WEXITED 0x400 -> "exit code unavailable"
| Unix.WEXITED i -> Printf.sprintf "exit(%d)" i
@@ -196,7 +196,7 @@ module Make(T : Task) = struct
report_status ~id "Idle";
let task = pick_task () in
match T.request_of_task !worker_age task with
- | None -> prerr_endline ("Task expired: " ^ T.name_of_task task)
+ | None -> stm_prerr_endline ("Task expired: " ^ T.name_of_task task)
| Some req ->
try
get_exec_token ();
@@ -222,8 +222,7 @@ module Make(T : Task) = struct
raise e (* we pass the exception to the external handler *)
| MarshalError s -> T.on_marshal_error s task; raise Die
| e ->
- pr_err ("Uncaught exception in worker manager: "^
- string_of_ppcmds (print e));
+ stm_pr_err Pp.(seq [str "Uncaught exception in worker manager: "; print e]);
flush_all (); raise Die
done with
| (Die | TQueue.BeingDestroyed) ->
@@ -261,7 +260,7 @@ module Make(T : Task) = struct
let broadcast { queue } = TQueue.broadcast queue
let enqueue_task { queue; active } (t, _ as item) =
- prerr_endline ("Enqueue task "^T.name_of_task t);
+ stm_prerr_endline ("Enqueue task "^T.name_of_task t);
TQueue.push queue item
let cancel_worker { active } n = Pool.cancel n active
@@ -298,26 +297,18 @@ module Make(T : Task) = struct
let slave_handshake () =
Pool.worker_handshake (Option.get !slave_ic) (Option.get !slave_oc)
- let pp_pid pp =
- (* Breaking all abstraction barriers... very nice *)
- let get_xml pp = match Richpp.repr pp with
- | Xml_datatype.Element("_", [], xml) -> xml
- | _ -> assert false in
- Richpp.richpp_of_xml (Xml_datatype.Element("_", [],
- get_xml (Richpp.richpp_of_pp Pp.(str (System.process_id ()^ " "))) @
- get_xml pp))
+ let pp_pid pp = Pp.(str (System.process_id () ^ " ") ++ pp)
let debug_with_pid = Feedback.(function
| { contents = Message(Debug, loc, pp) } as fb ->
- { fb with contents = Message(Debug,loc,pp_pid pp) }
+ { fb with contents = Message(Debug,loc, pp_pid pp) }
| x -> x)
let main_loop () =
(* We pass feedback to master *)
let slave_feeder oc fb =
Marshal.to_channel oc (RespFeedback (debug_with_pid fb)) []; flush oc in
- Feedback.add_feeder (fun x -> slave_feeder (Option.get !slave_oc) x);
- Feedback.set_logger Feedback.feedback_logger;
+ ignore (Feedback.add_feeder (fun x -> slave_feeder (Option.get !slave_oc) x));
(* We ask master to allocate universe identifiers *)
Universes.set_remote_new_univ_level (bufferize (fun () ->
marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel;
@@ -337,11 +328,11 @@ module Make(T : Task) = struct
CEphemeron.clear ()
with
| MarshalError s ->
- pr_err ("Fatal marshal error: " ^ s); flush_all (); exit 2
+ stm_pr_err Pp.(prlist str ["Fatal marshal error: "; s]); flush_all (); exit 2
| End_of_file ->
- prerr_endline "connection lost"; flush_all (); exit 2
+ stm_prerr_endline "connection lost"; flush_all (); exit 2
| e ->
- pr_err ("Slave: critical exception: " ^ Pp.string_of_ppcmds (print e));
+ stm_pr_err Pp.(seq [str "Slave: critical exception: "; print e]);
flush_all (); exit 1
done
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
deleted file mode 100644
index f667550b95..0000000000
--- a/stm/lemmas.ml
+++ /dev/null
@@ -1,555 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(* Created by Hugo Herbelin from contents related to lemma proofs in
- file command.ml, Aug 2009 *)
-
-open CErrors
-open Util
-open Flags
-open Pp
-open Names
-open Term
-open Declarations
-open Declareops
-open Entries
-open Environ
-open Nameops
-open Globnames
-open Decls
-open Decl_kinds
-open Declare
-open Pretyping
-open Termops
-open Namegen
-open Reductionops
-open Constrexpr
-open Constrintern
-open Impargs
-open Context.Rel.Declaration
-
-type 'a declaration_hook = Decl_kinds.locality -> Globnames.global_reference -> 'a
-let mk_hook hook = hook
-let call_hook fix_exn hook l c =
- try hook l c
- with e when CErrors.noncritical e ->
- let e = CErrors.push e in
- iraise (fix_exn e)
-
-(* Support for mutually proved theorems *)
-
-let retrieve_first_recthm = function
- | VarRef id ->
- let open Context.Named.Declaration in
- (get_value (Global.lookup_named id),variable_opacity id)
- | ConstRef cst ->
- let cb = Global.lookup_constant cst in
- (Global.body_of_constant_body cb, is_opaque cb)
- | _ -> assert false
-
-let adjust_guardness_conditions const = function
- | [] -> const (* Not a recursive statement *)
- | possible_indexes ->
- (* Try all combinations... not optimal *)
- let env = Global.env() in
- { const with const_entry_body =
- Future.chain ~greedy:true ~pure:true const.const_entry_body
- (fun ((body, ctx), eff) ->
- match kind_of_term body with
- | Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->
-(* let possible_indexes =
- List.map2 (fun i c -> match i with Some i -> i | None ->
- List.interval 0 (List.length ((lam_assum c))))
- lemma_guard (Array.to_list fixdefs) in
-*)
- let add c cb e =
- let exists c e =
- try ignore(Environ.lookup_constant c e); true
- with Not_found -> false in
- if exists c e then e else Environ.add_constant c cb e in
- let env = List.fold_left (fun env { eff } ->
- match eff with
- | SEsubproof (c, cb,_) -> add c cb env
- | SEscheme (l,_) ->
- List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l)
- env (Safe_typing.side_effects_of_private_constants eff) in
- let indexes =
- search_guard Loc.ghost env
- possible_indexes fixdecls in
- (mkFix ((indexes,0),fixdecls), ctx), eff
- | _ -> (body, ctx), eff) }
-
-let find_mutually_recursive_statements thms =
- let n = List.length thms in
- let inds = List.map (fun (id,(t,impls,annot)) ->
- let (hyps,ccl) = decompose_prod_assum t in
- let x = (id,(t,impls)) in
- match annot with
- (* Explicit fixpoint decreasing argument is given *)
- | Some (Some (_,id),CStructRec) ->
- let i,b,typ = lookup_rel_id id hyps in
- (match kind_of_term t with
- | Ind ((kn,_ as ind), u) when
- let mind = Global.lookup_mind kn in
- mind.mind_finite == Decl_kinds.Finite && Option.is_empty b ->
- [ind,x,i],[]
- | _ ->
- error "Decreasing argument is not an inductive assumption.")
- (* Unsupported cases *)
- | Some (_,(CWfRec _|CMeasureRec _)) ->
- error "Only structural decreasing is supported for mutual statements."
- (* Cofixpoint or fixpoint w/o explicit decreasing argument *)
- | None | Some (None, CStructRec) ->
- let whnf_hyp_hds = map_rel_context_in_env
- (fun env c -> fst (whd_all_stack env Evd.empty c))
- (Global.env()) hyps in
- let ind_hyps =
- List.flatten (List.map_i (fun i decl ->
- let t = get_type decl in
- match kind_of_term t with
- | Ind ((kn,_ as ind),u) when
- let mind = Global.lookup_mind kn in
- mind.mind_finite <> Decl_kinds.CoFinite && is_local_assum decl ->
- [ind,x,i]
- | _ ->
- []) 0 (List.rev whnf_hyp_hds)) in
- let ind_ccl =
- let cclenv = push_rel_context hyps (Global.env()) in
- let whnf_ccl,_ = whd_all_stack cclenv Evd.empty ccl in
- match kind_of_term whnf_ccl with
- | Ind ((kn,_ as ind),u) when
- let mind = Global.lookup_mind kn in
- Int.equal mind.mind_ntypes n && mind.mind_finite == Decl_kinds.CoFinite ->
- [ind,x,0]
- | _ ->
- [] in
- ind_hyps,ind_ccl) thms in
- let inds_hyps,ind_ccls = List.split inds in
- let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> eq_mind kn kn' in
- (* Check if all conclusions are coinductive in the same type *)
- (* (degenerated cartesian product since there is at most one coind ccl) *)
- let same_indccl =
- List.cartesians_filter (fun hyp oks ->
- if List.for_all (of_same_mutind hyp) oks
- then Some (hyp::oks) else None) [] ind_ccls in
- let ordered_same_indccl =
- List.filter (List.for_all_i (fun i ((kn,j),_,_) -> Int.equal i j) 0) same_indccl in
- (* Check if some hypotheses are inductive in the same type *)
- let common_same_indhyp =
- List.cartesians_filter (fun hyp oks ->
- if List.for_all (of_same_mutind hyp) oks
- then Some (hyp::oks) else None) [] inds_hyps in
- let ordered_inds,finite,guard =
- match ordered_same_indccl, common_same_indhyp with
- | indccl::rest, _ ->
- assert (List.is_empty rest);
- (* One occ. of common coind ccls and no common inductive hyps *)
- if not (List.is_empty common_same_indhyp) then
- if_verbose Feedback.msg_info (str "Assuming mutual coinductive statements.");
- flush_all ();
- indccl, true, []
- | [], _::_ ->
- let () = match same_indccl with
- | ind :: _ ->
- if List.distinct_f ind_ord (List.map pi1 ind)
- then
- if_verbose Feedback.msg_info
- (strbrk
- ("Coinductive statements do not follow the order of "^
- "definition, assuming the proof to be by induction."));
- flush_all ()
- | _ -> ()
- in
- let possible_guards = List.map (List.map pi3) inds_hyps in
- (* assume the largest indices as possible *)
- List.last common_same_indhyp, false, possible_guards
- | _, [] ->
- error
- ("Cannot find common (mutual) inductive premises or coinductive" ^
- " conclusions in the statements.")
- in
- (finite,guard,None), ordered_inds
-
-let look_for_possibly_mutual_statements = function
- | [id,(t,impls,None)] ->
- (* One non recursively proved theorem *)
- None,[id,(t,impls)],None
- | _::_ as thms ->
- (* More than one statement and/or an explicit decreasing mark: *)
- (* we look for a common inductive hyp or a common coinductive conclusion *)
- let recguard,ordered_inds = find_mutually_recursive_statements thms in
- let thms = List.map pi2 ordered_inds in
- Some recguard,thms, Some (List.map (fun (_,_,i) -> succ i) ordered_inds)
- | [] -> anomaly (Pp.str "Empty list of theorems.")
-
-(* Saving a goal *)
-
-let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook =
- let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in
- try
- let const = adjust_guardness_conditions const do_guard in
- let k = Kindops.logical_kind_of_goal_kind kind in
- let l,r = match locality with
- | Discharge when Lib.sections_are_opened () ->
- let c = SectionLocalDef const in
- let _ = declare_variable id (Lib.cwd(), c, k) in
- (Local, VarRef id)
- | Local | Global | Discharge ->
- let local = match locality with
- | Local | Discharge -> true
- | Global -> false
- in
- let kn =
- declare_constant ?export_seff id ~local (DefinitionEntry const, k) in
- (locality, ConstRef kn) in
- definition_message id;
- Option.iter (Universes.register_universe_binders r) pl;
- call_hook (fun exn -> exn) hook l r
- with e when CErrors.noncritical e ->
- let e = CErrors.push e in
- iraise (fix_exn e)
-
-let default_thm_id = Id.of_string "Unnamed_thm"
-
-let compute_proof_name locality = function
- | Some ((loc,id),pl) ->
- (* We check existence here: it's a bit late at Qed time *)
- if Nametab.exists_cci (Lib.make_path id) || is_section_variable id ||
- locality == Global && Nametab.exists_cci (Lib.make_path_except_section id)
- then
- user_err_loc (loc,"",pr_id id ++ str " already exists.");
- id, pl
- | None ->
- next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()), None
-
-let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,(_,imps))) =
- let t_i = norm t_i in
- match body with
- | None ->
- (match locality with
- | Discharge ->
- let impl = false in (* copy values from Vernacentries *)
- let k = IsAssumption Conjectural in
- let c = SectionLocalAssum ((t_i,ctx),p,impl) in
- let _ = declare_variable id (Lib.cwd(),c,k) in
- (Discharge, VarRef id,imps)
- | Local | Global ->
- let k = IsAssumption Conjectural in
- let local = match locality with
- | Local -> true
- | Global -> false
- | Discharge -> assert false
- in
- let ctx = Univ.ContextSet.to_context ctx in
- let decl = (ParameterEntry (None,p,(t_i,ctx),None), k) in
- let kn = declare_constant id ~local decl in
- (locality,ConstRef kn,imps))
- | Some body ->
- let body = norm body in
- let k = Kindops.logical_kind_of_goal_kind kind in
- let rec body_i t = match kind_of_term t with
- | Fix ((nv,0),decls) -> mkFix ((nv,i),decls)
- | CoFix (0,decls) -> mkCoFix (i,decls)
- | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, body_i t2)
- | Lambda(na,ty,t) -> mkLambda(na,ty,body_i t)
- | App (t, args) -> mkApp (body_i t, args)
- | _ -> anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr body) in
- let body_i = body_i body in
- match locality with
- | Discharge ->
- let const = definition_entry ~types:t_i ~opaque:opaq ~poly:p
- ~univs:(Univ.ContextSet.to_context ctx) body_i in
- let c = SectionLocalDef const in
- let _ = declare_variable id (Lib.cwd(), c, k) in
- (Discharge,VarRef id,imps)
- | Local | Global ->
- let ctx = Univ.ContextSet.to_context ctx in
- let local = match locality with
- | Local -> true
- | Global -> false
- | Discharge -> assert false
- in
- let const =
- Declare.definition_entry ~types:t_i ~poly:p ~univs:ctx ~opaque:opaq body_i
- in
- let kn = declare_constant id ~local (DefinitionEntry const, k) in
- (locality,ConstRef kn,imps)
-
-let save_hook = ref ignore
-let set_save_hook f = save_hook := f
-
-let save_named ?export_seff proof =
- let id,const,(cstrs,pl),do_guard,persistence,hook = proof in
- save ?export_seff id const cstrs pl do_guard persistence hook
-
-let check_anonymity id save_ident =
- if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then
- error "This command can only be used for unnamed theorem."
-
-let save_anonymous ?export_seff proof save_ident =
- let id,const,(cstrs,pl),do_guard,persistence,hook = proof in
- check_anonymity id save_ident;
- save ?export_seff save_ident const cstrs pl do_guard persistence hook
-
-let save_anonymous_with_strength ?export_seff proof kind save_ident =
- let id,const,(cstrs,pl),do_guard,_,hook = proof in
- check_anonymity id save_ident;
- (* we consider that non opaque behaves as local for discharge *)
- save ?export_seff save_ident const cstrs pl do_guard
- (Global, const.const_entry_polymorphic, Proof kind) hook
-
-(* Admitted *)
-
-let warn_let_as_axiom =
- CWarnings.create ~name:"let-as-axiom" ~category:"vernacular"
- (fun id -> strbrk "Let definition" ++ spc () ++ pr_id id ++
- spc () ++ strbrk "declared as an axiom.")
-
-let admit (id,k,e) pl hook () =
- let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in
- let () = match k with
- | Global, _, _ -> ()
- | Local, _, _ | Discharge, _, _ -> warn_let_as_axiom id
- in
- let () = assumption_message id in
- Option.iter (Universes.register_universe_binders (ConstRef kn)) pl;
- call_hook (fun exn -> exn) hook Global (ConstRef kn)
-
-(* Starting a goal *)
-
-let start_hook = ref ignore
-let set_start_hook = (:=) start_hook
-
-
-let get_proof proof do_guard hook opacity =
- let (id,(const,univs,persistence)) =
- Pfedit.cook_this_proof proof
- in
- id,{const with const_entry_opaque = opacity},univs,do_guard,persistence,hook
-
-let check_exist =
- List.iter (fun (loc,id) ->
- if not (Nametab.exists_cci (Lib.make_path id)) then
- user_err_loc (loc,"",pr_id id ++ str " does not exist.")
- )
-
-let universe_proof_terminator compute_guard hook =
- let open Proof_global in
- make_terminator begin function
- | Admitted (id,k,pe,(ctx,pl)) ->
- admit (id,k,pe) pl (hook (Some ctx)) ();
- Feedback.feedback Feedback.AddedAxiom
- | Proved (opaque,idopt,proof) ->
- let is_opaque, export_seff, exports = match opaque with
- | Vernacexpr.Transparent -> false, true, []
- | Vernacexpr.Opaque None -> true, false, []
- | Vernacexpr.Opaque (Some l) -> true, true, l in
- let proof = get_proof proof compute_guard
- (hook (Some (fst proof.Proof_global.universes))) is_opaque in
- begin match idopt with
- | None -> save_named ~export_seff proof
- | Some ((_,id),None) -> save_anonymous ~export_seff proof id
- | Some ((_,id),Some kind) ->
- save_anonymous_with_strength ~export_seff proof kind id
- end;
- check_exist exports
- end
-
-let standard_proof_terminator compute_guard hook =
- universe_proof_terminator compute_guard (fun _ -> hook)
-
-let start_proof id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook =
- let terminator = match terminator with
- | None -> standard_proof_terminator compute_guard hook
- | Some terminator -> terminator compute_guard hook
- in
- let sign =
- match sign with
- | Some sign -> sign
- | None -> initialize_named_context_for_proof ()
- in
- !start_hook c;
- Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator
-
-let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook =
- let terminator = match terminator with
- | None -> universe_proof_terminator compute_guard hook
- | Some terminator -> terminator compute_guard hook
- in
- let sign =
- match sign with
- | Some sign -> sign
- | None -> initialize_named_context_for_proof ()
- in
- !start_hook c;
- Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator
-
-let rec_tac_initializer finite guard thms snl =
- if finite then
- match List.map (fun ((id,_),(t,_)) -> (id,t)) thms with
- | (id,_)::l -> Tactics.mutual_cofix id l 0
- | _ -> assert false
- else
- (* nl is dummy: it will be recomputed at Qed-time *)
- let nl = match snl with
- | None -> List.map succ (List.map List.last guard)
- | Some nl -> nl
- in match List.map2 (fun ((id,_),(t,_)) n -> (id,n,t)) thms nl with
- | (id,n,_)::l -> Tactics.mutual_fix id n l 0
- | _ -> assert false
-
-let start_proof_with_initialization kind ctx recguard thms snl hook =
- let intro_tac (_, (_, (ids, _))) =
- Tacticals.New.tclMAP (function
- | Name id -> Tactics.intro_mustbe_force id
- | Anonymous -> Tactics.intro) (List.rev ids) in
- let init_tac,guard = match recguard with
- | Some (finite,guard,init_tac) ->
- let rec_tac = rec_tac_initializer finite guard thms snl in
- Some (match init_tac with
- | None ->
- if Flags.is_auto_intros () then
- Tacticals.New.tclTHENS rec_tac (List.map intro_tac thms)
- else
- rec_tac
- | Some tacl ->
- Tacticals.New.tclTHENS rec_tac
- (if Flags.is_auto_intros () then
- List.map2 (fun tac thm -> Tacticals.New.tclTHEN tac (intro_tac thm)) tacl thms
- else
- tacl)),guard
- | None ->
- let () = match thms with [_] -> () | _ -> assert false in
- (if Flags.is_auto_intros () then Some (intro_tac (List.hd thms)) else None), [] in
- match thms with
- | [] -> anomaly (Pp.str "No proof to start")
- | ((id,pl),(t,(_,imps)))::other_thms ->
- let hook ctx strength ref =
- let ctx = match ctx with
- | None -> Evd.empty_evar_universe_context
- | Some ctx -> ctx
- in
- let other_thms_data =
- if List.is_empty other_thms then [] else
- (* there are several theorems defined mutually *)
- let body,opaq = retrieve_first_recthm ref in
- let subst = Evd.evar_universe_context_subst ctx in
- let norm c = Universes.subst_opt_univs_constr subst c in
- let ctx = UState.context_set (*FIXME*) ctx in
- let body = Option.map norm body in
- List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in
- let thms_data = (strength,ref,imps)::other_thms_data in
- List.iter (fun (strength,ref,imps) ->
- maybe_declare_manual_implicits false ref imps;
- call_hook (fun exn -> exn) hook strength ref) thms_data in
- start_proof_univs id ?pl kind ctx t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard
-
-let start_proof_com ?inference_hook kind thms hook =
- let env0 = Global.env () in
- let levels = Option.map snd (fst (List.hd thms)) in
- let evdref = ref (match levels with
- | None -> Evd.from_env env0
- | Some l -> Evd.from_ctx (Evd.make_evar_universe_context env0 l))
- in
- let thms = List.map (fun (sopt,(bl,t,guard)) ->
- let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in
- let t', imps' = interp_type_evars_impls ~impls env evdref t in
- let flags = all_and_fail_flags in
- let flags = { flags with use_hook = inference_hook } in
- evdref := solve_remaining_evars flags env !evdref (Evd.empty,!evdref);
- let ids = List.map get_name ctx in
- (compute_proof_name (pi1 kind) sopt,
- (nf_evar !evdref (it_mkProd_or_LetIn t' ctx),
- (ids, imps @ lift_implicits (List.length ids) imps'),
- guard)))
- thms in
- let recguard,thms,snl = look_for_possibly_mutual_statements thms in
- let evd, nf = Evarutil.nf_evars_and_universes !evdref in
- let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in
- let () =
- match levels with
- | None -> ()
- | Some l -> ignore (Evd.universe_context evd ?names:l)
- in
- let evd =
- if pi2 kind then evd
- else (* We fix the variables to ensure they won't be lowered to Set *)
- Evd.fix_undefined_variables evd
- in
- start_proof_with_initialization kind evd recguard thms snl hook
-
-
-(* Saving a proof *)
-
-let keep_admitted_vars = ref true
-
-let _ =
- let open Goptions in
- declare_bool_option
- { optsync = true;
- optdepr = false;
- optname = "keep section variables in admitted proofs";
- optkey = ["Keep"; "Admitted"; "Variables"];
- optread = (fun () -> !keep_admitted_vars);
- optwrite = (fun b -> keep_admitted_vars := b) }
-
-let save_proof ?proof = function
- | Vernacexpr.Admitted ->
- let pe =
- let open Proof_global in
- match proof with
- | Some ({ id; entries; persistence = k; universes }, _) ->
- if List.length entries <> 1 then
- error "Admitted does not support multiple statements";
- let { const_entry_secctx; const_entry_type } = List.hd entries in
- if const_entry_type = None then
- error "Admitted requires an explicit statement";
- let typ = Option.get const_entry_type in
- let ctx = Evd.evar_context_universe_context (fst universes) in
- let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in
- Admitted(id, k, (sec_vars, pi2 k, (typ, ctx), None), universes)
- | None ->
- let pftree = Pfedit.get_pftreestate () in
- let id, k, typ = Pfedit.current_proof_statement () in
- let universes = Proof.initial_euctx pftree in
- (* This will warn if the proof is complete *)
- let pproofs, _univs =
- Proof_global.return_proof ~allow_partial:true () in
- let sec_vars =
- if not !keep_admitted_vars then None
- else match Pfedit.get_used_variables(), pproofs with
- | Some _ as x, _ -> x
- | None, (pproof, _) :: _ ->
- let env = Global.env () in
- let ids_typ = Environ.global_vars_set env typ in
- let ids_def = Environ.global_vars_set env pproof in
- Some (Environ.keep_hyps env (Idset.union ids_typ ids_def))
- | _ -> None in
- let names = Pfedit.get_universe_binders () in
- let evd = Evd.from_ctx universes in
- let binders, ctx = Evd.universe_context ?names evd in
- Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None),
- (universes, Some binders))
- in
- Proof_global.apply_terminator (Proof_global.get_terminator ()) pe
- | Vernacexpr.Proved (is_opaque,idopt) ->
- let (proof_obj,terminator) =
- match proof with
- | None ->
- Proof_global.close_proof ~keep_body_ucst_separate:false (fun x -> x)
- | Some proof -> proof
- in
- (* if the proof is given explicitly, nothing has to be deleted *)
- if Option.is_empty proof then Pfedit.delete_current_proof ();
- Proof_global.(apply_terminator terminator (Proved (is_opaque,idopt,proof_obj)))
-
-(* Miscellaneous *)
-
-let get_current_context () =
- Pfedit.get_current_context ()
-
diff --git a/stm/lemmas.mli b/stm/lemmas.mli
deleted file mode 100644
index eae10d89fc..0000000000
--- a/stm/lemmas.mli
+++ /dev/null
@@ -1,69 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Names
-open Term
-open Decl_kinds
-open Pfedit
-
-type 'a declaration_hook
-val mk_hook :
- (Decl_kinds.locality -> Globnames.global_reference -> 'a) -> 'a declaration_hook
-
-val call_hook :
- Future.fix_exn -> 'a declaration_hook -> Decl_kinds.locality -> Globnames.global_reference -> 'a
-
-(** A hook start_proof calls on the type of the definition being started *)
-val set_start_hook : (types -> unit) -> unit
-
-val start_proof : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map ->
- ?terminator:(lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) ->
- ?sign:Environ.named_context_val -> types ->
- ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards ->
- unit declaration_hook -> unit
-
-val start_proof_univs : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map ->
- ?terminator:(lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> Proof_global.proof_terminator) ->
- ?sign:Environ.named_context_val -> types ->
- ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards ->
- (Evd.evar_universe_context option -> unit declaration_hook) -> unit
-
-val start_proof_com :
- ?inference_hook:Pretyping.inference_hook ->
- goal_kind -> Vernacexpr.proof_expr list ->
- unit declaration_hook -> unit
-
-val start_proof_with_initialization :
- goal_kind -> Evd.evar_map ->
- (bool * lemma_possible_guards * unit Proofview.tactic list option) option ->
- ((Id.t * universe_binders option) *
- (types * (Name.t list * Impargs.manual_explicitation list))) list
- -> int list option -> unit declaration_hook -> unit
-
-val universe_proof_terminator :
- Proof_global.lemma_possible_guards ->
- (Evd.evar_universe_context option -> unit declaration_hook) ->
- Proof_global.proof_terminator
-
-val standard_proof_terminator :
- Proof_global.lemma_possible_guards -> unit declaration_hook ->
- Proof_global.proof_terminator
-
-(** {6 ... } *)
-
-(** A hook the next three functions pass to cook_proof *)
-val set_save_hook : (Proof.proof -> unit) -> unit
-
-val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit
-
-
-(** [get_current_context ()] returns the evar context and env of the
- current open proof if any, otherwise returns the empty evar context
- and the current global env *)
-
-val get_current_context : unit -> Evd.evar_map * Environ.env
diff --git a/stm/proofworkertop.ml b/stm/proofworkertop.ml
index 3241a774c3..95012d984e 100644
--- a/stm/proofworkertop.ml
+++ b/stm/proofworkertop.ml
@@ -8,11 +8,7 @@
module W = AsyncTaskQueue.MakeWorker(Stm.ProofTask)
-let () = Coqtop.toploop_init := (fun args ->
- Flags.make_silent true;
- W.init_stdout ();
- CoqworkmgrApi.init !Flags.async_proofs_worker_priority;
- args)
+let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
let () = Coqtop.toploop_run := W.main_loop
diff --git a/stm/queryworkertop.ml b/stm/queryworkertop.ml
index 3d0249fd81..85f0e6bfc1 100644
--- a/stm/queryworkertop.ml
+++ b/stm/queryworkertop.ml
@@ -8,11 +8,7 @@
module W = AsyncTaskQueue.MakeWorker(Stm.QueryTask)
-let () = Coqtop.toploop_init := (fun args ->
- Flags.make_silent true;
- W.init_stdout ();
- CoqworkmgrApi.init !Flags.async_proofs_worker_priority;
- args)
+let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
let () = Coqtop.toploop_run := W.main_loop
diff --git a/stm/spawned.ml b/stm/spawned.ml
index 0db4c3b698..6ab096abf9 100644
--- a/stm/spawned.ml
+++ b/stm/spawned.ml
@@ -46,7 +46,7 @@ let control_channel = ref None
let channels = ref None
let init_channels () =
- if !channels <> None then CErrors.anomaly(Pp.str "init_channels called twice");
+ if !channels <> None then CErrors.anomaly(Pp.str "init_channels called twice.");
let () = match !main_channel with
| None -> ()
| Some (Socket(mh,mpr,mpw)) ->
@@ -65,7 +65,7 @@ let init_channels () =
| Some (Socket (ch, cpr, cpw)) ->
controller ch cpr cpw
| Some AnonPipe ->
- CErrors.anomaly (Pp.str "control channel cannot be a pipe")
+ CErrors.anomaly (Pp.str "control channel cannot be a pipe.")
let get_channels () =
match !channels with
diff --git a/stm/stm.ml b/stm/stm.ml
index 4e7f4b9247..fd3d418c10 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -6,33 +6,33 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-let pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr
+(* enable in case of stm problems *)
+(* let stm_debug () = !Flags.debug *)
+let stm_debug () = !Flags.stm_debug
-let prerr_endline s = if false then begin pr_err (s ()) end else ()
-let prerr_debug s = if !Flags.debug then begin pr_err (s ()) end else ()
+let stm_pr_err s = Format.eprintf "%s] %s\n%!" (System.process_id ()) s
+let stm_pp_err pp = Format.eprintf "%s] @[%a@]\n%!" (System.process_id ()) Pp.pp_with pp
-(* Opening ppvernac below aliases Richpp, see PR#185 *)
-let pp_to_richpp = Richpp.richpp_of_pp
-let str_to_richpp = Richpp.richpp_of_string
+let stm_prerr_endline s = if stm_debug () then begin stm_pr_err (s ()) end else ()
+let stm_pperr_endline s = if stm_debug () then begin stm_pp_err (s ()) end else ()
+
+let stm_prerr_debug s = if !Flags.debug then begin stm_pr_err (s ()) end else ()
-open Vernacexpr
-open CErrors
open Pp
-open Names
-open Util
-open Ppvernac
-open Vernac_classifier
+open CErrors
open Feedback
+open Vernacexpr
+open Vernac_classifier
-module Hooks = struct
+let execution_error ?loc state_id msg =
+ feedback ~id:state_id
+ (Message (Error, loc, msg))
-let process_error, process_error_hook = Hook.make ()
-let interp, interp_hook = Hook.make ()
-let with_fail, with_fail_hook = Hook.make ()
+module Hooks = struct
let state_computed, state_computed_hook = Hook.make
~default:(fun state_id ~in_cache ->
- feedback ~id:(State state_id) Processed) ()
+ feedback ~id:state_id Processed) ()
let state_ready, state_ready_hook = Hook.make
~default:(fun state_id -> ()) ()
@@ -44,20 +44,9 @@ let forward_feedback, forward_feedback_hook =
try Mutex.lock m; feedback ~id:id ~route contents; Mutex.unlock m
with e -> Mutex.unlock m; raise e) ()
-let parse_error, parse_error_hook = Hook.make
- ~default:(fun id loc msg ->
- feedback ~id (Message(Error, Some loc, pp_to_richpp msg))) ()
-
-let execution_error, execution_error_hook = Hook.make
- ~default:(fun state_id loc msg ->
- feedback ~id:(State state_id) (Message(Error, Some loc, pp_to_richpp msg))) ()
-
let unreachable_state, unreachable_state_hook = Hook.make
~default:(fun _ _ -> ()) ()
-let tactic_being_run, tactic_being_run_hook = Hook.make
- ~default:(fun _ -> ()) ()
-
include Hook
(* enables: Hooks.(call foo args) *)
@@ -69,7 +58,7 @@ let call_process_error_once =
match Exninfo.get info processed with
| Some _ -> ei
| None ->
- let e, info = call process_error ei in
+ let e, info = ExplainErr.process_vernac_interp_error ei in
let info = Exninfo.add info processed () in
e, info
@@ -77,21 +66,21 @@ end
(* During interactive use we cache more states so that Undoing is fast *)
let interactive () =
- if !Flags.ide_slave || !Flags.print_emacs || not !Flags.batch_mode then `Yes
+ if !Flags.ide_slave || not !Flags.batch_mode then `Yes
else `No
let async_proofs_workers_extra_env = ref [||]
type aast = {
verbose : bool;
- loc : Loc.t;
+ loc : Loc.t option;
indentation : int;
strlen : int;
mutable expr : vernac_expr; (* mutable: Proof using hinted by aux file *)
}
-let pr_ast { expr; indentation } = int indentation ++ str " " ++ pr_vernac expr
+let pr_ast { expr; indentation } = Pp.(int indentation ++ str " " ++ Ppvernac.pr_vernac expr)
-let default_proof_mode () = Proof_global.get_default_proof_mode_name ()
+let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"]
(* Commands piercing opaque *)
let may_pierce_opaque = function
@@ -105,63 +94,6 @@ let may_pierce_opaque = function
| { expr = VernacExtend (("ExtractionInductive",_), _) } -> true
| _ -> false
-(* Wrapper for Vernacentries.interp to set the feedback id *)
-let vernac_interp ?proof id ?route { verbose; loc; expr } =
- let rec internal_command = function
- | VernacResetName _ | VernacResetInitial | VernacBack _
- | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _
- | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true
- | VernacTime (_,e) | VernacTimeout (_,e) | VernacRedirect (_,(_,e)) -> internal_command e
- | _ -> false in
- if internal_command expr then begin
- prerr_endline (fun () -> "ignoring " ^ Pp.string_of_ppcmds(pr_vernac expr))
- end else begin
- set_id_for_feedback ?route (State id);
- Aux_file.record_in_aux_set_at loc;
- prerr_endline (fun () -> "interpreting " ^ Pp.string_of_ppcmds(pr_vernac expr));
- try Hooks.(call interp ?verbosely:(Some verbose) ?proof (loc, expr))
- with e ->
- let e = CErrors.push e in
- iraise Hooks.(call_process_error_once e)
- end
-
-(* Wrapper for Vernac.parse_sentence to set the feedback id *)
-let indentation_of_string s =
- let len = String.length s in
- let rec aux n i precise =
- if i >= len then 0, precise, len
- else
- match s.[i] with
- | ' ' | '\t' -> aux (succ n) (succ i) precise
- | '\n' | '\r' -> aux 0 (succ i) true
- | _ -> n, precise, len in
- aux 0 0 false
-
-let vernac_parse ?(indlen_prev=fun() -> 0) ?newtip ?route eid s =
- let feedback_id =
- if Option.is_empty newtip then Edit eid
- else State (Option.get newtip) in
- let indentation, precise, strlen = indentation_of_string s in
- let indentation =
- if precise then indentation else indlen_prev () + indentation in
- set_id_for_feedback ?route feedback_id;
- let pa = Pcoq.Gram.parsable (Stream.of_string s) in
- Flags.with_option Flags.we_are_parsing (fun () ->
- try
- match Pcoq.Gram.entry_parse Pcoq.main_entry pa with
- | None -> raise (Invalid_argument "vernac_parse")
- | Some (loc, ast) -> indentation, strlen, loc, ast
- with e when CErrors.noncritical e ->
- let (e, info) = CErrors.push e in
- let loc = Option.default Loc.ghost (Loc.get_loc info) in
- Hooks.(call parse_error feedback_id loc (iprint (e, info)));
- iraise (e, info))
- ()
-
-let pr_open_cur_subgoals () =
- try Printer.pr_open_subgoals ()
- with Proof_global.NoCurrentProof -> Pp.str ""
-
let update_global_env () =
if Proof_global.there_are_pending_proofs () then
Proof_global.update_global_env ()
@@ -181,13 +113,13 @@ type cmd_t = {
ctac : bool; (* is a tactic *)
ceff : bool; (* is a side-effecting command in the middle of a proof *)
cast : aast;
- cids : Id.t list;
+ cids : Names.Id.t list;
cblock : proof_block_name option;
cqueue : [ `MainQueue
| `TacQueue of solving_tac * anon_abstracting_tac * cancel_switch
| `QueryQueue of cancel_switch
| `SkipQueue ] }
-type fork_t = aast * Vcs_.Branch.t * Vernacexpr.opacity_guarantee * Id.t list
+type fork_t = aast * Vcs_.Branch.t * Vernacexpr.opacity_guarantee * Names.Id.t list
type qed_t = {
qast : aast;
keep : vernac_qed_type;
@@ -195,8 +127,9 @@ type qed_t = {
brname : Vcs_.Branch.t;
brinfo : branch_type Vcs_.branch_info
}
-type seff_t = aast option
+type seff_t = ReplayCommand of aast | CherryPickEnv
type alias_t = Stateid.t * aast
+
type transaction =
| Cmd of cmd_t
| Fork of fork_t
@@ -208,7 +141,7 @@ type step =
[ `Cmd of cmd_t
| `Fork of fork_t * Stateid.t option
| `Qed of qed_t * Stateid.t
- | `Sideff of [ `Ast of aast * Stateid.t | `Id of Stateid.t ]
+ | `Sideff of seff_t * Stateid.t
| `Alias of alias_t ]
type visit = { step : step; next : Stateid.t }
@@ -276,7 +209,7 @@ end = struct (* {{{ *)
let proof_nesting vcs =
List.fold_left max 0
- (List.map_filter
+ (CList.map_filter
(function
| { Vcs_.kind = `Proof (_,n) } -> Some n
| { Vcs_.kind = `Edit _ } -> Some 1
@@ -286,7 +219,7 @@ end = struct (* {{{ *)
let find_proof_at_depth vcs pl =
try List.find (function
| _, { Vcs_.kind = `Proof(m, n) } -> Int.equal n pl
- | _, { Vcs_.kind = `Edit _ } -> anomaly(Pp.str "find_proof_at_depth")
+ | _, { Vcs_.kind = `Edit _ } -> anomaly(Pp.str "find_proof_at_depth.")
| _ -> false)
(List.map (fun h -> h, Vcs_.get_branch vcs h) (Vcs_.branches vcs))
with Not_found -> failwith "find_proof_at_depth"
@@ -294,9 +227,9 @@ end = struct (* {{{ *)
exception Expired
let visit vcs id =
if Stateid.equal id Stateid.initial then
- anomaly(Pp.str "Visiting the initial state id")
+ anomaly(Pp.str "Visiting the initial state id.")
else if Stateid.equal id Stateid.dummy then
- anomaly(Pp.str "Visiting the dummy state id")
+ anomaly(Pp.str "Visiting the dummy state id.")
else
try
match Vcs_.Dag.from_node (Vcs_.dag vcs) id with
@@ -307,12 +240,12 @@ end = struct (* {{{ *)
| [p, Noop; n, Fork x] -> { step = `Fork (x,Some p); next = n }
| [n, Qed x; p, Noop]
| [p, Noop; n, Qed x] -> { step = `Qed (x,p); next = n }
- | [n, Sideff None; p, Noop]
- | [p, Noop; n, Sideff None]-> { step = `Sideff (`Id p); next = n }
- | [n, Sideff (Some x); p, Noop]
- | [p, Noop; n, Sideff (Some x)]-> { step = `Sideff(`Ast (x,p)); next = n }
- | [n, Sideff (Some x)]-> {step = `Sideff(`Ast (x,Stateid.dummy)); next=n}
- | _ -> anomaly (Pp.str ("Malformed VCS at node "^Stateid.to_string id))
+ | [n, Sideff CherryPickEnv; p, Noop]
+ | [p, Noop; n, Sideff CherryPickEnv]-> { step = `Sideff (CherryPickEnv, p); next = n }
+ | [n, Sideff (ReplayCommand x); p, Noop]
+ | [p, Noop; n, Sideff (ReplayCommand x)]-> { step = `Sideff(ReplayCommand x,p); next = n }
+ | [n, Sideff (ReplayCommand x)]-> {step = `Sideff(ReplayCommand x, Stateid.dummy); next=n}
+ | _ -> anomaly (Pp.str ("Malformed VCS at node "^Stateid.to_string id^"."))
with Not_found -> raise Expired
end (* }}} *)
@@ -373,7 +306,7 @@ module VCS : sig
val proof_nesting : unit -> int
val checkout_shallowest_proof_branch : unit -> unit
- val propagate_sideff : replay:aast option -> unit
+ val propagate_sideff : action:seff_t -> unit
val gc : unit -> unit
@@ -392,18 +325,27 @@ end = struct (* {{{ *)
open Printf
let print_dag vcs () =
+
+ (* Due to threading, be wary that this will be called from the
+ toplevel with we_are_parsing set to true, as indeed, the
+ toplevel is waiting for input . What a race! XD
+
+ In case you are hitting the race enable stm_debug.
+ *)
+ if stm_debug () then Flags.we_are_parsing := false;
+
let fname =
"stm_" ^ Str.global_replace (Str.regexp " ") "_" (System.process_id ()) in
let string_of_transaction = function
| Cmd { cast = t } | Fork (t, _,_,_) ->
(try Pp.string_of_ppcmds (pr_ast t) with _ -> "ERR")
- | Sideff (Some t) ->
+ | Sideff (ReplayCommand t) ->
sprintf "Sideff(%s)"
(try Pp.string_of_ppcmds (pr_ast t) with _ -> "ERR")
- | Sideff None -> "EnvChange"
+ | Sideff CherryPickEnv -> "EnvChange"
| Noop -> " "
| Alias (id,_) -> sprintf "Alias(%s)" (Stateid.to_string id)
- | Qed { qast } -> string_of_ppcmds (pr_ast qast) in
+ | Qed { qast } -> Pp.string_of_ppcmds (pr_ast qast) in
let is_green id =
match get_info vcs id with
| Some { state = Valid _ } -> true
@@ -532,10 +474,12 @@ end = struct (* {{{ *)
vcs := rewrite_merge !vcs id ~ours ~theirs:Noop ~at branch
let reachable id = reachable !vcs id
let mk_branch_name { expr = x } = Branch.make
- (match x with
- | VernacDefinition (_,((_,i),_),_) -> string_of_id i
- | VernacStartTheoremProof (_,[Some ((_,i),_),_],_) -> string_of_id i
- | _ -> "branch")
+ (let rec aux x = match x with
+ | VernacDefinition (_,((_,i),_),_) -> Names.string_of_id i
+ | VernacStartTheoremProof (_,[Some ((_,i),_),_]) -> Names.string_of_id i
+ | VernacTime (_, e)
+ | VernacTimeout (_, e) -> aux e
+ | _ -> "branch" in aux x)
let edit_branch = Branch.make "edit"
let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind
let get_info id =
@@ -558,7 +502,7 @@ end = struct (* {{{ *)
if List.mem edit_branch (Vcs_.branches !vcs) then begin
checkout edit_branch;
match get_branch edit_branch with
- | { kind = `Edit (mode, _,_,_,_) } -> Proof_global.activate_proof_mode mode
+ | { kind = `Edit (mode, _,_,_,_) } -> Proof_global.activate_proof_mode mode [@ocaml.warning "-3"]
| _ -> assert false
end else
let pl = proof_nesting () in
@@ -566,18 +510,18 @@ end = struct (* {{{ *)
let branch, mode = match Vcs_aux.find_proof_at_depth !vcs pl with
| h, { Vcs_.kind = `Proof (m, _) } -> h, m | _ -> assert false in
checkout branch;
- prerr_endline (fun () -> "mode:" ^ mode);
- Proof_global.activate_proof_mode mode
+ stm_prerr_endline (fun () -> "mode:" ^ mode);
+ Proof_global.activate_proof_mode mode [@ocaml.warning "-3"]
with Failure _ ->
checkout Branch.master;
- Proof_global.disactivate_current_proof_mode ()
+ Proof_global.disactivate_current_proof_mode () [@ocaml.warning "-3"]
(* copies the transaction on every open branch *)
- let propagate_sideff ~replay:t =
+ let propagate_sideff ~action =
List.iter (fun b ->
checkout b;
let id = new_node () in
- merge id ~ours:(Sideff t) ~into:b Branch.master)
+ merge id ~ours:(Sideff action) ~into:b Branch.master)
(List.filter (fun b -> not (Branch.equal b Branch.master)) (branches ()))
let visit id = Vcs_aux.visit !vcs id
@@ -588,10 +532,10 @@ end = struct (* {{{ *)
match visit id with
| { next = n; step = `Cmd x } -> (id,Cmd x) :: aux n
| { next = n; step = `Alias x } -> (id,Alias x) :: aux n
- | { next = n; step = `Sideff (`Ast (x,_)) } ->
- (id,Sideff (Some x)) :: aux n
- | _ -> anomaly(str("Cannot slice from "^ Stateid.to_string block_start ^
- " to "^Stateid.to_string block_stop))
+ | { next = n; step = `Sideff (ReplayCommand x,_) } ->
+ (id,Sideff (ReplayCommand x)) :: aux n
+ | _ -> anomaly Pp.(str("Cannot slice from "^ Stateid.to_string block_start ^
+ " to "^Stateid.to_string block_stop^"."))
in aux block_stop
let slice ~block_start ~block_stop =
@@ -643,11 +587,11 @@ end = struct (* {{{ *)
l
let create_proof_task_box l ~qed ~block_start:lemma =
- if not (topo_invariant l) then anomaly (str "overlapping boxes");
+ if not (topo_invariant l) then anomaly Pp.(str "overlapping boxes.");
vcs := create_property !vcs l (ProofTask { qed; lemma })
let create_proof_block ({ block_start; block_stop} as decl) name =
let l = nodes_in_slice ~block_start ~block_stop in
- if not (topo_invariant l) then anomaly (str "overlapping boxes");
+ if not (topo_invariant l) then anomaly Pp.(str "overlapping boxes.");
vcs := create_property !vcs l (ProofBlock (decl, name))
let box_of id = List.map Dag.Property.data (property_of !vcs id)
let delete_boxes_of id =
@@ -658,7 +602,7 @@ end = struct (* {{{ *)
with
| [] -> None
| [x] -> Some x
- | _ -> anomaly (str "node with more than 1 proof task box")
+ | _ -> anomaly Pp.(str "node with more than 1 proof task box.")
let gc () =
let old_vcs = !vcs in
@@ -739,14 +683,14 @@ module State : sig
?safe_id:Stateid.t ->
?redefine:bool -> ?cache:Summary.marshallable ->
?feedback_processed:bool -> (unit -> unit) -> Stateid.t -> unit
- val fix_exn_ref : (iexn -> iexn) ref
+ 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 -> iexn -> iexn
+ 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
@@ -759,6 +703,9 @@ module State : sig
val proof_part_of_frozen : frozen_state -> proof_part
val assign : Stateid.t -> partial_state -> 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 (* {{{ *)
(* cur_id holds Stateid.dummy in case the last attempt to define a state
@@ -819,13 +766,13 @@ end = struct (* {{{ *)
| _ ->
(* coqc has a 1 slot cache and only for valid states *)
if interactive () = `No && Stateid.equal id !cur_id then ()
- else anomaly (str "installing a non cached state")
+ else anomaly Pp.(str "installing a non cached state.")
let get_cached id =
try match VCS.get_info id with
| { state = Valid s } -> s
- | _ -> anomaly (str "not a cached state")
- with VCS.Expired -> anomaly (str "not a cached state (expired)")
+ | _ -> anomaly Pp.(str "not a cached state.")
+ with VCS.Expired -> anomaly Pp.(str "not a cached state (expired).")
let assign id what =
if VCS.get_state id <> Empty then () else
@@ -858,9 +805,9 @@ end = struct (* {{{ *)
match Stateid.get info with
| Some _ -> (e, info)
| None ->
- let loc = Option.default Loc.ghost (Loc.get_loc info) in
+ let loc = Loc.get_loc info in
let (e, info) = Hooks.(call_process_error_once (e, info)) in
- Hooks.(call execution_error id loc (iprint (e, info)));
+ execution_error ?loc id (iprint (e, info));
(e, Stateid.add info ~valid id)
let same_env { system = s1 } { system = s2 } =
@@ -873,12 +820,12 @@ end = struct (* {{{ *)
let define ?safe_id ?(redefine=false) ?(cache=`No) ?(feedback_processed=true)
f id
=
- feedback ~id:(State id) (ProcessingIn !Flags.async_proofs_worker_id);
+ feedback ~id:id (ProcessingIn !Flags.async_proofs_worker_id);
let str_id = Stateid.to_string id in
if is_cached id && not redefine then
- anomaly (str"defining state "++str str_id++str" twice");
+ anomaly Pp.(str"defining state "++str str_id++str" twice.");
try
- prerr_endline (fun () -> "defining "^str_id^" (cache="^
+ stm_prerr_endline (fun () -> "defining "^str_id^" (cache="^
if cache = `Yes then "Y)" else if cache = `Shallow then "S)" else "N)");
let good_id = match safe_id with None -> !cur_id | Some id -> id in
fix_exn_ref := exn_on id ~valid:good_id;
@@ -886,7 +833,7 @@ end = struct (* {{{ *)
fix_exn_ref := (fun x -> x);
if cache = `Yes then freeze `No id
else if cache = `Shallow then freeze `Shallow id;
- prerr_endline (fun () -> "setting cur id to "^str_id);
+ 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);
@@ -910,6 +857,126 @@ end = struct (* {{{ *)
end (* }}} *)
+(* indentation code for Show Script, initially contributed
+ * by D. de Rauglaudre. Should be moved away.
+ *)
+
+module ShowScript = struct
+
+let indent_script_item ((ng1,ngl1),nl,beginend,ppl) (cmd,ng) =
+ (* ng1 : number of goals remaining at the current level (before cmd)
+ ngl1 : stack of previous levels with their remaining goals
+ ng : number of goals after the execution of cmd
+ beginend : special indentation stack for { } *)
+ let ngprev = List.fold_left (+) ng1 ngl1 in
+ let new_ngl =
+ if ng > ngprev then
+ (* We've branched *)
+ (ng - ngprev + 1, ng1 - 1 :: ngl1)
+ else if ng < ngprev then
+ (* A subgoal have been solved. Let's compute the new current level
+ by discarding all levels with 0 remaining goals. *)
+ let rec loop = function
+ | (0, ng2::ngl2) -> loop (ng2,ngl2)
+ | p -> p
+ in loop (ng1-1, ngl1)
+ else
+ (* Standard case, same goal number as before *)
+ (ng1, ngl1)
+ in
+ (* When a subgoal have been solved, separate this block by an empty line *)
+ let new_nl = (ng < ngprev)
+ in
+ (* Indentation depth *)
+ let ind = List.length ngl1
+ in
+ (* Some special handling of bullets and { }, to get a nicer display *)
+ let pred n = max 0 (n-1) in
+ let ind, nl, new_beginend = match cmd with
+ | VernacSubproof _ -> pred ind, nl, (pred ind)::beginend
+ | VernacEndSubproof -> List.hd beginend, false, List.tl beginend
+ | VernacBullet _ -> pred ind, nl, beginend
+ | _ -> ind, nl, beginend
+ in
+ let pp = Pp.(
+ (if nl then fnl () else mt ()) ++
+ (hov (ind+1) (str (String.make ind ' ') ++ Ppvernac.pr_vernac cmd)))
+ in
+ (new_ngl, new_nl, new_beginend, pp :: ppl)
+
+let get_script prf =
+ let branch, test =
+ match prf with
+ | None -> VCS.Branch.master, fun _ -> true
+ | Some name -> VCS.current_branch (),fun nl -> nl=[] || List.mem name nl in
+ let rec find acc id =
+ if Stateid.equal id Stateid.initial ||
+ Stateid.equal id Stateid.dummy then acc else
+ let view = VCS.visit id in
+ match view.step with
+ | `Fork((_,_,_,ns), _) when test ns -> acc
+ | `Qed (qed, proof) -> find [qed.qast.expr, (VCS.get_info id).n_goals] proof
+ | `Sideff (ReplayCommand x,_) ->
+ find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next
+ | `Sideff (CherryPickEnv, id) -> find acc id
+ | `Cmd {cast = x; ctac} when ctac -> (* skip non-tactics *)
+ find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next
+ | `Cmd _ -> find acc view.next
+ | `Alias (id,_) -> find acc id
+ | `Fork _ -> find acc view.next
+ in
+ find [] (VCS.get_branch_pos branch)
+
+let show_script ?proof () =
+ try
+ let prf =
+ try match proof with
+ | None -> Some (Proof_global.get_current_proof_name ())
+ | Some (p,_) -> Some (p.Proof_global.id)
+ with Proof_global.NoCurrentProof -> None
+ in
+ let cmds = get_script prf in
+ let _,_,_,indented_cmds =
+ List.fold_left indent_script_item ((1,[]),false,[],[]) cmds
+ in
+ let indented_cmds = List.rev (indented_cmds) in
+ msg_notice Pp.(v 0 (prlist_with_sep fnl (fun x -> x) indented_cmds))
+ with Vcs_aux.Expired -> ()
+
+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 } =
+ (* 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;
+ 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
+ * future refactorings.
+ *)
+ let rec is_filtered_command = function
+ | VernacResetName _ | VernacResetInitial | VernacBack _
+ | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _
+ | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true
+ | VernacTime (_,e) | VernacTimeout (_,e) | VernacRedirect (_,(_,e)) -> is_filtered_command e
+ | _ -> false
+ in
+ let aux_interp cmd =
+ if is_filtered_command cmd then
+ stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr)
+ else match cmd with
+ | VernacShow ShowScript -> ShowScript.show_script ()
+ | expr ->
+ stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr);
+ try Vernacentries.interp ?verbosely:(Some verbose) ?proof (Loc.tag ?loc expr)
+ with e ->
+ let e = CErrors.push e in
+ Exninfo.iraise Hooks.(call_process_error_once e)
+ in aux_interp expr
(****************************** CRUFT *****************************************)
(******************************************************************************)
@@ -919,7 +986,6 @@ module Backtrack : sig
val record : unit -> unit
val backto : Stateid.t -> unit
- val back_safe : unit -> unit
(* we could navigate the dag, but this ways easy *)
val branches_of : Stateid.t -> backup
@@ -948,16 +1014,16 @@ end = struct (* {{{ *)
let info = VCS.get_info oid in
match info.vcs_backup with
| None, _ ->
- anomaly(str"Backtrack.backto "++str(Stateid.to_string oid)++
- str": a state with no vcs_backup")
+ 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
| _, None ->
- anomaly(str"Backtrack.branches_of "++str(Stateid.to_string id)++
- str": a state with no vcs_backup")
+ anomaly Pp.(str"Backtrack.branches_of "++str(Stateid.to_string id)++
+ str": a state with no vcs_backup.")
| _, Some x -> x
let rec fold_until f acc id =
@@ -979,13 +1045,6 @@ end = struct (* {{{ *)
| `Stop x -> x
| `Cont acc -> next acc
- let back_safe () =
- let id =
- fold_until (fun n (id,_,_,_,_) ->
- if n >= 0 && State.is_cached_and_valid id then `Stop id else `Cont (succ n))
- 0 (VCS.get_branch_pos (VCS.current_branch ())) in
- backto id
-
let undo_vernac_classifier v =
try
match v with
@@ -1018,7 +1077,7 @@ end = struct (* {{{ *)
let id = VCS.get_branch_pos (VCS.current_branch ()) in
let vcs =
match (VCS.get_info id).vcs_backup with
- | None, _ -> anomaly(str"Backtrack: tip with no vcs_backup")
+ | None, _ -> anomaly Pp.(str"Backtrack: tip with no vcs_backup.")
| Some vcs, _ -> vcs in
let cb, _ =
try Vcs_aux.find_proof_at_depth vcs (Vcs_aux.proof_nesting vcs)
@@ -1037,12 +1096,12 @@ end = struct (* {{{ *)
VtStm (VtBack oid, true), VtLater
| VernacBacktrack (id,_,_)
| VernacBackTo id ->
- VtStm (VtBack (Stateid.of_int id), not !Flags.print_emacs), VtNow
+ VtStm (VtBack (Stateid.of_int id), not !Flags.batch_mode), VtNow
| _ -> VtUnknown, VtNow
with
| Not_found ->
- CErrors.errorlabstrm "undo_vernac_classifier"
- (str "Cannot undo")
+ CErrors.user_err ~hdr:"undo_vernac_classifier"
+ Pp.(str "Cannot undo")
end (* }}} *)
@@ -1050,11 +1109,11 @@ 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 !hints loc "context_used" in
+ 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.ghost, id) ids in
+ let ids = List.map (fun id -> Loc.tag id) ids in
begin match ids with
| [] -> SsEmpty
| x :: xs ->
@@ -1063,18 +1122,18 @@ let get_hint_ctx loc =
| _ -> raise Not_found
let get_hint_bp_time proof_name =
- try float_of_string (Aux_file.get !hints Loc.ghost proof_name)
+ try float_of_string (Aux_file.get !hints proof_name)
with Not_found -> 1.0
-let record_pb_time proof_name loc time =
+let record_pb_time ?loc proof_name time =
let proof_build_time = Printf.sprintf "%.3f" time in
- Aux_file.record_in_aux_at loc "proof_build_time" proof_build_time;
+ Aux_file.record_in_aux_at ?loc "proof_build_time" proof_build_time;
if proof_name <> "" then begin
- Aux_file.record_in_aux_at Loc.ghost proof_name proof_build_time;
- hints := Aux_file.set !hints Loc.ghost proof_name proof_build_time
+ Aux_file.record_in_aux_at proof_name proof_build_time;
+ hints := Aux_file.set !hints proof_name proof_build_time
end
-exception RemoteException of std_ppcmds
+exception RemoteException of Pp.std_ppcmds
let _ = CErrors.register_handler (function
| RemoteException ppcmd -> ppcmd
| _ -> raise Unhandled)
@@ -1109,13 +1168,13 @@ let proof_block_delimiters = ref []
let register_proof_block_delimiter name static dynamic =
if List.mem_assoc name !proof_block_delimiters then
- CErrors.errorlabstrm "STM" (str "Duplicate block delimiter " ++ str name);
+ CErrors.user_err ~hdr:"STM" Pp.(str "Duplicate block delimiter " ++ str name);
proof_block_delimiters := (name, (static,dynamic)) :: !proof_block_delimiters
let mk_doc_node id = function
| { step = `Cmd { ctac; cast = { indentation; expr }}; next } when ctac ->
Some { indentation; ast = expr; id }
- | { step = `Sideff (`Ast ({ indentation; expr }, _)); next } ->
+ | { step = `Sideff (ReplayCommand { indentation; expr }, _); next } ->
Some { indentation; ast = expr; id }
| _ -> None
let prev_node { id } =
@@ -1144,12 +1203,14 @@ let detect_proof_block id name =
VCS.create_proof_block decl name
end
with Not_found ->
- CErrors.errorlabstrm "STM"
- (str "Unknown proof block delimiter " ++ str name)
+ CErrors.user_err ~hdr:"STM"
+ Pp.(str "Unknown proof block delimiter " ++ str name)
)
(****************************** THE SCHEDULER *********************************)
(******************************************************************************)
+(* Unused module warning doesn't understand [module rec] *)
+[@@@ocaml.warning "-60"]
module rec ProofTask : sig
type competence = Stateid.t list
@@ -1160,7 +1221,7 @@ module rec ProofTask : sig
t_drop : bool;
t_states : competence;
t_assign : Proof_global.closed_proof_output Future.assignement -> unit;
- t_loc : Loc.t;
+ t_loc : Loc.t option;
t_uuid : Future.UUID.t;
t_name : string }
@@ -1178,8 +1239,9 @@ module rec ProofTask : sig
and type request := request
val build_proof_here :
+ ?loc:Loc.t ->
drop_pt:bool ->
- Stateid.t * Stateid.t -> Loc.t -> Stateid.t ->
+ Stateid.t * Stateid.t -> Stateid.t ->
Proof_global.closed_proof_output Future.computation
(* If set, only tasks overlapping with this list are processed *)
@@ -1197,7 +1259,7 @@ end = struct (* {{{ *)
t_drop : bool;
t_states : competence;
t_assign : Proof_global.closed_proof_output Future.assignement -> unit;
- t_loc : Loc.t;
+ t_loc : Loc.t option;
t_uuid : Future.UUID.t;
t_name : string }
@@ -1212,14 +1274,13 @@ end = struct (* {{{ *)
type error = {
e_error_at : Stateid.t;
e_safe_id : Stateid.t;
- e_msg : std_ppcmds;
+ e_msg : Pp.std_ppcmds;
e_safe_states : Stateid.t list }
type response =
| RespBuiltProof of Proof_global.closed_proof_output * float
| RespError of error
| RespStates of (Stateid.t * State.partial_state) list
- | RespDone
let name = ref "proofworker"
let extra_env () = !async_proofs_workers_extra_env
@@ -1266,7 +1327,7 @@ end = struct (* {{{ *)
RespBuiltProof (pl, time) ->
feedback (InProgress ~-1);
t_assign (`Val pl);
- record_pb_time t_name t_loc time;
+ record_pb_time ?loc:t_loc t_name time;
if !Flags.async_proofs_full || t_drop
then `Stay(t_states,[States t_states])
else `End
@@ -1285,21 +1346,21 @@ end = struct (* {{{ *)
| Some (BuildProof { t_start = start; t_assign }) ->
let s = "Worker dies or task expired" in
let info = Stateid.add ~valid:start Exninfo.null start in
- let e = (RemoteException (strbrk s), info) in
+ let e = (RemoteException (Pp.strbrk s), info) in
t_assign (`Exn e);
- Hooks.(call execution_error start Loc.ghost (strbrk s));
+ execution_error start (Pp.strbrk s);
feedback (InProgress ~-1)
- let build_proof_here ~drop_pt (id,valid) loc eop =
+ 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
else Reach.known_state ~cache:`Shallow eop;
let wall_clock2 = Unix.gettimeofday () in
- Aux_file.record_in_aux_at loc "proof_build_time"
+ Aux_file.record_in_aux_at ?loc "proof_build_time"
(Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
let p = Proof_global.return_proof ~allow_partial:drop_pt () in
- if drop_pt then feedback ~id:(State id) Complete;
+ if drop_pt then feedback ~id Complete;
p)
let perform_buildp { Stateid.exn_info; stop; document; loc } drop my_states =
@@ -1308,7 +1369,7 @@ end = struct (* {{{ *)
VCS.print ();
let proof, future_proof, time =
let wall_clock = Unix.gettimeofday () in
- let fp = build_proof_here ~drop_pt:drop exn_info loc stop in
+ let fp = build_proof_here ?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
@@ -1318,10 +1379,10 @@ end = struct (* {{{ *)
if not drop then begin
let checked_proof = Future.chain ~pure:false future_proof (fun p ->
let pobject, _ =
- Proof_global.close_future_proof stop (Future.from_val ~fix_exn p) in
+ 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
- vernac_interp stop
+ stm_vernac_interp stop
~proof:(pobject, terminator)
{ verbose = false; loc; indentation = 0; strlen = 0;
expr = (VernacEndProof (Proved (Opaque None,None))) }) in
@@ -1337,11 +1398,10 @@ end = struct (* {{{ *)
| Some (safe, err) -> err, safe
| None -> Stateid.dummy, Stateid.dummy in
let e_msg = iprint (e, info) in
- prerr_endline (fun () -> "failed with the following exception:");
- prerr_endline (fun () -> string_of_ppcmds e_msg);
+ stm_pperr_endline Pp.(fun () -> str "failed with the following exception: " ++ fnl () ++ e_msg);
let e_safe_states = List.filter State.is_cached_and_valid my_states in
RespError { e_error_at; e_safe_id; e_msg; e_safe_states }
-
+
let perform_states query =
if query = [] then [] else
let is_tac e = match classify_vernac e with
@@ -1369,7 +1429,7 @@ end = struct (* {{{ *)
when is_tac expr && State.same_env o n -> (* A pure tactic *)
Some (id, `Proof (prev, State.proof_part_of_frozen n))
| Some _, Some s ->
- msg_debug (str "STM: sending back a fat state");
+ msg_debug (Pp.str "STM: sending back a fat state");
Some (id, `Full s)
| _, Some s -> Some (id, `Full s) in
let rec aux seen = function
@@ -1385,13 +1445,13 @@ end = struct (* {{{ *)
| ReqStates sl -> RespStates (perform_states sl)
let on_marshal_error s = function
- | States _ -> msg_error(strbrk("Marshalling error: "^s^". "^
+ | States _ -> msg_error(Pp.strbrk("Marshalling error: "^s^". "^
"The system state could not be sent to the master process."))
| BuildProof { t_exn_info; t_stop; t_assign; t_loc; t_drop = drop_pt } ->
- msg_error(strbrk("Marshalling error: "^s^". "^
+ msg_error(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 ~drop_pt t_exn_info t_loc t_stop));
+ t_assign(`Comp(build_proof_here ?loc:t_loc ~drop_pt t_exn_info t_stop));
feedback (InProgress ~-1)
end (* }}} *)
@@ -1401,7 +1461,7 @@ and Slaves : sig
(* (eventually) remote calls *)
val build_proof :
- loc:Loc.t -> drop_pt:bool ->
+ ?loc:Loc.t -> drop_pt:bool ->
exn_info:(Stateid.t * Stateid.t) -> block_start:Stateid.t -> block_stop:Stateid.t ->
name:string -> future_proof * cancel_switch
@@ -1441,7 +1501,7 @@ end = struct (* {{{ *)
let check_task_aux extra name l i =
let { Stateid.stop; document; loc; name = r_name }, drop = List.nth l i in
Flags.if_verbose msg_info
- (str(Printf.sprintf "Checking task %d (%s%s) of %s" i r_name extra name));
+ Pp.(str(Printf.sprintf "Checking task %d (%s%s) of %s" i r_name extra name));
VCS.restore document;
let start =
let rec aux cur =
@@ -1463,7 +1523,7 @@ 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;
- vernac_interp stop ~proof
+ stm_vernac_interp stop ~proof
{ verbose = false; loc; indentation = 0; strlen = 0;
expr = (VernacEndProof (Proved (Opaque None,None))) };
`OK proof
@@ -1472,7 +1532,7 @@ end = struct (* {{{ *)
let (e, info) = CErrors.push e in
(try match Stateid.get info with
| None ->
- msg_error (
+ msg_error Pp.(
str"File " ++ str name ++ str ": proof of " ++ str r_name ++
spc () ++ iprint (e, info))
| Some (_, cur) ->
@@ -1480,18 +1540,18 @@ end = struct (* {{{ *)
| { step = `Cmd { cast = { loc } } }
| { step = `Fork (( { loc }, _, _, _), _) }
| { step = `Qed ( { qast = { loc } }, _) }
- | { step = `Sideff (`Ast ( { loc }, _)) } ->
- let start, stop = Loc.unloc loc in
- msg_error (
+ | { step = `Sideff (ReplayCommand { loc }, _) } ->
+ let start, stop = Option.cata Loc.unloc (0,0) loc in
+ msg_error Pp.(
str"File " ++ str name ++ str ": proof of " ++ str r_name ++
str ": chars " ++ int start ++ str "-" ++ int stop ++
spc () ++ iprint (e, info))
| _ ->
- msg_error (
+ msg_error Pp.(
str"File " ++ str name ++ str ": proof of " ++ str r_name ++
spc () ++ iprint (e, info))
with e ->
- msg_error (str"unable to print error message: " ++
+ msg_error Pp.(str"unable to print error message: " ++
str (Printexc.to_string e)));
if drop then `ERROR_ADMITTED else `ERROR
@@ -1520,9 +1580,9 @@ end = struct (* {{{ *)
Future.from_val (Option.get (Global.body_of_constant_body c)) in
let uc =
Future.chain
- ~greedy:true ~pure:true uc Univ.hcons_universe_context_set in
- let pr = Future.chain ~greedy:true ~pure:true pr discharge in
- let pr = Future.chain ~greedy:true ~pure:true pr Constr.hcons in
+ ~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.sink pr;
let extra = Future.join uc in
u.(bucket) <- uc;
@@ -1537,10 +1597,10 @@ end = struct (* {{{ *)
let info_tasks l =
CList.map_i (fun i ({ Stateid.loc; name }, _) ->
let time1 =
- try float_of_string (Aux_file.get !hints loc "proof_build_time")
+ try float_of_string (Aux_file.get ?loc !hints "proof_build_time")
with Not_found -> 0.0 in
let time2 =
- try float_of_string (Aux_file.get !hints loc "proof_check_time")
+ try float_of_string (Aux_file.get ?loc !hints "proof_check_time")
with Not_found -> 0.0 in
name, max (time1 +. time2) 0.0001,i) 0 l
@@ -1561,7 +1621,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 ?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
@@ -1576,7 +1636,7 @@ end = struct (* {{{ *)
TaskQueue.enqueue_task (Option.get !queue) (task,cancel_switch);
f, cancel_switch
end else
- ProofTask.build_proof_here ~drop_pt t_exn_info loc block_stop, cancel_switch
+ ProofTask.build_proof_here ?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
@@ -1603,7 +1663,7 @@ end = struct (* {{{ *)
| Some (ReqBuildProof (r, b, _)) -> Some(r, b)
| _ -> None)
tasks in
- prerr_endline (fun () -> Printf.sprintf "dumping %d tasks\n" (List.length reqs));
+ stm_prerr_endline (fun () -> Printf.sprintf "dumping %d tasks\n" (List.length reqs));
reqs
let reset_task_queue () = TaskQueue.clear (Option.get !queue)
@@ -1612,7 +1672,7 @@ end (* }}} *)
and TacTask : sig
- type output = Constr.constr * Evd.evar_universe_context
+ type output = (Constr.constr * Evd.evar_universe_context) option
type task = {
t_state : Stateid.t;
t_state_fb : Stateid.t;
@@ -1621,13 +1681,12 @@ and TacTask : sig
t_goal : Goal.goal;
t_kill : unit -> unit;
t_name : string }
- exception NoProgress
include AsyncTaskQueue.Task with type task := task
end = struct (* {{{ *)
- type output = Constr.constr * Evd.evar_universe_context
+ type output = (Constr.constr * Evd.evar_universe_context) option
let forward_feedback msg = Hooks.(call forward_feedback msg)
@@ -1649,10 +1708,9 @@ end = struct (* {{{ *)
r_name : string }
type response =
- | RespBuiltSubProof of output
- | RespError of std_ppcmds
+ | RespBuiltSubProof of (Constr.constr * Evd.evar_universe_context)
+ | RespError of Pp.std_ppcmds
| RespNoProgress
- exception NoProgress
let name = ref "tacworker"
let extra_env () = [||]
@@ -1674,10 +1732,9 @@ end = struct (* {{{ *)
let use_response _ { t_assign; t_state; t_state_fb; t_kill } resp =
match resp with
- | RespBuiltSubProof o -> t_assign (`Val o); `Stay ((),[])
+ | RespBuiltSubProof o -> t_assign (`Val (Some o)); `Stay ((),[])
| RespNoProgress ->
- let e = (NoProgress, Exninfo.null) in
- t_assign (`Exn e);
+ t_assign (`Val None);
t_kill ();
`Stay ((),[])
| RespError msg ->
@@ -1687,7 +1744,7 @@ end = struct (* {{{ *)
`Stay ((),[])
let on_marshal_error err { t_name } =
- pr_err ("Fatal marshal error: " ^ t_name );
+ stm_pr_err ("Fatal marshal error: " ^ t_name );
flush_all (); exit 1
let on_task_cancellation_or_expiration_or_slave_death = function
@@ -1704,25 +1761,28 @@ end = struct (* {{{ *)
Future.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
if not (
- Evarutil.is_ground_term sigma0 Evd.(evar_concl g) &&
- List.for_all (Context.Named.Declaration.for_all (Evarutil.is_ground_term sigma0))
+ is_ground Evd.(evar_concl g) &&
+ List.for_all (Context.Named.Declaration.for_all is_ground)
Evd.(evar_context g))
then
- CErrors.errorlabstrm "STM" (strbrk("the par: goal selector supports ground "^
+ CErrors.user_err ~hdr:"STM" Pp.(strbrk("the par: goal selector supports ground "^
"goals only"))
else begin
let (i, ast) = r_ast in
Proof_global.simple_with_current_proof (fun _ p -> Proof.focus focus_cond () i p);
- vernac_interp r_state_fb ast;
+ stm_vernac_interp r_state_fb 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
| 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
RespBuiltSubProof (t, Evd.evar_universe_context sigma)
- else CErrors.errorlabstrm "STM" (str"The solution is not ground")
+ else CErrors.user_err ~hdr:"STM" Pp.(str"The solution is not ground")
end) ()
with e when CErrors.noncritical e -> RespError (CErrors.print e)
@@ -1751,7 +1811,7 @@ 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
- Hooks.call Hooks.with_fail fail (fun () ->
+ Vernacentries.with_fail 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 ->
@@ -1773,11 +1833,11 @@ end = struct (* {{{ *)
1 goals in
TaskQueue.join queue;
let assign_tac : unit Proofview.tactic =
- Proofview.(Goal.nf_enter { Goal.enter = fun g ->
+ Proofview.(Goal.nf_enter begin fun g ->
let gid = Goal.goal g in
let f =
try List.assoc gid res
- with Not_found -> CErrors.anomaly(str"Partac: wrong focus") in
+ with Not_found -> CErrors.anomaly(str"Partac: wrong focus.") in
if not (Future.is_over f) then
(* One has failed and cancelled the others, but not this one *)
if solve then Tacticals.New.tclZEROMSG
@@ -1785,18 +1845,18 @@ end = struct (* {{{ *)
else tclUNIT ()
else
let open Notations in
- try
- let pt, uc = Future.join f in
- prerr_endline (fun () -> string_of_ppcmds(hov 0 (
+ match Future.join f with
+ | Some (pt, uc) ->
+ stm_pperr_endline (fun () -> hov 0 (
str"g=" ++ int (Evar.repr gid) ++ spc () ++
str"t=" ++ (Printer.pr_constr pt) ++ spc () ++
- str"uc=" ++ Evd.pr_evar_universe_context uc)));
+ str"uc=" ++ Termops.pr_evar_universe_context uc));
(if abstract then Tactics.tclABSTRACT None else (fun x -> x))
(V82.tactic (Refiner.tclPUSHEVARUNIVCONTEXT uc) <*>
- Tactics.exact_no_check pt)
- with TacTask.NoProgress ->
+ Tactics.exact_no_check (EConstr.of_constr pt))
+ | None ->
if solve then Tacticals.New.tclSOLVE [] else tclUNIT ()
- })
+ end)
in
Proof.run_tactic (Global.env()) assign_tac p)))) ())
@@ -1832,7 +1892,7 @@ end = struct (* {{{ *)
let use_response _ _ _ = `End
let on_marshal_error _ _ =
- pr_err ("Fatal marshal error in query");
+ stm_pr_err ("Fatal marshal error in query");
flush_all (); exit 1
let on_task_cancellation_or_expiration_or_slave_death _ = ()
@@ -1844,12 +1904,12 @@ end = struct (* {{{ *)
VCS.print ();
Reach.known_state ~cache:`No r_where;
try
- vernac_interp r_for { r_what with verbose = true };
- feedback ~id:(State r_for) Processed
+ stm_vernac_interp r_for { r_what with verbose = true };
+ feedback ~id:r_for Processed
with e when CErrors.noncritical e ->
let e = CErrors.push e in
- let msg = pp_to_richpp (iprint e) in
- feedback ~id:(State r_for) (Message (Error, None, msg))
+ let msg = iprint e in
+ feedback ~id:r_for (Message (Error, None, msg))
let name_of_task { t_what } = string_of_ppcmds (pr_ast t_what)
let name_of_request { r_what } = string_of_ppcmds (pr_ast r_what)
@@ -1907,11 +1967,11 @@ let warn_deprecated_nested_proofs =
"stop working in a future Coq version"))
let collect_proof keep cur hd brkind id =
- prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id);
+ stm_prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id);
let no_name = "" in
let name = function
| [] -> no_name
- | id :: _ -> Id.to_string id in
+ | id :: _ -> Names.Id.to_string id in
let loc = (snd cur).loc in
let rec is_defined_expr = function
| VernacEndProof (Proved ((Transparent|Opaque (Some _)),_)) -> true
@@ -1943,10 +2003,10 @@ let collect_proof keep cur hd brkind id =
let rec collect last accn id =
let view = VCS.visit id in
match view.step with
- | (`Sideff (`Ast(x,_)) | `Cmd { cast = x })
+ | (`Sideff (ReplayCommand x,_) | `Cmd { cast = x })
when too_complex_to_delegate x -> `Sync(no_name,None,`Print)
| `Cmd { cast = x } -> collect (Some (id,x)) (id::accn) view.next
- | `Sideff (`Ast(x,_)) -> collect (Some (id,x)) (id::accn) view.next
+ | `Sideff (ReplayCommand x,_) -> collect (Some (id,x)) (id::accn) view.next
(* An Alias could jump everywhere... we hope we can ignore it*)
| `Alias _ -> `Sync (no_name,None,`Alias)
| `Fork((_,_,_,_::_::_), _) ->
@@ -1983,7 +2043,8 @@ let collect_proof keep cur hd brkind id =
| `ASync(_,pua,_,name,_) -> `Sync (name,pua,why) in
let check_policy rc = if async_policy () then rc else make_sync `Policy rc in
match cur, (VCS.visit id).step, brkind with
- | (parent, { expr = VernacExactProof _ }), `Fork _, _ ->
+ | (parent, { expr = VernacExactProof _ }), `Fork _, _
+ | (parent, { expr = VernacTime (_, VernacExactProof _) }), `Fork _, _ ->
`Sync (no_name,None,`Immediate)
| _, _, { VCS.kind = `Edit _ } -> check_policy (collect (Some cur) [] id)
| _ ->
@@ -2011,7 +2072,7 @@ let string_of_reason = function
| `NoPU_NoHint_NoES -> "no 'Proof using..', no .aux file, inside a section"
| `Unknown -> "unsupported case"
-let log_string s = prerr_debug (fun () -> "STM: " ^ s)
+let log_string s = stm_prerr_debug (fun () -> "STM: " ^ s)
let log_processing_async id name = log_string Printf.(sprintf
"%s: proof %s: asynch" (Stateid.to_string id) name
)
@@ -2036,35 +2097,34 @@ let known_state ?(redefine_qed=false) ~cache id =
Some (decl, name)
| _ -> None) boxes in
assert(List.length valid_boxes < 2);
- if valid_boxes = [] then iraise exn
+ if valid_boxes = [] then Exninfo.iraise exn
else
let decl, name = List.hd valid_boxes in
try
let _, dynamic_check = List.assoc name !proof_block_delimiters in
match dynamic_check decl with
- | `Leaks -> iraise exn
+ | `Leaks -> Exninfo.iraise exn
| `ValidBlock { base_state; goals_to_admit; recovery_command } -> begin
let tac =
- let open Proofview.Notations in
- Proofview.Goal.nf_enter { enter = fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
if CList.mem_f Evar.equal
(Proofview.Goal.goal gl) goals_to_admit then
Proofview.give_up else Proofview.tclUNIT ()
- } in
+ end in
match (VCS.get_info base_state).state with
| Valid { proof } ->
Proof_global.unfreeze proof;
Proof_global.with_current_proof (fun _ p ->
- feedback ~id:(State id) Feedback.AddedAxiom;
+ feedback ~id:id Feedback.AddedAxiom;
fst (Pfedit.solve Vernacexpr.SelectAll None tac p), ());
- Option.iter (fun expr -> vernac_interp id {
- verbose = true; loc = Loc.ghost; expr; indentation = 0;
+ Option.iter (fun expr -> stm_vernac_interp id {
+ verbose = true; loc = None; expr; indentation = 0;
strlen = 0 })
recovery_command
| _ -> assert false
end
with Not_found ->
- CErrors.errorlabstrm "STM"
+ CErrors.user_err ~hdr:"STM"
(str "Unknown proof block delimiter " ++ str name)
in
@@ -2098,16 +2158,16 @@ let known_state ?(redefine_qed=false) ~cache id =
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 ->
- prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string 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 =
- prerr_endline (fun () -> "reaching: " ^ Stateid.to_string 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);
- prerr_endline (fun () -> "reached (cache)");
+ stm_prerr_endline (fun () -> "reached (cache)");
State.install_cached id
end else
let step, cache_step, feedback_processed =
@@ -2122,10 +2182,8 @@ let known_state ?(redefine_qed=false) ~cache id =
(fun () ->
resilient_tactic id cblock (fun () ->
reach ~cache:`Shallow view.next;
- Hooks.(call tactic_being_run true);
Partac.vernac_interp ~solve ~abstract
- cancel !Flags.async_proofs_n_tacworkers view.next id x;
- Hooks.(call tactic_being_run false))
+ cancel !Flags.async_proofs_n_tacworkers view.next id x)
), cache, true
| `Cmd { cast = x; cqueue = `QueryQueue cancel }
when Flags.async_proofs_is_master () -> (fun () ->
@@ -2135,9 +2193,7 @@ 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;
- Hooks.(call tactic_being_run true);
- vernac_interp id x;
- Hooks.(call tactic_being_run false));
+ stm_vernac_interp id x);
if eff then update_global_env ()
), (if eff then `Yes else cache), true
| `Cmd { cast = x; ceff = eff } -> (fun () ->
@@ -2145,22 +2201,22 @@ let known_state ?(redefine_qed=false) ~cache id =
| Flags.APon | Flags.APonLazy ->
resilient_command reach view.next
| Flags.APoff -> reach view.next);
- vernac_interp id x;
+ stm_vernac_interp id x;
if eff then update_global_env ()
), (if eff then `Yes else cache), true
| `Fork ((x,_,_,_), None) -> (fun () ->
resilient_command reach view.next;
- vernac_interp id x;
+ stm_vernac_interp id x;
wall_clock_last_fork := Unix.gettimeofday ()
), `Yes, true
| `Fork ((x,_,_,_), Some prev) -> (fun () -> (* nested proof *)
reach ~cache:`Shallow prev;
reach view.next;
- (try vernac_interp id x;
+ (try stm_vernac_interp id x;
with e when CErrors.noncritical e ->
let (e, info) = CErrors.push e in
let info = Stateid.add info ~valid:prev id in
- iraise (e, info));
+ Exninfo.iraise (e, info));
wall_clock_last_fork := Unix.gettimeofday ()
), `Yes, true
| `Qed ({ qast = x; keep; brinfo; brname } as qed, eop) ->
@@ -2184,7 +2240,7 @@ let known_state ?(redefine_qed=false) ~cache id =
^"the proof's statement to avoid that."));
let fp, cancel =
Slaves.build_proof
- ~loc ~drop_pt ~exn_info ~block_start ~block_stop ~name in
+ ?loc ~drop_pt ~exn_info ~block_start ~block_stop ~name in
Future.replace ofp fp;
qed.fproof <- Some (fp, cancel);
(* We don't generate a new state, but we still need
@@ -2196,30 +2252,30 @@ let known_state ?(redefine_qed=false) ~cache id =
let fp, cancel =
if delegate then
Slaves.build_proof
- ~loc ~drop_pt ~exn_info ~block_start ~block_stop ~name
+ ?loc ~drop_pt ~exn_info ~block_start ~block_stop ~name
else
- ProofTask.build_proof_here
- ~drop_pt exn_info loc block_stop, ref false
+ ProofTask.build_proof_here ?loc
+ ~drop_pt exn_info block_stop, ref false
in
qed.fproof <- Some (fp, cancel);
let proof =
Proof_global.close_future_proof ~feedback_id:id fp in
if not delegate then ignore(Future.compute fp);
reach view.next;
- vernac_interp id ~proof x;
- feedback ~id:(State id) Incomplete
+ stm_vernac_interp id ~proof 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; vernac_interp id x; Proof_global.discard_all ()
+ reach eop; stm_vernac_interp id x; Proof_global.discard_all ()
), `Yes, true
| `Sync (name, pua, reason) -> (fun () ->
log_processing_sync id name reason;
reach eop;
let wall_clock = Unix.gettimeofday () in
- record_pb_time name x.loc (wall_clock -. !wall_clock_last_fork);
+ record_pb_time name ?loc:x.loc (wall_clock -. !wall_clock_last_fork);
let proof =
match keep with
| VtDrop -> None
@@ -2234,25 +2290,25 @@ let known_state ?(redefine_qed=false) ~cache id =
if keep != VtKeepAsAxiom then
reach view.next;
let wall_clock2 = Unix.gettimeofday () in
- vernac_interp id ?proof x;
+ stm_vernac_interp id ?proof x;
let wall_clock3 = Unix.gettimeofday () in
- Aux_file.record_in_aux_at x.loc "proof_check_time"
+ Aux_file.record_in_aux_at ?loc:x.loc "proof_check_time"
(Printf.sprintf "%.3f" (wall_clock3 -. wall_clock2));
Proof_global.discard_all ()
), `Yes, true
| `MaybeASync (start, pua, nodes, name, delegate) -> (fun () ->
reach ~cache:`Shallow start;
(* no sections *)
- if List.is_empty (Environ.named_context (Global.env ()))
- then pi1 (aux (`ASync (start, pua, nodes, name, delegate))) ()
- else pi1 (aux (`Sync (name, pua, `NoPU_NoHint_NoES))) ()
+ if CList.is_empty (Environ.named_context (Global.env ()))
+ then Util.pi1 (aux (`ASync (start, pua, nodes, name, delegate))) ()
+ else Util.pi1 (aux (`Sync (name, pua, `NoPU_NoHint_NoES))) ()
), (if redefine_qed then `No else `Yes), true
in
aux (collect_proof keep (view.next, x) brname brinfo eop)
- | `Sideff (`Ast (x,_)) -> (fun () ->
- reach view.next; vernac_interp id x; update_global_env ()
+ | `Sideff (ReplayCommand x,_) -> (fun () ->
+ reach view.next; stm_vernac_interp id x; update_global_env ()
), cache, true
- | `Sideff (`Id origin) -> (fun () ->
+ | `Sideff (CherryPickEnv, origin) -> (fun () ->
reach view.next;
inject_non_pstate (pure_cherry_pick_non_pstate view.next origin);
), cache, true
@@ -2262,10 +2318,11 @@ let known_state ?(redefine_qed=false) ~cache id =
else cache_step in
State.define ?safe_id
~cache:cache_step ~redefine:redefine_qed ~feedback_processed step id;
- prerr_endline (fun () -> "reached: "^ Stateid.to_string id) in
+ stm_prerr_endline (fun () -> "reached: "^ Stateid.to_string id) in
reach ~redefine_qed id
end (* }}} *)
+[@@@ocaml.warning "+60"]
(********************************* STM API ************************************)
(******************************************************************************)
@@ -2277,7 +2334,7 @@ let init () =
Backtrack.record ();
Slaves.init ();
if Flags.async_proofs_is_master () then begin
- prerr_endline (fun () -> "Initializing workers");
+ stm_prerr_endline (fun () -> "Initializing workers");
Query.init ();
let opts = match !Flags.async_proofs_private_flags with
| None -> []
@@ -2299,20 +2356,20 @@ let observe id =
let e = CErrors.push e in
VCS.print ();
VCS.restore vcs;
- iraise e
+ Exninfo.iraise e
-let finish ?(print_goals=false) () =
+let finish () =
let head = VCS.current_branch () in
observe (VCS.get_branch_pos head);
- if print_goals then msg_notice (pr_open_cur_subgoals ());
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
- | { VCS.kind = `Edit (mode,_,_,_,_) } -> Proof_global.activate_proof_mode mode
- | { VCS.kind = `Proof (mode, _) } -> Proof_global.activate_proof_mode mode
+ | { 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"]
| _ -> ()
-
let wait () =
Slaves.wait_all_done ();
VCS.print ()
@@ -2329,9 +2386,9 @@ let rec join_admitted_proofs id =
let join () =
finish ();
wait ();
- prerr_endline (fun () -> "Joining the environment");
+ stm_prerr_endline (fun () -> "Joining the environment");
Global.join_safe_environment ();
- prerr_endline (fun () -> "Joining Admitted proofs");
+ stm_prerr_endline (fun () -> "Joining Admitted proofs");
join_admitted_proofs (VCS.get_branch_pos (VCS.current_branch ()));
VCS.print ();
VCS.print ()
@@ -2372,7 +2429,7 @@ let merge_proof_branch ~valid ?id qast keep brname =
let id = VCS.new_node ?id () in
VCS.merge id ~ours:(Qed (qed None)) brname;
VCS.delete_branch brname;
- VCS.propagate_sideff None;
+ VCS.propagate_sideff ~action:CherryPickEnv;
`Ok
| { VCS.kind = `Edit (mode, qed_id, master_id, _,_) } ->
let ofp =
@@ -2386,71 +2443,51 @@ let merge_proof_branch ~valid ?id qast keep brname =
VCS.checkout VCS.Branch.master;
`Unfocus qed_id
| { VCS.kind = `Master } ->
- iraise (State.exn_on ~valid Stateid.dummy (Proof_global.NoCurrentProof, Exninfo.null))
+ Exninfo.iraise (State.exn_on ~valid Stateid.dummy (Proof_global.NoCurrentProof, Exninfo.null))
(* 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 tty =
- if e = CErrors.Drop then iraise (e, info) else
+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;
VCS.print ();
- if tty && interactive () = `Yes then begin
- (* Hopefully the 1 to last state is valid *)
- Backtrack.back_safe ();
- VCS.checkout_shallowest_proof_branch ();
- end;
- VCS.print ();
anomaly(str"error with no safe_id attached:" ++ spc() ++
- CErrors.iprint_no_report (e, info))
+ CErrors.iprint_no_report (e, info) ++ str".")
| Some (safe_id, id) ->
- prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
+ stm_prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
VCS.restore vcs;
- if tty && interactive () = `Yes then begin
- (* We stay on a valid state *)
- Backtrack.backto safe_id;
- VCS.checkout_shallowest_proof_branch ();
- Reach.known_state ~cache:(interactive ()) safe_id;
- end;
VCS.print ();
- iraise (e, info)
+ Exninfo.iraise (e, info)
let snapshot_vio ldir long_f_dot_vo =
finish ();
if List.length (VCS.branches ()) > 1 then
- CErrors.errorlabstrm "stm" (str"Cannot dump a vio with open proofs");
+ 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 ())
let reset_task_queue = Slaves.reset_task_queue
(* Document building *)
-let process_transaction ?(newtip=Stateid.fresh ()) ~tty
+let process_transaction ?(newtip=Stateid.fresh ())
({ verbose; loc; expr } as x) c =
- prerr_endline (fun () -> "{{{ processing: "^ string_of_ppcmds (pr_ast x));
+ stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x);
let vcs = VCS.backup () in
try
let head = VCS.current_branch () in
VCS.checkout head;
let rc = begin
- prerr_endline (fun () ->
+ stm_prerr_endline (fun () ->
" classified as: " ^ string_of_vernac_classification c);
match c with
- (* PG stuff *)
- | VtStm(VtPG,false), VtNow -> vernac_interp Stateid.dummy x; `Ok
- | VtStm(VtPG,_), _ -> anomaly(str "PG command in script or VtLater")
(* Joining various parts of the document *)
| VtStm (VtJoinDocument, b), VtNow -> join (); `Ok
- | VtStm (VtFinish, b), VtNow -> finish (); `Ok
- | VtStm (VtWait, b), VtNow -> finish (); wait (); `Ok
- | VtStm (VtPrintDag, b), VtNow ->
- VCS.print ~now:true (); `Ok
- | VtStm (VtObserve id, b), VtNow -> observe id; `Ok
- | VtStm ((VtObserve _ | VtFinish | VtJoinDocument
- |VtPrintDag |VtWait),_), VtLater ->
- anomaly(str"classifier: join actions cannot be classified as VtLater")
-
+ | VtStm (VtWait, b), VtNow -> finish (); wait (); `Ok
+ | VtStm ((VtJoinDocument|VtWait),_), VtLater ->
+ anomaly(str"classifier: join actions cannot be classified as VtLater.")
+
(* Back *)
| VtStm (VtBack oid, true), w ->
let id = VCS.new_node ~id:newtip () in
@@ -2472,40 +2509,37 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
VCS.commit id (Alias (oid,x));
Backtrack.record (); if w == VtNow then finish (); `Ok
| VtStm (VtBack id, false), VtNow ->
- prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id);
+ 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
| VtStm (VtBack id, false), VtLater ->
- anomaly(str"classifier: VtBack + VtLater must imply part_of_script")
+ anomaly(str"classifier: VtBack + VtLater must imply part_of_script.")
(* Query *)
- | VtQuery (false,(report_id,route)), VtNow when tty = true ->
- finish ();
- (try Future.purify (vernac_interp report_id ~route)
- {x with verbose = true }
- with e when CErrors.noncritical e ->
- let e = CErrors.push e in
- iraise (State.exn_on ~valid:Stateid.dummy report_id e)); `Ok
- | VtQuery (false,(report_id,route)), VtNow ->
- (try vernac_interp report_id ~route x
- with e ->
- let e = CErrors.push e in
- iraise (State.exn_on ~valid:Stateid.dummy report_id e)); `Ok
- | VtQuery (true,(report_id,_)), w ->
- assert(Stateid.equal report_id Stateid.dummy);
+ | 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 ->
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) &&
VCS.((get_branch head).kind = `Master) &&
may_pierce_opaque x
- then `SkipQueue
+ then `SkipQueue
else `MainQueue in
VCS.commit id (mkTransCmd x [] false queue);
Backtrack.record (); if w == VtNow then finish (); `Ok
+
| VtQuery (false,_), VtLater ->
- anomaly(str"classifier: VtQuery + VtLater must imply part_of_script")
+ anomaly(str"classifier: VtQuery + VtLater must imply part_of_script.")
(* Proof *)
| VtStartProof (mode, guarantee, names), w ->
@@ -2519,10 +2553,10 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
VCS.branch bname (`Proof (mode, VCS.proof_nesting () + 1));
VCS.merge id ~ours:(Fork (x, bname, guarantee, names)) head
end;
- Proof_global.activate_proof_mode mode;
+ Proof_global.activate_proof_mode mode [@ocaml.warning "-3"];
Backtrack.record (); if w == VtNow then finish (); `Ok
| VtProofMode _, VtLater ->
- anomaly(str"VtProofMode must be executed VtNow")
+ anomaly(str"VtProofMode must be executed VtNow.")
| VtProofMode mode, VtNow ->
let id = VCS.new_node ~id:newtip () in
VCS.commit id (mkTransCmd x [] false `MainQueue);
@@ -2561,7 +2595,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
(* Side effect on all branches *)
| VtUnknown, _ when expr = VernacToplevelControl Drop ->
- vernac_interp (VCS.get_branch_pos head) x; `Ok
+ stm_vernac_interp (VCS.get_branch_pos head) x; `Ok
| VtSideff l, w ->
let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in
@@ -2570,10 +2604,10 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
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 replay = match x.expr with
- | VernacDefinition(_, _, DefineBody _) -> None
- | _ -> Some x in
- VCS.propagate_sideff ~replay;
+ let action = match x.expr with
+ | VernacDefinition(_, _, DefineBody _) -> CherryPickEnv
+ | _ -> ReplayCommand x in
+ VCS.propagate_sideff ~action;
VCS.checkout_shallowest_proof_branch ();
Backtrack.record (); if w == VtNow then finish (); `Ok
@@ -2587,7 +2621,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
VCS.checkout VCS.Branch.master;
let mid = VCS.get_branch_pos VCS.Branch.master in
Reach.known_state ~cache:(interactive ()) mid;
- vernac_interp id x;
+ stm_vernac_interp id x;
(* Vernac x may or may not start a proof *)
if not in_proof && Proof_global.there_are_pending_proofs () then
begin
@@ -2600,68 +2634,128 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
VCS.commit id (Fork (x,bname,opacity_of_produced_term x.expr,[]));
let proof_mode = default_proof_mode () in
VCS.branch bname (`Proof (proof_mode, VCS.proof_nesting () + 1));
- Proof_global.activate_proof_mode proof_mode;
+ 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 ~replay:(Some x);
+ VCS.propagate_sideff ~action:(ReplayCommand x);
VCS.checkout_shallowest_proof_branch ();
end in
State.define ~safe_id:head_id ~cache:`Yes step id;
Backtrack.record (); `Ok
| VtUnknown, VtLater ->
- anomaly(str"classifier: VtUnknown must imply VtNow")
+ anomaly(str"classifier: VtUnknown must imply VtNow.")
end in
- (* Proof General *)
- begin match expr with
- | VernacStm (PGLast _) ->
- if not (VCS.Branch.equal head VCS.Branch.master) then
- vernac_interp Stateid.dummy
- { verbose = true; loc = Loc.ghost; indentation = 0; strlen = 0;
- expr = VernacShow (ShowGoal OpenSubgoals) }
- | _ -> ()
- end;
- prerr_endline (fun () -> "processed }}}");
+ let pr_rc rc = match rc with
+ | `Ok -> Pp.(seq [str "newtip ("; str (Stateid.to_string (VCS.cur_tip ())); str ")"])
+ | _ -> Pp.(str "unfocus")
+ in
+ stm_pperr_endline (fun () -> str "processed with " ++ pr_rc rc ++ str " }}}");
VCS.print ();
rc
with e ->
let e = CErrors.push e in
- handle_failure e vcs tty
+ handle_failure e vcs
let get_ast id =
match VCS.visit id with
| { step = `Cmd { cast = { loc; expr } } }
| { step = `Fork (({ loc; expr }, _, _, _), _) }
| { step = `Qed ({ qast = { loc; expr } }, _) } ->
- Some (expr, loc)
+ Some (Loc.tag ?loc expr)
| _ -> None
let stop_worker n = Slaves.cancel_worker n
+(* We must parse on top of a state id, it should be something like:
+
+ - get parsing information for that state.
+ - feed the parsable / parser with the right parsing information.
+ - call the parser
+
+ Now, the invariant in ensured by the callers, but this is a bit
+ problematic.
+*)
+exception End_of_input
+
+let parse_sentence 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 *)
+ (* Reach.known_state ~cache:`Yes sid; *)
+ let cur_tip = VCS.cur_tip () in
+ let real_tip = !State.cur_id in
+ if not (Stateid.equal sid cur_tip) then
+ user_err ~hdr:"Stm.parse_sentence"
+ (str "Currently, the parsing api only supports parsing at the tip of the document." ++ fnl () ++
+ str "You wanted to parse at: " ++ str (Stateid.to_string sid) ++
+ str " but the current tip is: " ++ str (Stateid.to_string cur_tip)) ;
+ if not (Stateid.equal sid real_tip) && !Flags.debug && stm_debug () then
+ Feedback.msg_debug
+ (str "Warning, the real tip doesn't match the current tip." ++
+ str "You wanted to parse at: " ++ str (Stateid.to_string sid) ++
+ str " but the real tip is: " ++ str (Stateid.to_string real_tip) ++ fnl () ++
+ str "This is usually due to use of Stm.observe to evaluate a state different than the tip. " ++
+ 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
+ | None -> raise End_of_input
+ | Some (loc, cmd) -> Loc.tag ~loc cmd
+ with e when CErrors.noncritical e ->
+ let (e, info) = CErrors.push e in
+ Exninfo.iraise (e, info))
+ ()
+
(* You may need to know the len + indentation of previous command to compute
* the indentation of the current one.
* Eg. foo. bar.
* Here bar is indented of the indentation of foo + its strlen (4) *)
-let ind_len_of id =
- if Stateid.equal id Stateid.initial then 0
- else match (VCS.visit id).step with
- | `Cmd { ctac = true; cast = { indentation; strlen } } ->
- indentation + strlen
- | _ -> 0
-
-let add ~ontop ?newtip ?(check=ignore) verb eid s =
+let ind_len_loc_of_id sid =
+ if Stateid.equal sid Stateid.initial then None
+ else match (VCS.visit sid).step with
+ | `Cmd { ctac = true; cast = { indentation; strlen; loc } } ->
+ Some (indentation, strlen, loc)
+ | _ -> None
+
+(* the indentation logic works like this: if the beginning of the
+ command is different than the start we are in a new line, thus
+ indentation follows from the starting position. Otherwise, we use
+ the previous one plus the offset.
+
+ Note, this could maybe improved by handling more cases in
+ compute_indentation. *)
+
+let compute_indentation ?loc sid = Option.cata (fun loc ->
+ let open Loc in
+ (* The effective lenght is the lenght on the last line *)
+ let len = loc.ep - loc.bp in
+ let prev_indent = match ind_len_loc_of_id sid with
+ | None -> 0
+ | Some (i,l,p) -> i + l
+ in
+ (* Now if the line has not changed, the need to add the previous indent *)
+ let eff_indent = loc.bp - loc.bol_pos in
+ if loc.bol_pos = 0 then
+ eff_indent + prev_indent, len
+ else
+ eff_indent, len
+ ) (0, 0) loc
+
+let add ~ontop ?newtip verb (loc, ast) =
let cur_tip = VCS.cur_tip () in
if not (Stateid.equal ontop cur_tip) then
- (* For now, arbitrary edits should be announced with edit_at *)
- anomaly(str"Not yet implemented, the GUI should not try this");
- let indentation, strlen, loc, ast =
- vernac_parse ~indlen_prev:(fun () -> ind_len_of ontop) ?newtip eid s in
+ user_err ?loc ~hdr:"Stm.add"
+ (str "Stm.add called for a different state (" ++ str (Stateid.to_string ontop) ++
+ str ") than the tip: " ++ str (Stateid.to_string cur_tip) ++ str "." ++ fnl () ++
+ str "This is not supported yet, sorry.");
+ let indentation, strlen = compute_indentation ?loc ontop in
CWarnings.set_current_loc loc;
- check(loc,ast);
+ (* XXX: Classifiy vernac should be moved inside process transaction *)
let clas = classify_vernac ast in
let aast = { verbose = verb; indentation; strlen; loc; expr = ast } in
- match process_transaction ?newtip ~tty:false aast clas with
+ match process_transaction ?newtip aast clas with
| `Ok -> VCS.cur_tip (), `NewTip
| `Unfocus qed_id -> qed_id, `Unfocus (VCS.cur_tip ())
@@ -2673,25 +2767,24 @@ type focus = {
tip : Stateid.t
}
-let query ~at ?(report_with=(Stateid.dummy,default_route)) s =
+let query ~at ~route s =
Future.purify (fun s ->
if Stateid.equal at Stateid.dummy then finish ()
else Reach.known_state ~cache:`Yes at;
- let newtip, route = report_with in
- let indentation, strlen, loc, ast = vernac_parse ~newtip ~route 0 s in
+ let loc, ast = parse_sentence at s in
+ let indentation, strlen = compute_indentation ?loc at in
CWarnings.set_current_loc loc;
let clas = classify_vernac ast in
let aast = { verbose = true; indentation; strlen; loc; expr = ast } in
match clas with
| VtStm (w,_), _ ->
- ignore(process_transaction ~tty:false aast (VtStm (w,false), VtNow))
+ ignore(process_transaction aast (VtStm (w,false), VtNow))
| _ ->
- ignore(process_transaction
- ~tty:false aast (VtQuery (false,report_with), VtNow)))
+ ignore(process_transaction aast (VtQuery (false, route), VtNow)))
s
let edit_at id =
- if Stateid.equal id Stateid.dummy then anomaly(str"edit_at dummy") else
+ if Stateid.equal id Stateid.dummy then anomaly(str"edit_at dummy.") else
let vcs = VCS.backup () in
let on_cur_branch id =
let rec aux cur =
@@ -2722,7 +2815,7 @@ let edit_at id =
if Stateid.equal tip Stateid.initial then tip else
match VCS.visit tip with
| { step = (`Fork _ | `Qed _) } -> tip
- | { step = `Sideff (`Ast(_,id)) } -> id
+ | { step = `Sideff (ReplayCommand _,id) } -> id
| { step = `Sideff _ } -> tip
| { next } -> master_for_br root next in
let reopen_branch start at_id mode qed_id tip old_branch =
@@ -2730,7 +2823,7 @@ let edit_at id =
(* Hum, this should be the real start_id in the cluster and not next *)
match VCS.visit qed_id with
| { step = `Qed ({ fproof = Some (_,cs); keep },_) } -> start, cs, keep
- | _ -> anomaly (str "ProofTask not ending with Qed") in
+ | _ -> anomaly (str "ProofTask not ending with Qed.") in
VCS.branch ~root:master_id ~pos:id
VCS.edit_branch (`Edit (mode, qed_id, master_id, keep, old_branch));
VCS.delete_boxes_of id;
@@ -2782,7 +2875,7 @@ let edit_at id =
end else if is_ancestor_of_cur_branch id then begin
backto id (Some bn)
end else begin
- anomaly(str"Cannot leave an `Edit branch open")
+ anomaly(str"Cannot leave an `Edit branch open.")
end
| true, None, _ ->
if on_cur_branch id then begin
@@ -2793,7 +2886,7 @@ let edit_at id =
end else if is_ancestor_of_cur_branch id then begin
backto id None
end else begin
- anomaly(str"Cannot leave an `Edit branch open")
+ anomaly(str"Cannot leave an `Edit branch open.")
end
| false, None, Some(_,bn) -> backto id (Some bn)
| false, None, None -> backto id None
@@ -2806,42 +2899,21 @@ let edit_at id =
| None ->
VCS.print ();
anomaly (str ("edit_at "^Stateid.to_string id^": ") ++
- CErrors.print_no_report e)
+ CErrors.print_no_report e ++ str ".")
| Some (_, id) ->
- prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
+ stm_prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
VCS.restore vcs;
VCS.print ();
- iraise (e, info)
+ Exninfo.iraise (e, info)
let backup () = VCS.backup ()
let restore d = VCS.restore d
+let get_current_state () = VCS.cur_tip ()
+
(*********************** TTY API (PG, coqtop, coqc) ***************************)
(******************************************************************************)
-let interp verb (loc,e) =
- let clas = classify_vernac e in
- let aast = { verbose = verb; indentation = 0; strlen = 0; loc; expr = e } in
- let rc = process_transaction ~tty:true aast clas in
- if rc <> `Ok then anomaly(str"tty loop can't be mixed with the STM protocol");
- if interactive () = `Yes ||
- (!Flags.async_proofs_mode = Flags.APoff &&
- !Flags.compilation_mode = Flags.BuildVo) then
- let vcs = VCS.backup () in
- let print_goals =
- verb && match clas with
- | VtQuery _, _ -> false
- | (VtProofStep _ | VtStm (VtBack _, _) | VtStartProof _), _ -> true
- | _ -> not !Flags.coqtop_ui in
- try finish ~print_goals ()
- with e ->
- let e = CErrors.push e in
- handle_failure e vcs true
-
-let finish () = finish ()
-
-let get_current_state () = VCS.cur_tip ()
-
let current_proof_depth () =
let head = VCS.current_branch () in
match VCS.get_branch head with
@@ -2862,104 +2934,13 @@ let proofname b = match VCS.get_branch b with
| _ -> None
let get_all_proof_names () =
- List.map unmangle (List.map_filter proofname (VCS.branches ()))
-
-let get_current_proof_name () =
- Option.map unmangle (proofname (VCS.current_branch ()))
-
-let get_script prf =
- let branch, test =
- match prf with
- | None -> VCS.Branch.master, fun _ -> true
- | Some name -> VCS.current_branch (),fun nl -> nl=[] || List.mem name nl in
- let rec find acc id =
- if Stateid.equal id Stateid.initial ||
- Stateid.equal id Stateid.dummy then acc else
- let view = VCS.visit id in
- match view.step with
- | `Fork((_,_,_,ns), _) when test ns -> acc
- | `Qed (qed, proof) -> find [qed.qast.expr, (VCS.get_info id).n_goals] proof
- | `Sideff (`Ast (x,_)) ->
- find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next
- | `Sideff (`Id id) -> find acc id
- | `Cmd {cast = x; ctac} when ctac -> (* skip non-tactics *)
- find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next
- | `Cmd _ -> find acc view.next
- | `Alias (id,_) -> find acc id
- | `Fork _ -> find acc view.next
- in
- find [] (VCS.get_branch_pos branch)
-
-(* indentation code for Show Script, initially contributed
- by D. de Rauglaudre *)
-
-let indent_script_item ((ng1,ngl1),nl,beginend,ppl) (cmd,ng) =
- (* ng1 : number of goals remaining at the current level (before cmd)
- ngl1 : stack of previous levels with their remaining goals
- ng : number of goals after the execution of cmd
- beginend : special indentation stack for { } *)
- let ngprev = List.fold_left (+) ng1 ngl1 in
- let new_ngl =
- if ng > ngprev then
- (* We've branched *)
- (ng - ngprev + 1, ng1 - 1 :: ngl1)
- else if ng < ngprev then
- (* A subgoal have been solved. Let's compute the new current level
- by discarding all levels with 0 remaining goals. *)
- let rec loop = function
- | (0, ng2::ngl2) -> loop (ng2,ngl2)
- | p -> p
- in loop (ng1-1, ngl1)
- else
- (* Standard case, same goal number as before *)
- (ng1, ngl1)
- in
- (* When a subgoal have been solved, separate this block by an empty line *)
- let new_nl = (ng < ngprev)
- in
- (* Indentation depth *)
- let ind = List.length ngl1
- in
- (* Some special handling of bullets and { }, to get a nicer display *)
- let pred n = max 0 (n-1) in
- let ind, nl, new_beginend = match cmd with
- | VernacSubproof _ -> pred ind, nl, (pred ind)::beginend
- | VernacEndSubproof -> List.hd beginend, false, List.tl beginend
- | VernacBullet _ -> pred ind, nl, beginend
- | _ -> ind, nl, beginend
- in
- let pp =
- (if nl then fnl () else mt ()) ++
- (hov (ind+1) (str (String.make ind ' ') ++ Ppvernac.pr_vernac cmd))
- in
- (new_ngl, new_nl, new_beginend, pp :: ppl)
-
-let show_script ?proof () =
- try
- let prf =
- try match proof with
- | None -> Some (Pfedit.get_current_proof_name ())
- | Some (p,_) -> Some (p.Proof_global.id)
- with Proof_global.NoCurrentProof -> None
- in
- let cmds = get_script prf in
- let _,_,_,indented_cmds =
- List.fold_left indent_script_item ((1,[]),false,[],[]) cmds
- in
- let indented_cmds = List.rev (indented_cmds) in
- msg_notice (v 0 (prlist_with_sep fnl (fun x -> x) indented_cmds))
- with Vcs_aux.Expired -> ()
+ List.map unmangle (CList.map_filter proofname (VCS.branches ()))
(* Export hooks *)
let state_computed_hook = Hooks.state_computed_hook
let state_ready_hook = Hooks.state_ready_hook
-let parse_error_hook = Hooks.parse_error_hook
-let execution_error_hook = Hooks.execution_error_hook
let forward_feedback_hook = Hooks.forward_feedback_hook
-let process_error_hook = Hooks.process_error_hook
-let interp_hook = Hooks.interp_hook
-let with_fail_hook = Hooks.with_fail_hook
let unreachable_state_hook = Hooks.unreachable_state_hook
-let get_fix_exn () = !State.fix_exn_ref
-let tactic_being_run_hook = Hooks.tactic_being_run_hook
+let () = Hook.set Obligations.stm_get_fix_exn (fun () -> !State.fix_exn_ref)
+
(* vim:set foldmethod=marker: *)
diff --git a/stm/stm.mli b/stm/stm.mli
index b8a2a38596..188b176bab 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -6,31 +6,35 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Vernacexpr
open Names
-open Feedback
-open Loc
(** state-transaction-machine interface *)
-(* [add ontop check vebose eid s] adds a new command [s] on the state [ontop]
- having edit id [eid]. [check] is called on the AST.
- The [ontop] parameter is just for asserting the GUI is on sync, but
- will eventually call edit_at on the fly if needed.
- The sentence [s] is parsed in the state [ontop].
- If [newtip] is provided, then the returned state id is guaranteed to be
- [newtip] *)
-val add :
- ontop:Stateid.t -> ?newtip:Stateid.t ->
- ?check:(vernac_expr located -> unit) ->
- bool -> edit_id -> string ->
- Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]
-
-(* parses and executes a command at a given state, throws away its side effects
- but for the printings. Feedback is sent with report_with (defaults to dummy
- state id) *)
+(* [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 ->
+ Vernacexpr.vernac_expr Loc.located
+
+(* Reminder: A parsable [pa] is constructed using
+ [Pcoq.Gram.coq_parsable stream], where [stream : char Stream.t]. *)
+
+exception End_of_input
+
+(* [add ~ontop ?newtip verbose cmd] adds a new command [cmd] ontop of
+ the state [ontop].
+ The [ontop] parameter just asserts that the GUI is on
+ 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 ->
+ bool -> Vernacexpr.vernac_expr Loc.located ->
+ 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 :
- at:Stateid.t -> ?report_with:(Stateid.t * Feedback.route_id) -> string -> unit
+ 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
the requested id is the new document tip hence the document portion following
@@ -80,7 +84,7 @@ val get_current_state : unit -> Stateid.t
val init : unit -> unit
(* This returns the node at that position *)
-val get_ast : Stateid.t -> (Vernacexpr.vernac_expr * Loc.t) option
+val get_ast : Stateid.t -> (Vernacexpr.vernac_expr Loc.located) option
(* Filename *)
val set_compilation_hints : string -> unit
@@ -182,15 +186,10 @@ val register_proof_block_delimiter :
* the name of the Task(s) above) *)
val state_computed_hook : (Stateid.t -> in_cache:bool -> unit) Hook.t
-val parse_error_hook :
- (Feedback.edit_or_state_id -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t
-val execution_error_hook : (Stateid.t -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t
val unreachable_state_hook : (Stateid.t -> Exninfo.iexn -> unit) Hook.t
+
(* ready means that master has it at hand *)
val state_ready_hook : (Stateid.t -> unit) Hook.t
-(* called with true before and with false after a tactic explicitly
- * in the document is run *)
-val tactic_being_run_hook : (bool -> unit) Hook.t
(* Messages from the workers to the master *)
val forward_feedback_hook : (Feedback.feedback -> unit) Hook.t
@@ -203,22 +202,6 @@ type state = {
val state_of_id :
Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ]
-(** read-eval-print loop compatible interface ****************************** **)
-
-(* Adds a new line to the document. It replaces the core of Vernac.interp.
- [finish] is called as the last bit of this function if the system
- is running interactively (-emacs or coqtop). *)
-val interp : bool -> vernac_expr located -> unit
-
(* Queries for backward compatibility *)
val current_proof_depth : unit -> int
val get_all_proof_names : unit -> Id.t list
-val get_current_proof_name : unit -> Id.t option
-val show_script : ?proof:Proof_global.closed_proof -> unit -> unit
-
-(* Hooks to be set by other Coq components in order to break file cycles *)
-val process_error_hook : Future.fix_exn Hook.t
-val interp_hook : (?verbosely:bool -> ?proof:Proof_global.closed_proof ->
- Loc.t * Vernacexpr.vernac_expr -> unit) Hook.t
-val with_fail_hook : (bool -> (unit -> unit) -> unit) Hook.t
-val get_fix_exn : unit -> (Exninfo.iexn -> Exninfo.iexn)
diff --git a/stm/stm.mllib b/stm/stm.mllib
index 939ee187ae..72b5380162 100644
--- a/stm/stm.mllib
+++ b/stm/stm.mllib
@@ -4,8 +4,8 @@ Vcs
TQueue
WorkerPool
Vernac_classifier
-Lemmas
CoqworkmgrApi
+WorkerLoop
AsyncTaskQueue
Stm
ProofBlockDelimiter
diff --git a/stm/tQueue.ml b/stm/tQueue.ml
index 8abf8e9559..56e8c41acd 100644
--- a/stm/tQueue.ml
+++ b/stm/tQueue.ml
@@ -88,7 +88,7 @@ let broadcast { lock = m; cond = c } =
let push { queue = q; lock = m; cond = c; release } x =
if release then CErrors.anomaly(Pp.str
- "TQueue.push while being destroyed! Only 1 producer/destroyer allowed");
+ "TQueue.push while being destroyed! Only 1 producer/destroyer allowed.");
Mutex.lock m;
PriorityQueue.push q x;
Condition.broadcast c;
diff --git a/stm/tacworkertop.ml b/stm/tacworkertop.ml
index 208d04a0bf..186c8f8b7c 100644
--- a/stm/tacworkertop.ml
+++ b/stm/tacworkertop.ml
@@ -8,11 +8,7 @@
module W = AsyncTaskQueue.MakeWorker(Stm.TacTask)
-let () = Coqtop.toploop_init := (fun args ->
- Flags.make_silent true;
- W.init_stdout ();
- CoqworkmgrApi.init !Flags.async_proofs_worker_priority;
- args)
+let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
let () = Coqtop.toploop_run := W.main_loop
diff --git a/stm/vcs.ml b/stm/vcs.ml
index ef548a0031..5d4a812fac 100644
--- a/stm/vcs.ml
+++ b/stm/vcs.ml
@@ -74,8 +74,6 @@ module Dag = Dag.Make(OT)
type id = OT.t
-module NodeSet = Dag.NodeSet
-
module Branch =
struct
type t = string
@@ -115,7 +113,7 @@ let add_node vcs id edges =
let get_branch vcs head =
try BranchMap.find head vcs.heads
- with Not_found -> anomaly (str"head " ++ str head ++ str" not found")
+ with Not_found -> anomaly (str"head " ++ str head ++ str" not found.")
let reset_branch vcs head id =
let map name h =
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 3bbed974f9..c2ebea961f 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -10,7 +10,7 @@ open Vernacexpr
open CErrors
open Pp
-let default_proof_mode () = Proof_global.get_default_proof_mode_name ()
+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 ""
@@ -30,12 +30,8 @@ let string_of_vernac_type = function
"ProofStep " ^ string_of_parallel parallel ^
Option.default "" proof_block_detection
| VtProofMode s -> "ProofMode " ^ s
- | VtQuery (b,(id,route)) ->
- "Query " ^ string_of_in_script b ^ " report " ^ Stateid.to_string id ^
- " route " ^ string_of_int route
- | VtStm ((VtFinish|VtJoinDocument|VtObserve _|VtPrintDag|VtWait), b) ->
- "Stm " ^ string_of_in_script b
- | VtStm (VtPG, b) -> "Stm PG " ^ string_of_in_script b
+ | VtQuery (b, route) -> "Query " ^ string_of_in_script b ^ " route " ^ string_of_int route
+ | VtStm ((VtJoinDocument|VtWait), b) -> "Stm " ^ string_of_in_script b
| VtStm (VtBack _, b) -> "Stm Back " ^ string_of_in_script b
let string_of_vernac_when = function
@@ -52,12 +48,6 @@ let declare_vernac_classifier
=
classifiers := !classifiers @ [s,f]
-let elide_part_of_script_and_now (a, _) =
- match a with
- | VtQuery (_,id) -> VtQuery (false,id), VtNow
- | VtStm (x, _) -> VtStm (x, false), VtNow
- | x -> x, VtNow
-
let make_polymorphic (a, b as x) =
match a with
| VtStartProof (x, _, ids) ->
@@ -69,23 +59,14 @@ let set_undo_classifier f = undo_classifier := f
let rec classify_vernac e =
let static_classifier e = match e with
- (* PG compatibility *)
- | VernacUnsetOption (["Silent"]|["Undo"]|["Printing";"Depth"])
- | VernacSetOption ((["Silent"]|["Undo"]|["Printing";"Depth"]),_)
- when !Flags.print_emacs -> VtStm(VtPG,false), VtNow
(* Univ poly compatibility: we run it now, so that we can just
* look at Flags in stm.ml. Would be nicer to have the stm
* look at the entire dag to detect this option. *)
| VernacSetOption (["Universe"; "Polymorphism"],_)
| VernacUnsetOption (["Universe"; "Polymorphism"]) -> VtSideff [], VtNow
(* Stm *)
- | VernacStm Finish -> VtStm (VtFinish, true), VtNow
- | VernacStm Wait -> VtStm (VtWait, true), VtNow
+ | VernacStm Wait -> VtStm (VtWait, true), VtNow
| VernacStm JoinDocument -> VtStm (VtJoinDocument, true), VtNow
- | VernacStm PrintDag -> VtStm (VtPrintDag, true), VtNow
- | VernacStm (Observe id) -> VtStm (VtObserve id, true), VtNow
- | VernacStm (Command x) -> elide_part_of_script_and_now (classify_vernac x)
- | VernacStm (PGLast x) -> fst (classify_vernac x), VtNow
(* Nested vernac exprs *)
| VernacProgram e -> classify_vernac e
| VernacLocal (_,e) -> classify_vernac e
@@ -109,8 +90,7 @@ let rec classify_vernac e =
| VernacEndProof _ | VernacExactProof _ -> VtQed VtKeep, VtLater
(* Query *)
| VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _
- | VernacCheckMayEval _ ->
- VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater
+ | VernacCheckMayEval _ -> VtQuery (true,Feedback.default_route), VtLater
(* ProofStep *)
| VernacProof _
| VernacFocus _ | VernacUnfocus
@@ -135,7 +115,7 @@ let rec classify_vernac e =
VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity,[i]), VtLater
| VernacDefinition (_,((_,i),_),ProveBody _) ->
VtStartProof(default_proof_mode (),GuaranteesOpacity,[i]), VtLater
- | VernacStartTheoremProof (_,l,_) ->
+ | VernacStartTheoremProof (_,l) ->
let ids =
CList.map_filter (function (Some ((_,i),pl), _) -> Some i | _ -> None) l in
VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater
@@ -159,7 +139,7 @@ let rec classify_vernac e =
let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map (fun (id, _) -> snd id) l) l) in
VtSideff ids, VtLater
| VernacDefinition (_,((_,id),_),DefineBody _) -> VtSideff [id], VtLater
- | VernacInductive (_,_,l) ->
+ | VernacInductive (_, _,_,l) ->
let ids = List.map (fun (((_,((_,id),_)),_,_,_,cl),_) -> id :: match cl with
| Constructors l -> List.map (fun (_,((_,id),_)) -> id) l
| RecordDecl (oid,l) -> (match oid with Some (_,x) -> [x] | _ -> []) @
@@ -219,19 +199,17 @@ let rec classify_vernac e =
(* What are these? *)
| VernacToplevelControl _
| VernacRestoreState _
- | VernacWriteState _
- | VernacError _ -> VtUnknown, VtNow
+ | VernacWriteState _ -> VtUnknown, VtNow
(* Plugins should classify their commands *)
| VernacExtend (s,l) ->
try List.assoc s !classifiers l ()
- with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s))
+ with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".")
in
let res = static_classifier e in
if Flags.is_universe_polymorphism () then
make_polymorphic res
else res
-let classify_as_query =
- VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater
+let classify_as_query = VtQuery (true,Feedback.default_route), VtLater
let classify_as_sideeff = VtSideff [], VtLater
let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}, VtLater
diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml
index dbc46c0c53..9507e90ba7 100644
--- a/stm/vio_checking.ml
+++ b/stm/vio_checking.ml
@@ -24,7 +24,7 @@ end
module Pool = Map.Make(IntOT)
let schedule_vio_checking j fs =
- if j < 1 then CErrors.error "The number of workers must be bigger than 0";
+ if j < 1 then CErrors.user_err Pp.(str "The number of workers must be bigger than 0");
let jobs = ref [] in
List.iter (fun f ->
let f =
@@ -98,7 +98,7 @@ let schedule_vio_checking j fs =
exit !rc
let schedule_vio_compilation j fs =
- if j < 1 then CErrors.error "The number of workers must be bigger than 0";
+ if j < 1 then CErrors.user_err Pp.(str "The number of workers must be bigger than 0");
let jobs = ref [] in
List.iter (fun f ->
let f =
@@ -107,7 +107,7 @@ let schedule_vio_compilation j fs =
let long_f_dot_v = Loadpath.locate_file (f^".v") in
let aux = Aux_file.load_aux_file_for long_f_dot_v in
let eta =
- try float_of_string (Aux_file.get aux Loc.ghost "vo_compile_time")
+ try float_of_string (Aux_file.get aux "vo_compile_time")
with Not_found -> 0.0 in
jobs := (f, eta) :: !jobs)
fs;
diff --git a/stm/workerLoop.ml b/stm/workerLoop.ml
new file mode 100644
index 0000000000..64121eb3d5
--- /dev/null
+++ b/stm/workerLoop.ml
@@ -0,0 +1,19 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+let rec parse = function
+ | "--xml_format=Ppcmds" :: rest -> parse rest
+ | x :: rest -> x :: parse rest
+ | [] -> []
+
+let loop init args =
+ let args = parse args in
+ Flags.quiet := true;
+ init ();
+ CoqworkmgrApi.init !Flags.async_proofs_worker_priority;
+ args
diff --git a/stm/workerLoop.mli b/stm/workerLoop.mli
new file mode 100644
index 0000000000..53f7459357
--- /dev/null
+++ b/stm/workerLoop.mli
@@ -0,0 +1,9 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+val loop : (unit -> unit) -> string list -> string list
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 08:56:05 +0000