aboutsummaryrefslogtreecommitdiff
path: root/stm
diff options
context:
space:
mode:
Diffstat (limited to 'stm')
-rw-r--r--stm/asyncTaskQueue.ml28
-rw-r--r--stm/lemmas.ml38
-rw-r--r--stm/spawned.ml4
-rw-r--r--stm/stm.ml102
-rw-r--r--stm/tQueue.ml2
-rw-r--r--stm/vcs.ml2
-rw-r--r--stm/vernac_classifier.ml2
-rw-r--r--stm/vio_checking.ml4
-rw-r--r--stm/workerPool.ml4
9 files changed, 110 insertions, 76 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index a7b381ad62..fa6422cdc5 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
+open CErrors
open Pp
open Util
@@ -229,10 +229,8 @@ module Make(T : Task) = struct
| (Die | TQueue.BeingDestroyed) ->
giveback_exec_token (); kill proc; exit ()
| Sys_error _ | Invalid_argument _ | End_of_file ->
- giveback_exec_token ();
T.on_task_cancellation_or_expiration_or_slave_death !last_task;
- kill proc;
- exit ()
+ giveback_exec_token (); kill proc; exit ()
end
module Pool = WorkerPool.Make(Model)
@@ -300,11 +298,27 @@ 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 debug_with_pid = Feedback.(function
+ | { contents = Message(Debug, loc, pp) } as fb ->
+ { 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 fb) []; flush oc in
- Feedback.set_feeder (fun x -> slave_feeder (Option.get !slave_oc) x);
+ 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;
+ (* We ask master to allocate universe identifiers *)
Universes.set_remote_new_univ_level (bufferize (fun () ->
marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel;
match unmarshal_more_data (Option.get !slave_ic) with
@@ -343,7 +357,7 @@ module Make(T : Task) = struct
let with_n_workers n f =
let q = create n in
try let rc = f q in destroy q; rc
- with e -> let e = Errors.push e in destroy q; iraise e
+ with e -> let e = CErrors.push e in destroy q; iraise e
let n_workers { active } = Pool.n_workers active
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 6b78ce72cc..50f2b82c3b 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -9,7 +9,7 @@
(* Created by Hugo Herbelin from contents related to lemma proofs in
file command.ml, Aug 2009 *)
-open Errors
+open CErrors
open Util
open Flags
open Pp
@@ -37,8 +37,8 @@ type 'a declaration_hook = Decl_kinds.locality -> Globnames.global_reference ->
let mk_hook hook = hook
let call_hook fix_exn hook l c =
try hook l c
- with e when Errors.noncritical e ->
- let e = Errors.push e in
+ with e when CErrors.noncritical e ->
+ let e = CErrors.push e in
iraise (fix_exn e)
(* Support for mutually proved theorems *)
@@ -106,7 +106,7 @@ let find_mutually_recursive_statements thms =
(* 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_betadeltaiota_stack env Evd.empty c))
+ (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 ->
@@ -120,7 +120,7 @@ let find_mutually_recursive_statements thms =
[]) 0 (List.rev whnf_hyp_hds)) in
let ind_ccl =
let cclenv = push_rel_context hyps (Global.env()) in
- let whnf_ccl,_ = whd_betadeltaiota_stack cclenv Evd.empty ccl 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
@@ -210,8 +210,8 @@ let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook =
definition_message id;
Option.iter (Universes.register_universe_binders r) pl;
call_hook (fun exn -> exn) hook l r
- with e when Errors.noncritical e ->
- let e = Errors.push e in
+ 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"
@@ -252,10 +252,14 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,
| Some body ->
let body = norm body in
let k = Kindops.logical_kind_of_goal_kind kind in
- let body_i = match kind_of_term body with
+ 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
@@ -480,6 +484,18 @@ let start_proof_com kind thms 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 =
@@ -493,7 +509,8 @@ let save_proof ?proof = function
error "Admitted requires an explicit statement";
let typ = Option.get const_entry_type in
let ctx = Evd.evar_context_universe_context (fst universes) in
- Admitted(id, k, (const_entry_secctx, pi2 k, (typ, ctx), None), universes)
+ 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
@@ -502,7 +519,8 @@ let save_proof ?proof = function
let pproofs, _univs =
Proof_global.return_proof ~allow_partial:true () in
let sec_vars =
- match Pfedit.get_used_variables(), pproofs with
+ 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
diff --git a/stm/spawned.ml b/stm/spawned.ml
index 2eae6f5e24..c5bd5f6f96 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 Errors.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 ->
- Errors.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 928a0dd6f5..c53bd958aa 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -16,7 +16,7 @@ let pp_to_richpp = Richpp.richpp_of_pp
let str_to_richpp = Richpp.richpp_of_string
open Vernacexpr
-open Errors
+open CErrors
open Pp
open Names
open Util
@@ -37,10 +37,12 @@ let state_computed, state_computed_hook = Hook.make
let state_ready, state_ready_hook = Hook.make
~default:(fun state_id -> ()) ()
-let forward_feedback, forward_feedback_hook = Hook.make
- ~default:(function
+let forward_feedback, forward_feedback_hook =
+ let m = Mutex.create () in
+ Hook.make ~default:(function
| { id = id; route; contents } ->
- feedback ~id:id ~route contents) ()
+ 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 ->
@@ -119,7 +121,7 @@ let vernac_interp ?proof id ?route { verbose; loc; expr } =
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 = Errors.push e in
+ let e = CErrors.push e in
iraise Hooks.(call_process_error_once e)
end
@@ -149,8 +151,8 @@ let vernac_parse ?(indlen_prev=fun() -> 0) ?newtip ?route eid s =
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 Errors.noncritical e ->
- let (e, info) = Errors.push e in
+ 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))
@@ -892,7 +894,7 @@ end = struct (* {{{ *)
if Proof_global.there_are_pending_proofs () then
VCS.goals id (Proof_global.get_open_goals ())
with e ->
- let (e, info) = Errors.push e in
+ let (e, info) = CErrors.push e in
let good_id = !cur_id in
VCS.reached id;
let ie =
@@ -1038,7 +1040,7 @@ end = struct (* {{{ *)
| _ -> VtUnknown, VtNow
with
| Not_found ->
- Errors.errorlabstrm "undo_vernac_classifier"
+ CErrors.errorlabstrm "undo_vernac_classifier"
(str "Cannot undo")
end (* }}} *)
@@ -1072,7 +1074,7 @@ let record_pb_time proof_name loc time =
end
exception RemoteException of std_ppcmds
-let _ = Errors.register_handler (function
+let _ = CErrors.register_handler (function
| RemoteException ppcmd -> ppcmd
| _ -> raise Unhandled)
@@ -1106,7 +1108,7 @@ let proof_block_delimiters = ref []
let register_proof_block_delimiter name static dynamic =
if List.mem_assoc name !proof_block_delimiters then
- Errors.errorlabstrm "STM" (str "Duplicate block delimiter " ++ str name);
+ CErrors.errorlabstrm "STM" (str "Duplicate block delimiter " ++ str name);
proof_block_delimiters := (name, (static,dynamic)) :: !proof_block_delimiters
let mk_doc_node id = function
@@ -1141,7 +1143,7 @@ let detect_proof_block id name =
VCS.create_proof_block decl name
end
with Not_found ->
- Errors.errorlabstrm "STM"
+ CErrors.errorlabstrm "STM"
(str "Unknown proof block delimiter " ++ str name)
)
(****************************** THE SCHEDULER *********************************)
@@ -1326,8 +1328,8 @@ end = struct (* {{{ *)
end;
RespBuiltProof(proof,time)
with
- | e when Errors.noncritical e || e = Stack_overflow ->
- let (e, info) = Errors.push e in
+ | e when CErrors.noncritical e || e = Stack_overflow ->
+ let (e, info) = CErrors.push e in
(* This can happen if the proof is broken. The error has also been
* signalled as a feedback, hence we can silently recover *)
let e_error_at, e_safe_id = match Stateid.get info with
@@ -1437,8 +1439,8 @@ end = struct (* {{{ *)
let check_task_aux extra name l i =
let { Stateid.stop; document; loc; name = r_name }, drop = List.nth l i in
- msg_info(
- str(Printf.sprintf "Checking task %d (%s%s) of %s" i r_name extra name));
+ Flags.if_verbose msg_info
+ (str(Printf.sprintf "Checking task %d (%s%s) of %s" i r_name extra name));
VCS.restore document;
let start =
let rec aux cur =
@@ -1466,7 +1468,7 @@ end = struct (* {{{ *)
`OK proof
end
with e ->
- let (e, info) = Errors.push e in
+ let (e, info) = CErrors.push e in
(try match Stateid.get info with
| None ->
msg_error (
@@ -1706,7 +1708,7 @@ end = struct (* {{{ *)
List.for_all (Context.Named.Declaration.for_all (Evarutil.is_ground_term sigma0))
Evd.(evar_context g))
then
- Errors.errorlabstrm "STM" (strbrk("the par: goal selector supports ground "^
+ CErrors.errorlabstrm "STM" (strbrk("the par: goal selector supports ground "^
"goals only"))
else begin
let (i, ast) = r_ast in
@@ -1719,9 +1721,9 @@ end = struct (* {{{ *)
let t = Evarutil.nf_evar sigma t in
if Evarutil.is_ground_term sigma t then
RespBuiltSubProof (t, Evd.evar_universe_context sigma)
- else Errors.errorlabstrm "STM" (str"The solution is not ground")
+ else CErrors.errorlabstrm "STM" (str"The solution is not ground")
end) ()
- with e when Errors.noncritical e -> RespError (Errors.print e)
+ with e when CErrors.noncritical e -> RespError (CErrors.print e)
let name_of_task { t_name } = t_name
let name_of_request { r_name } = r_name
@@ -1773,7 +1775,7 @@ end = struct (* {{{ *)
let gid = Goal.goal g in
let f =
try List.assoc gid res
- with Not_found -> Errors.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
@@ -1842,8 +1844,8 @@ end = struct (* {{{ *)
try
vernac_interp r_for { r_what with verbose = true };
feedback ~id:(State r_for) Processed
- with e when Errors.noncritical e ->
- let e = Errors.push e in
+ 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))
@@ -2056,7 +2058,7 @@ let known_state ?(redefine_qed=false) ~cache id =
| _ -> assert false
end
with Not_found ->
- Errors.errorlabstrm "STM"
+ CErrors.errorlabstrm "STM"
(str "Unknown proof block delimiter " ++ str name)
in
@@ -2068,8 +2070,8 @@ let known_state ?(redefine_qed=false) ~cache id =
then f ()
else
try f ()
- with e when Errors.noncritical e ->
- let ie = Errors.push e in
+ with e when CErrors.noncritical e ->
+ let ie = CErrors.push e in
error_absorbing_tactic id blockname ie in
(* Absorb errors from f x *)
let resilient_command f x =
@@ -2079,7 +2081,7 @@ let known_state ?(redefine_qed=false) ~cache id =
then f x
else
try f x
- with e when Errors.noncritical e -> () in
+ with e when CErrors.noncritical e -> () in
(* ugly functions to process nested lemmas, i.e. hard to reproduce
* side effects *)
@@ -2089,13 +2091,13 @@ let known_state ?(redefine_qed=false) ~cache id =
let inject_non_pstate (s,l) =
Summary.unfreeze_summary s; Lib.unfreeze l; update_global_env ()
in
- let rec pure_cherry_pick_non_pstate id = Future.purify (fun id ->
+ 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);
- reach id;
+ reach ~safe_id id;
cherry_pick_non_pstate ()) id
(* traverses the dag backward from nodes being already calculated *)
- and reach ?(redefine_qed=false) ?(cache=cache) id =
+ and reach ?safe_id ?(redefine_qed=false) ?(cache=cache) id =
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);
@@ -2146,8 +2148,8 @@ let known_state ?(redefine_qed=false) ~cache id =
reach ~cache:`Shallow prev;
reach view.next;
(try vernac_interp id x;
- with e when Errors.noncritical e ->
- let (e, info) = Errors.push e in
+ 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));
wall_clock_last_fork := Unix.gettimeofday ()
@@ -2240,13 +2242,13 @@ let known_state ?(redefine_qed=false) ~cache id =
), cache, true
| `Sideff (`Id origin) -> (fun () ->
reach view.next;
- inject_non_pstate (pure_cherry_pick_non_pstate origin);
+ inject_non_pstate (pure_cherry_pick_non_pstate view.next origin);
), cache, true
in
let cache_step =
if !Flags.async_proofs_cache = Some Flags.Force then `Yes
else cache_step in
- State.define
+ State.define ?safe_id
~cache:cache_step ~redefine:redefine_qed ~feedback_processed step id;
prerr_endline (fun () -> "reached: "^ Stateid.to_string id) in
reach ~redefine_qed id
@@ -2282,7 +2284,7 @@ let observe id =
Reach.known_state ~cache:(interactive ()) id;
VCS.print ()
with e ->
- let e = Errors.push e in
+ let e = CErrors.push e in
VCS.print ();
VCS.restore vcs;
iraise e
@@ -2332,7 +2334,7 @@ let check_task name (tasks,rcbackup) i =
let rc = Future.purify (Slaves.check_task name tasks) i in
VCS.restore vcs;
rc
- with e when Errors.noncritical e -> VCS.restore vcs; false
+ with e when CErrors.noncritical e -> VCS.restore vcs; false
let info_tasks (tasks,_) = Slaves.info_tasks tasks
let finish_tasks name u d p (t,rcbackup as tasks) =
RemoteCounter.restore rcbackup;
@@ -2345,7 +2347,7 @@ let finish_tasks name u d p (t,rcbackup as tasks) =
let u, a, _ = List.fold_left finish_task u (info_tasks tasks) in
(u,a,true), p
with e ->
- let e = Errors.push e in
+ let e = CErrors.push e in
msg_error (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e);
exit 1
@@ -2358,7 +2360,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;
- if keep <> VtDrop then VCS.propagate_sideff None;
+ VCS.propagate_sideff None;
`Ok
| { VCS.kind = `Edit (mode, qed_id, master_id, _,_) } ->
let ofp =
@@ -2377,7 +2379,7 @@ let merge_proof_branch ?valid ?id qast keep brname =
(* When tty is true, this code also does some of the job of the user interface:
jump back to a state that is valid *)
let handle_failure (e, info) vcs tty =
- if e = Errors.Drop then iraise (e, info) else
+ if e = CErrors.Drop then iraise (e, info) else
match Stateid.get info with
| None ->
VCS.restore vcs;
@@ -2389,7 +2391,7 @@ let handle_failure (e, info) vcs tty =
end;
VCS.print ();
anomaly(str"error with no safe_id attached:" ++ spc() ++
- Errors.iprint_no_report (e, info))
+ CErrors.iprint_no_report (e, info))
| Some (safe_id, id) ->
prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
VCS.restore vcs;
@@ -2405,7 +2407,7 @@ let handle_failure (e, info) vcs tty =
let snapshot_vio ldir long_f_dot_vo =
finish ();
if List.length (VCS.branches ()) > 1 then
- Errors.errorlabstrm "stm" (str"Cannot dump a vio with open proofs");
+ CErrors.errorlabstrm "stm" (str"Cannot dump a vio with open proofs");
Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_vo
(Global.opaque_tables ())
@@ -2469,14 +2471,14 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
finish ();
(try Future.purify (vernac_interp report_id ~route)
{x with verbose = true }
- with e when Errors.noncritical e ->
- let e = Errors.push e in
- iraise (State.exn_on report_id e)); `Ok
+ 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 = Errors.push e in
- iraise (State.exn_on report_id e)); `Ok
+ 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);
let id = VCS.new_node ~id:newtip () in
@@ -2611,7 +2613,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
VCS.print ();
rc
with e ->
- let e = Errors.push e in
+ let e = CErrors.push e in
handle_failure e vcs tty
let get_ast id =
@@ -2786,12 +2788,12 @@ let edit_at id =
VCS.print ();
rc
with e ->
- let (e, info) = Errors.push e in
+ let (e, info) = CErrors.push e in
match Stateid.get info with
| None ->
VCS.print ();
anomaly (str ("edit_at "^Stateid.to_string id^": ") ++
- Errors.print_no_report e)
+ CErrors.print_no_report e)
| Some (_, id) ->
prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
VCS.restore vcs;
@@ -2820,7 +2822,7 @@ let interp verb (loc,e) =
| _ -> not !Flags.coqtop_ui in
try finish ~print_goals ()
with e ->
- let e = Errors.push e in
+ let e = CErrors.push e in
handle_failure e vcs true
let finish () = finish ()
diff --git a/stm/tQueue.ml b/stm/tQueue.ml
index ee121c46a2..a0b08778ba 100644
--- a/stm/tQueue.ml
+++ b/stm/tQueue.ml
@@ -87,7 +87,7 @@ let broadcast { lock = m; cond = c } =
Mutex.unlock m
let push { queue = q; lock = m; cond = c; release } x =
- if release then Errors.anomaly(Pp.str
+ if release then CErrors.anomaly(Pp.str
"TQueue.push while being destroyed! Only 1 producer/destroyer allowed");
Mutex.lock m;
PriorityQueue.push q x;
diff --git a/stm/vcs.ml b/stm/vcs.ml
index c483ea4a9d..d3886464d9 100644
--- a/stm/vcs.ml
+++ b/stm/vcs.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
module type S = sig
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index f6d8c327e8..fa7acd00ab 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Vernacexpr
-open Errors
+open CErrors
open Pp
let default_proof_mode () = Proof_global.get_default_proof_mode_name ()
diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml
index d4dcf72c13..a6237daa04 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 Errors.error "The number of workers must be bigger than 0";
+ if j < 1 then CErrors.error "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 Errors.error "The number of workers must be bigger than 0";
+ if j < 1 then CErrors.error "The number of workers must be bigger than 0";
let jobs = ref [] in
List.iter (fun f ->
let f =
diff --git a/stm/workerPool.ml b/stm/workerPool.ml
index b94fae547d..9623765de0 100644
--- a/stm/workerPool.ml
+++ b/stm/workerPool.ml
@@ -52,7 +52,7 @@ let master_handshake worker_id ic oc =
Printf.eprintf "Handshake with %s failed: protocol mismatch\n" worker_id;
exit 1;
end
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
Printf.eprintf "Handshake with %s failed: %s\n"
worker_id (Printexc.to_string e);
exit 1
@@ -65,7 +65,7 @@ let worker_handshake slave_ic slave_oc =
exit 1;
end;
Marshal.to_channel slave_oc v []; flush slave_oc;
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
prerr_endline ("Handshake failed: " ^ Printexc.to_string e);
exit 1
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 11:14:00 +0000