diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/asyncTaskQueue.ml | 28 | ||||
| -rw-r--r-- | stm/lemmas.ml | 65 | ||||
| -rw-r--r-- | stm/lemmas.mli | 4 | ||||
| -rw-r--r-- | stm/proofBlockDelimiter.ml | 8 | ||||
| -rw-r--r-- | stm/spawned.ml | 4 | ||||
| -rw-r--r-- | stm/stm.ml | 250 | ||||
| -rw-r--r-- | stm/stm.mli | 4 | ||||
| -rw-r--r-- | stm/tQueue.ml | 2 | ||||
| -rw-r--r-- | stm/vcs.ml | 2 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 4 | ||||
| -rw-r--r-- | stm/vio_checking.ml | 4 | ||||
| -rw-r--r-- | stm/workerPool.ml | 4 |
12 files changed, 219 insertions, 160 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 39f5810825..022c89ad9a 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 @@ -301,13 +305,16 @@ let save_anonymous_with_strength ?export_seff proof kind save_ident = (* 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, _, _ -> - Feedback.msg_warning (str "Let definition" ++ spc () ++ pr_id id ++ spc () ++ - str "declared as an axiom.") + | Local, _, _ | Discharge, _, _ -> warn_let_as_axiom id in let () = assumption_message id in Option.iter (Universes.register_universe_binders (ConstRef kn)) pl; @@ -442,7 +449,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook = 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 kind thms hook = +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 @@ -452,7 +459,9 @@ let start_proof_com kind thms hook = 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 - evdref := solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref); + 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), @@ -462,6 +471,11 @@ let start_proof_com kind thms hook = 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 *) @@ -472,6 +486,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 = @@ -485,14 +511,18 @@ 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 + let universes = Proof.initial_euctx pftree in (* This will warn if the proof is complete *) - let pproofs, universes = + 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 @@ -501,7 +531,8 @@ let save_proof ?proof = function Some (Environ.keep_hyps env (Idset.union ids_typ ids_def)) | _ -> None in let names = Pfedit.get_universe_binders () in - let binders, ctx = Evd.universe_context ?names (Evd.from_ctx universes) 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 diff --git a/stm/lemmas.mli b/stm/lemmas.mli index f751598f04..39c089be9f 100644 --- a/stm/lemmas.mli +++ b/stm/lemmas.mli @@ -33,7 +33,9 @@ val start_proof_univs : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_ma ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> unit -val start_proof_com : goal_kind -> Vernacexpr.proof_expr list -> +val start_proof_com : + ?inference_hook:Pretyping.inference_hook -> + goal_kind -> Vernacexpr.proof_expr list -> unit declaration_hook -> unit val start_proof_with_initialization : diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index ce12185cba..8162fc3bb5 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -83,7 +83,7 @@ let static_bullet ({ entry_point; prev_node } as view) = if node.indentation > base then `Cont node else match node.ast with | Vernacexpr.VernacBullet b' when b = b' -> - `Found { stop = entry_point.id; start = prev.id; + `Found { block_stop = entry_point.id; block_start = prev.id; dynamic_switch = node.id; carry_on_data = of_bullet_val b } | _ -> `Stop) entry_point | _ -> assert false @@ -108,7 +108,7 @@ let static_curly_brace ({ entry_point; prev_node } as view) = crawl view (fun (nesting,prev) node -> match node.ast with | Vernacexpr.VernacSubproof _ when nesting = 0 -> - `Found { stop = entry_point.id; start = prev.id; + `Found { block_stop = entry_point.id; block_start = prev.id; dynamic_switch = node.id; carry_on_data = unit_val } | Vernacexpr.VernacSubproof _ -> `Cont (nesting - 1,node) @@ -135,7 +135,7 @@ let static_par { entry_point; prev_node } = match prev_node entry_point with | None -> None | Some { id = pid } -> - Some { stop = entry_point.id; start = pid; + Some { block_stop = entry_point.id; block_start = pid; dynamic_switch = pid; carry_on_data = unit_val } let dynamic_par { dynamic_switch = id } = @@ -162,7 +162,7 @@ let static_indent ({ entry_point; prev_node } as view) = crawl view ~init:(Some last_tac) (fun prev node -> if node.indentation >= last_tac.indentation then `Cont node else - `Found { stop = entry_point.id; start = node.id; + `Found { block_stop = entry_point.id; block_start = node.id; dynamic_switch = node.id; carry_on_data = of_vernac_expr_val entry_point.ast } ) last_tac 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 87c23c30ce..e387e6322f 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -11,8 +11,12 @@ let pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr 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 () +(* Opening ppvernac below aliases Richpp, see PR#185 *) +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 @@ -33,18 +37,20 @@ 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 -> - feedback ~id (ErrorMsg (loc, Pp.string_of_ppcmds 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) (ErrorMsg (loc, Pp.string_of_ppcmds msg))) () + feedback ~id:(State state_id) (Message(Error, Some loc, pp_to_richpp msg))) () let unreachable_state, unreachable_state_hook = Hook.make ~default:(fun _ _ -> ()) () @@ -115,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 @@ -145,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)) @@ -250,8 +256,8 @@ and pt = { (* TODO: inline records in OCaml 4.03 *) qed : Stateid.t; } and static_block_declaration = { - start : Stateid.t; - stop : Stateid.t; + block_start : Stateid.t; + block_stop : Stateid.t; dynamic_switch : Stateid.t; carry_on_data : DynBlockData.t; } @@ -356,10 +362,10 @@ module VCS : sig val get_state : id -> cached_state (* cuts from start -> stop, raising Expired if some nodes are not there *) - val slice : start:id -> stop:id -> vcs - val nodes_in_slice : start:id -> stop:id -> Stateid.t list + val slice : block_start:id -> block_stop:id -> vcs + val nodes_in_slice : block_start:id -> block_stop:id -> Stateid.t list - val create_proof_task_box : id list -> qed:id -> start:id -> unit + val create_proof_task_box : id list -> qed:id -> block_start:id -> unit val create_proof_block : static_block_declaration -> string -> unit val box_of : id -> box list val delete_boxes_of : id -> unit @@ -576,20 +582,20 @@ end = struct (* {{{ *) let visit id = Vcs_aux.visit !vcs id - let nodes_in_slice ~start ~stop = + let nodes_in_slice ~block_start ~block_stop = let rec aux id = - if Stateid.equal id start then [] else + if Stateid.equal id block_start then [] else 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 start ^ - " to "^Stateid.to_string stop)) - in aux stop + | _ -> anomaly(str("Cannot slice from "^ Stateid.to_string block_start ^ + " to "^Stateid.to_string block_stop)) + in aux block_stop - let slice ~start ~stop = - let l = nodes_in_slice ~start ~stop in + let slice ~block_start ~block_stop = + let l = nodes_in_slice ~block_start ~block_stop in let copy_info v id = Vcs_.set_info v id { (get_info id) with state = Empty; vcs_backup = None,None } in @@ -605,27 +611,27 @@ end = struct (* {{{ *) (Stateid.Set.elements (Vcs_.Dag.Property.having_it p)) (Vcs_.Dag.Property.data p)) v props in - let v = Vcs_.empty start in - let v = copy_info v start in + let v = Vcs_.empty block_start in + let v = copy_info v block_start in let v = List.fold_right (fun (id,tr) v -> let v = Vcs_.commit v id tr in let v = copy_info v id in v) l v in (* Stm should have reached the beginning of proof *) - assert (match (get_info start).state with Valid _ -> true | _ -> false); + assert (match (get_info block_start).state with Valid _ -> true | _ -> false); (* We put in the new dag the most recent state known to master *) let rec fill id = match (get_info id).state with | Empty | Error _ -> fill (Vcs_aux.visit v id).next | Valid _ -> copy_info_w_state v id in - let v = fill stop in + let v = fill block_stop in (* We put in the new dag the first state (since Qed shall run on it, * see check_task_aux) *) - let v = copy_info_w_state v start in + let v = copy_info_w_state v block_start in copy_proof_blockes v - let nodes_in_slice ~start ~stop = - List.rev (List.map fst (nodes_in_slice ~start ~stop)) + let nodes_in_slice ~block_start ~block_stop = + List.rev (List.map fst (nodes_in_slice ~block_start ~block_stop)) let topo_invariant l = let all = List.fold_right Stateid.Set.add l Stateid.Set.empty in @@ -636,11 +642,11 @@ end = struct (* {{{ *) List.for_all (fun s -> Stateid.Set.(subset s all || subset all s)) sets) l - let create_proof_task_box l ~qed ~start:lemma = + let create_proof_task_box l ~qed ~block_start:lemma = if not (topo_invariant l) then anomaly (str "overlapping boxes"); vcs := create_property !vcs l (ProofTask { qed; lemma }) - let create_proof_block ({ start; stop} as decl) name = - let l = nodes_in_slice ~start ~stop in + 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"); vcs := create_property !vcs l (ProofBlock (decl, name)) let box_of id = List.map Dag.Property.data (property_of !vcs id) @@ -740,7 +746,7 @@ module State : sig 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 -> iexn -> iexn (* to send states across worker/master *) type frozen_state val get_cached : Stateid.t -> frozen_state @@ -848,14 +854,14 @@ end = struct (* {{{ *) VCS.set_state id (Valid s) with VCS.Expired -> () - let exn_on id ?valid (e, info) = + let exn_on id ~valid (e, info) = match Stateid.get info with | Some _ -> (e, info) | None -> let loc = Option.default Loc.ghost (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))); - (e, Stateid.add info ?valid id) + (e, Stateid.add info ~valid id) let same_env { system = s1 } { system = s2 } = let s1 = States.summary_of_state s1 in @@ -888,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 = @@ -985,8 +991,6 @@ end = struct (* {{{ *) | VernacResetInitial -> VtStm (VtBack Stateid.initial, true), VtNow | VernacResetName (_,name) -> - msg_warning - (str"Reset not implemented for automatically generated constants"); let id = VCS.get_branch_pos (VCS.current_branch ()) in (try let oid = @@ -1036,8 +1040,8 @@ end = struct (* {{{ *) | _ -> VtUnknown, VtNow with | Not_found -> - msg_warning(str"undo_vernac_classifier: going back to the initial state."); - VtStm (VtBack Stateid.initial, true), VtNow + CErrors.errorlabstrm "undo_vernac_classifier" + (str "Cannot undo") end (* }}} *) @@ -1070,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) @@ -1104,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 @@ -1135,11 +1139,11 @@ let detect_proof_block id name = let static, _ = List.assoc name !proof_block_delimiters in begin match static { prev_node; entry_point } with | None -> () - | Some ({ start; stop } as decl) -> + | Some ({ block_start; block_stop } as decl) -> 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 *********************************) @@ -1247,7 +1251,7 @@ end = struct (* {{{ *) try Some (ReqBuildProof ({ Stateid.exn_info = t_exn_info; stop = t_stop; - document = VCS.slice ~start:t_start ~stop:t_stop; + document = VCS.slice ~block_start:t_start ~block_stop:t_stop; loc = t_loc; uuid = t_uuid; name = t_name }, t_drop, t_states)) @@ -1324,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 @@ -1364,7 +1368,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_warning (str "STM: sending back a fat state"); + msg_debug (str "STM: sending back a fat state"); Some (id, `Full s) | _, Some s -> Some (id, `Full s) in let rec aux seen = function @@ -1397,7 +1401,7 @@ and Slaves : sig (* (eventually) remote calls *) val build_proof : loc:Loc.t -> drop_pt:bool -> - exn_info:(Stateid.t * Stateid.t) -> start:Stateid.t -> stop:Stateid.t -> + exn_info:(Stateid.t * Stateid.t) -> block_start:Stateid.t -> block_stop:Stateid.t -> name:string -> future_proof * cancel_switch (* blocking function that waits for the task queue to be empty *) @@ -1435,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 = @@ -1464,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 ( @@ -1556,7 +1560,7 @@ end = struct (* {{{ *) BuildProof { t_states = s2 } -> overlap_rel s1 s2 | _ -> 0) - let build_proof ~loc ~drop_pt ~exn_info ~start ~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 @@ -1565,21 +1569,21 @@ end = struct (* {{{ *) Future.create_delegate ~blocking:true ~name:pname (State.exn_on id ~valid) in let t_uuid = Future.uuid f in let task = ProofTask.(BuildProof { - t_exn_info; t_start = start; t_stop = stop; t_drop = drop_pt; + t_exn_info; t_start = block_start; t_stop = block_stop; t_drop = drop_pt; t_assign = assign; t_loc = loc; t_uuid; t_name = pname; - t_states = VCS.nodes_in_slice ~start ~stop }) in + t_states = VCS.nodes_in_slice ~block_start ~block_stop }) in TaskQueue.enqueue_task (Option.get !queue) (task,cancel_switch); f, cancel_switch end else - ProofTask.build_proof_here ~drop_pt t_exn_info loc stop, cancel_switch + ProofTask.build_proof_here ~drop_pt t_exn_info loc 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 feedback (InProgress 1); let task = ProofTask.(BuildProof { - t_exn_info; t_start = start; t_stop = stop; t_assign; t_drop = drop_pt; + t_exn_info; t_start = block_start; t_stop = block_stop; t_assign; t_drop = drop_pt; t_loc = loc; t_uuid; t_name = pname; - t_states = VCS.nodes_in_slice ~start ~stop }) in + t_states = VCS.nodes_in_slice ~block_start ~block_stop }) in TaskQueue.enqueue_task (Option.get !queue) (task,cancel_switch); f, cancel_switch @@ -1661,7 +1665,7 @@ end = struct (* {{{ *) r_state_fb = t_state_fb; r_document = if age <> `Fresh then None - else Some (VCS.slice ~start:t_state ~stop:t_state); + else Some (VCS.slice ~block_start:t_state ~block_stop:t_state); r_ast = t_ast; r_goal = t_goal; r_name = t_name } @@ -1704,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 @@ -1717,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 @@ -1771,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 @@ -1819,7 +1823,7 @@ end = struct (* {{{ *) try Some { r_where = t_where; r_for = t_for; - r_doc = VCS.slice ~start:t_where ~stop:t_where; + r_doc = VCS.slice ~block_start:t_where ~block_stop:t_where; r_what = t_what } with VCS.Expired -> None @@ -1840,10 +1844,10 @@ 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 - let msg = string_of_ppcmds (iprint e) in - feedback ~id:(State r_for) (ErrorMsg (Loc.ghost, msg)) + 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 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) @@ -1894,6 +1898,12 @@ let delegate name = || !Flags.compilation_mode = Flags.BuildVio || !Flags.async_proofs_full +let warn_deprecated_nested_proofs = + CWarnings.create ~name:"deprecated-nested-proofs" ~category:"deprecated" + (fun () -> + strbrk ("Nested proofs are deprecated and will "^ + "stop working in a future Coq version")) + let collect_proof keep cur hd brkind id = prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id); let no_name = "" in @@ -1958,8 +1968,7 @@ let collect_proof keep cur hd brkind id = let name = name ids in `MaybeASync (parent last, None, accn, name, delegate name) | `Sideff _ -> - Pp.(msg_warning (strbrk ("Nested proofs are deprecated and will "^ - "stop working in the next Coq version"))); + warn_deprecated_nested_proofs (); `Sync (no_name,None,`NestedProof) | _ -> `Sync (no_name,None,`Unknown) in let make_sync why = function @@ -2017,7 +2026,7 @@ let known_state ?(redefine_qed=false) ~cache id = let boxes = VCS.box_of id in let valid_boxes = CList.map_filter (function - | ProofBlock ({ stop } as decl, name) when Stateid.equal stop id -> + | ProofBlock ({ block_stop } as decl, name) when Stateid.equal block_stop id -> Some (decl, name) | _ -> None) boxes in assert(List.length valid_boxes < 2); @@ -2049,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 @@ -2061,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 = @@ -2072,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 *) @@ -2082,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); @@ -2139,20 +2148,20 @@ 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 () ), `Yes, true | `Qed ({ qast = x; keep; brinfo; brname } as qed, eop) -> let rec aux = function - | `ASync (start, pua, nodes, name, delegate) -> (fun () -> + | `ASync (block_start, pua, nodes, name, delegate) -> (fun () -> assert(keep == VtKeep || keep == VtKeepAsAxiom); let drop_pt = keep == VtKeepAsAxiom in - let stop, exn_info, loc = eop, (id, eop), x.loc in + let block_stop, exn_info, loc = eop, (id, eop), x.loc in log_processing_async id name; - VCS.create_proof_task_box nodes ~qed:id ~start; + VCS.create_proof_task_box nodes ~qed:id ~block_start; begin match brinfo, qed.fproof with | { VCS.kind = `Edit _ }, None -> assert false | { VCS.kind = `Edit (_,_,_, okeep, _) }, Some (ofp, cancel) -> @@ -2166,19 +2175,22 @@ 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 ~start ~stop ~name in + ~loc ~drop_pt ~exn_info ~block_start ~block_stop ~name in Future.replace ofp fp; - qed.fproof <- Some (fp, cancel) + qed.fproof <- Some (fp, cancel); + (* We don't generate a new state, but we still need + * to install the right one *) + State.install_cached id | { VCS.kind = `Proof _ }, Some _ -> assert false | { VCS.kind = `Proof _ }, None -> - reach ~cache:`Shallow start; + reach ~cache:`Shallow block_start; let fp, cancel = if delegate then Slaves.build_proof - ~loc ~drop_pt ~exn_info ~start ~stop ~name + ~loc ~drop_pt ~exn_info ~block_start ~block_stop ~name else ProofTask.build_proof_here - ~drop_pt exn_info loc stop, ref false + ~drop_pt exn_info loc block_stop, ref false in qed.fproof <- Some (fp, cancel); let proof = @@ -2233,13 +2245,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 @@ -2275,7 +2287,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 @@ -2325,7 +2337,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; @@ -2338,11 +2350,11 @@ 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 -let merge_proof_branch ?valid ?id qast keep brname = +let merge_proof_branch ~valid ?id qast keep brname = let brinfo = VCS.get_branch brname in let qed fproof = { qast; keep; brname; brinfo; fproof } in match brinfo with @@ -2351,7 +2363,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 = @@ -2365,12 +2377,12 @@ 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)) + 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 = 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; @@ -2382,7 +2394,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; @@ -2398,7 +2410,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 ()) @@ -2406,10 +2418,7 @@ let reset_task_queue = Slaves.reset_task_queue (* Document building *) let process_transaction ?(newtip=Stateid.fresh ()) ~tty - ({ verbose; loc; expr } as x) c - = - let warn_if_pos a b = - if b then msg_warning(pr_ast a ++ str" should not be part of a script") in + ({ verbose; loc; expr } as x) c = prerr_endline (fun () -> "{{{ processing: "^ string_of_ppcmds (pr_ast x)); let vcs = VCS.backup () in try @@ -2423,12 +2432,12 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty | 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 -> warn_if_pos x b; join (); `Ok - | VtStm (VtFinish, b), VtNow -> warn_if_pos x b; finish (); `Ok - | VtStm (VtWait, b), VtNow -> warn_if_pos x b; finish (); wait (); `Ok + | VtStm (VtJoinDocument, b), VtNow -> join (); `Ok + | VtStm (VtFinish, b), VtNow -> finish (); `Ok + | VtStm (VtWait, b), VtNow -> finish (); wait (); `Ok | VtStm (VtPrintDag, b), VtNow -> - warn_if_pos x b; VCS.print ~now:true (); `Ok - | VtStm (VtObserve id, b), VtNow -> warn_if_pos x b; observe id; `Ok + 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") @@ -2437,9 +2446,10 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty | VtStm (VtBack oid, true), w -> let id = VCS.new_node ~id:newtip () in let { mine; others } = Backtrack.branches_of oid in + let valid = VCS.get_branch_pos head in List.iter (fun branch -> if not (List.mem_assoc branch (mine::others)) then - ignore(merge_proof_branch x VtDrop branch)) + ignore(merge_proof_branch ~valid x VtDrop branch)) (VCS.branches ()); VCS.checkout_shallowest_proof_branch (); let head = VCS.current_branch () in @@ -2465,14 +2475,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 @@ -2534,8 +2544,8 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty detect_proof_block id cblock; *) Backtrack.record (); if w == VtNow then finish (); `Ok | VtQed keep, w -> - let valid = if tty then Some(VCS.get_branch_pos head) else None in - let rc = merge_proof_branch ?valid ~id:newtip x keep head in + let valid = VCS.get_branch_pos head in + let rc = merge_proof_branch ~valid ~id:newtip x keep head in VCS.checkout_shallowest_proof_branch (); Backtrack.record (); if w == VtNow then finish (); rc @@ -2607,7 +2617,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 = @@ -2638,6 +2648,7 @@ let add ~ontop ?newtip ?(check=ignore) verb eid s = 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 + CWarnings.set_current_loc loc; check(loc,ast); let clas = classify_vernac ast in let aast = { verbose = verb; indentation; strlen; loc; expr = ast } in @@ -2659,6 +2670,7 @@ let query ~at ?(report_with=(Stateid.dummy,default_route)) s = 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 + CWarnings.set_current_loc loc; let clas = classify_vernac ast in let aast = { verbose = true; indentation; strlen; loc; expr = ast } in match clas with @@ -2780,12 +2792,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; @@ -2814,7 +2826,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/stm.mli b/stm/stm.mli index 37ec1f0a13..b8a2a38596 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -139,8 +139,8 @@ module QueryTask : AsyncTaskQueue.Task module DynBlockData : Dyn.S type static_block_declaration = { - start : Stateid.t; - stop : Stateid.t; + block_start : Stateid.t; + block_stop : Stateid.t; dynamic_switch : Stateid.t; carry_on_data : DynBlockData.t; } 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..dc5be08a37 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 () @@ -181,7 +181,7 @@ let rec classify_vernac e = | VernacReserve _ | VernacGeneralizable _ | VernacSetOpacity _ | VernacSetStrategy _ - | VernacUnsetOption _ | VernacSetOption _ + | VernacUnsetOption _ | VernacSetOption _ | VernacSetAppendOption _ | VernacAddOption _ | VernacRemoveOption _ | VernacMemOption _ | VernacPrintOption _ | VernacGlobalCheck _ 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 |