From 99c92fedebf629549eb16feb266f55c83ad99bd9 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 16 Feb 2017 13:43:38 +0100 Subject: [stm] remove tactic_being_run hook `tactic_being_run_hook` was used for the "xml" pluging but I am not sure we have a sensible use case here. --- stm/stm.ml | 12 ++---------- stm/stm.mli | 3 --- 2 files changed, 2 insertions(+), 13 deletions(-) diff --git a/stm/stm.ml b/stm/stm.ml index b0ad3f8790..d505168446 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -52,9 +52,6 @@ let parse_error, parse_error_hook = Hook.make 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) *) @@ -2213,10 +2210,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 () -> @@ -2226,9 +2221,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); - stm_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 () -> @@ -2946,5 +2939,4 @@ let forward_feedback_hook = Hooks.forward_feedback_hook let process_error_hook = Hooks.process_error_hook let unreachable_state_hook = Hooks.unreachable_state_hook let () = Hook.set Obligations.stm_get_fix_exn (fun () -> !State.fix_exn_ref) -let tactic_being_run_hook = Hooks.tactic_being_run_hook (* vim:set foldmethod=marker: *) diff --git a/stm/stm.mli b/stm/stm.mli index 0f0a3c4e13..9ae78e02cf 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -187,9 +187,6 @@ val parse_error_hook : 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 -- cgit v1.2.3 From b209cea412a9541fd1c434dde36ea6eb1e256a33 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 16 Feb 2017 13:41:07 +0100 Subject: [stm] remove process_error_hook `process_error_hook` seems unnecesary, we just call the proper error interpretation. --- stm/stm.ml | 5 +---- stm/stm.mli | 3 --- toplevel/vernac.ml | 3 --- 3 files changed, 1 insertion(+), 10 deletions(-) diff --git a/stm/stm.ml b/stm/stm.ml index d505168446..ba5e8a11fb 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -29,8 +29,6 @@ let execution_error state_id loc msg = module Hooks = struct -let process_error, process_error_hook = Hook.make () - let state_computed, state_computed_hook = Hook.make ~default:(fun state_id ~in_cache -> feedback ~id:(State state_id) Processed) () @@ -63,7 +61,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 @@ -2936,7 +2934,6 @@ 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 forward_feedback_hook = Hooks.forward_feedback_hook -let process_error_hook = Hooks.process_error_hook let unreachable_state_hook = Hooks.unreachable_state_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 9ae78e02cf..a89062c298 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -209,6 +209,3 @@ 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 - -(* Hooks to be set by other Coq components in order to break file cycles *) -val process_error_hook : Future.fix_exn Hook.t diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 9917a49b42..d5ceeaccd7 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -347,6 +347,3 @@ let compile v f = ignore(CoqworkmgrApi.get 1); compile v f; CoqworkmgrApi.giveback 1 - -let () = Hook.set Stm.process_error_hook - ExplainErr.process_vernac_interp_error -- cgit v1.2.3 From 3a7d9fcafedc4987d0748a8717b2b012a779de39 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 16 Feb 2017 14:14:34 +0100 Subject: [stm] Remove edit_id. We remove `edit_id` from the STM. In PIDE they serve a different purpose, however in Coq they were of limited utility and required many special cases all around the code. Indeed, parsing is not an asynchronous operation in Coq, thus having feedback about parsing didn't make much sense. All clients indeed ignore such feedback and handle parsing in a synchronous way. XML protocol clients are unaffected, they rely on the instead on the Fail value. This commit supersedes PR#203. --- ide/coqOps.ml | 12 +++------- ide/ide_slave.ml | 4 ++-- ide/interface.mli | 6 +++-- ide/xmlprotocol.ml | 10 ++------- kernel/term_typing.ml | 2 +- lib/feedback.ml | 10 ++++----- lib/feedback.mli | 23 ++++++++----------- plugins/ltac/profile_ltac.ml | 2 +- stm/asyncTaskQueue.ml | 2 +- stm/stm.ml | 53 ++++++++++++++++++++++---------------------- stm/stm.mli | 9 ++++---- 11 files changed, 58 insertions(+), 75 deletions(-) diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 45b5a1007a..15150dce99 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -415,11 +415,7 @@ object(self) buffer#apply_tag Tags.Script.tooltip ~start ~stop; add_tooltip sentence pre post markup - method private is_dummy_id id = - match id with - | Edit 0 -> true - | State id when Stateid.equal id Stateid.dummy -> true - | _ -> false + method private is_dummy_id id = Stateid.equal id Stateid.dummy method private enqueue_feedback msg = (* Minilib.log ("Feedback received: " ^ Xml_printer.to_string_fmt (Xmlprotocol.of_feedback msg)); *) @@ -434,8 +430,7 @@ object(self) let sentence = let finder _ state_id s = match state_id, id with - | Some id', State id when Stateid.equal id id' -> Some (state_id, s) - | _, Edit id when id = s.edit_id -> Some (state_id, s) + | Some id', id when Stateid.equal id id' -> Some (state_id, s) | _ -> None in try Some (Doc.find_map document finder) with Not_found -> None in @@ -505,8 +500,7 @@ object(self) else try match id, Doc.tip document with - | Edit _, _ -> () - | State id1, id2 when Stateid.newer_than id2 id1 -> () + | id1, id2 when Stateid.newer_than id2 id1 -> () | _ -> Queue.add msg feedbacks with Doc.Empty | Invalid_argument _ -> Queue.add msg feedbacks end; diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 8cadf1a263..2d2b54678f 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -95,7 +95,7 @@ let ide_cmd_checks (loc,ast) = (** Interpretation (cf. [Ide_intf.interp]) *) let add ((s,eid),(sid,verbose)) = - let newid, rc = Stm.add ~ontop:sid verbose ~check:ide_cmd_checks eid s in + let newid, rc = Stm.add ~ontop:sid verbose ~check:ide_cmd_checks s in let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in (* TODO: the "" parameter is a leftover of the times the protocol * used to include stderr/stdout output. @@ -379,7 +379,7 @@ let init = let initial_id, _ = if not (is_in_load_paths (physical_path_of_string dir)) then Stm.add false ~ontop:(Stm.get_current_state ()) - 0 (Printf.sprintf "Add LoadPath \"%s\". " dir) + (Printf.sprintf "Add LoadPath \"%s\". " dir) else Stm.get_current_state (), `NewTip in if Filename.check_suffix file ".v" then Stm.set_compilation_hints file; diff --git a/ide/interface.mli b/ide/interface.mli index 9ed6062588..62f63aefb9 100644 --- a/ide/interface.mli +++ b/ide/interface.mli @@ -111,8 +111,10 @@ type coq_info = { (** Calls result *) type location = (int * int) option (* start and end of the error *) -type state_id = Feedback.state_id -type edit_id = Feedback.edit_id +type state_id = Stateid.t + +(* Obsolete *) +type edit_id = int (* The fail case carries the current state_id of the prover, the GUI should probably retract to that point *) diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index d7950e5fd5..bf52b0b52b 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -907,9 +907,7 @@ let of_feedback_content = function of_string filename ] | Message (l,loc,m) -> constructor "feedback_content" "message" [ of_message l loc m ] -let of_edit_or_state_id = function - | Edit id -> ["object","edit"], of_edit_id id - | State id -> ["object","state"], of_stateid id +let of_edit_or_state_id id = ["object","state"], of_stateid id let of_feedback msg = let content = of_feedback_content msg.contents in @@ -921,12 +919,8 @@ let of_feedback msg_fmt = msg_format := msg_fmt; of_feedback let to_feedback xml = match xml with - | Element ("feedback", ["object","edit";"route",route], [id;content]) -> { - id = Edit(to_edit_id id); - route = int_of_string route; - contents = to_feedback_content content } | Element ("feedback", ["object","state";"route",route], [id;content]) -> { - id = State(to_stateid id); + id = to_stateid id; route = int_of_string route; contents = to_feedback_content content } | x -> raise (Marshal_error("feedback",x)) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 6dfa64357c..88a4fa529a 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -194,7 +194,7 @@ let rec unzip ctx j = let feedback_completion_typecheck = let open Feedback in Option.iter (fun state_id -> - feedback ~id:(State state_id) Feedback.Complete) + feedback ~id:state_id Feedback.Complete) let infer_declaration ~trust env kn dcl = match dcl with diff --git a/lib/feedback.ml b/lib/feedback.ml index 7d9d6bf7f0..df6fe3a629 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -15,9 +15,6 @@ type level = | Warning | Error -type edit_id = int -type state_id = Stateid.t -type edit_or_state_id = Edit of edit_id | State of state_id type route_id = int type feedback_content = @@ -38,9 +35,9 @@ type feedback_content = | Message of level * Loc.t option * Pp.std_ppcmds type feedback = { - id : edit_or_state_id; + id : Stateid.t; + route : route_id; contents : feedback_content; - route : route_id; } let default_route = 0 @@ -56,7 +53,8 @@ let add_feeder = let del_feeder fid = Hashtbl.remove feeders fid -let feedback_id = ref (Edit 0) +let default_route = 0 +let feedback_id = ref Stateid.dummy let feedback_route = ref default_route let set_id_for_feedback ?(route=default_route) i = diff --git a/lib/feedback.mli b/lib/feedback.mli index 4bbdfcb5b6..bdd236ac78 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -16,11 +16,8 @@ type level = | Warning | Error -(** Coq "semantic" infos obtained during parsing/execution *) -type edit_id = int -type state_id = Stateid.t -type edit_or_state_id = Edit of edit_id | State of state_id +(** Coq "semantic" infos obtained during execution *) type route_id = int val default_route : route_id @@ -46,17 +43,16 @@ type feedback_content = | Message of level * Loc.t option * Pp.std_ppcmds type feedback = { - id : edit_or_state_id; (* The document part concerned *) - contents : feedback_content; (* The payload *) + id : Stateid.t; (* The document part concerned *) route : route_id; (* Extra routing info *) + contents : feedback_content; (* The payload *) } (** {6 Feedback sent, even asynchronously, to the user interface} *) -(* Morally the parser gets a string and an edit_id, and gives back an AST. - * Feedbacks during the parsing phase are attached to this edit_id. - * The interpreter assignes an exec_id to the ast, and feedbacks happening - * during interpretation are attached to the exec_id. - * Only one among state_id and edit_id can be provided. *) + +(* The interpreter assignes an state_id to the ast, and feedbacks happening + * during interpretation are attached to it. + *) (** [add_feeder f] adds a feeder listiner [f], returning its id *) val add_feeder : (feedback -> unit) -> int @@ -67,11 +63,10 @@ val del_feeder : int -> unit (** [feedback ?id ?route fb] produces feedback fb, with [route] and [id] set appropiatedly, if absent, it will use the defaults set by [set_id_for_feedback] *) -val feedback : - ?id:edit_or_state_id -> ?route:route_id -> feedback_content -> unit +val feedback : ?id:Stateid.t -> ?route:route_id -> feedback_content -> unit (** [set_id_for_feedback route id] Set the defaults for feedback *) -val set_id_for_feedback : ?route:route_id -> edit_or_state_id -> unit +val set_id_for_feedback : ?route:route_id -> Stateid.t -> unit (** {6 output functions} diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 58123f63ef..bcb28f77ce 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -374,7 +374,7 @@ let data = ref SM.empty let _ = Feedback.(add_feeder (function - | { id = State s; contents = Custom (_, "ltacprof_results", xml) } -> + | { id = s; contents = Custom (_, "ltacprof_results", xml) } -> let results = to_ltacprof_results xml in let other_results = (* Multi success can cause this *) try SM.find s !data diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 1254919880..3459156a43 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -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) diff --git a/stm/stm.ml b/stm/stm.ml index ba5e8a11fb..f8d959f97a 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -24,14 +24,14 @@ open Vernac_classifier open Feedback let execution_error state_id loc msg = - feedback ~id:(State state_id) + feedback ~id:state_id (Message (Error, Some loc, msg)) 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 -> ()) () @@ -43,10 +43,6 @@ 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, msg))) () - let unreachable_state, unreachable_state_hook = Hook.make ~default:(fun _ _ -> ()) () @@ -109,24 +105,30 @@ let indentation_of_string s = | _ -> 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 +(* 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. +*) +let stm_parse ?(indlen_prev=fun() -> 0) s = 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") + | None -> raise (Invalid_argument "stm_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))); + (* This is the old error recovery strategy. *) + (* let loc = Loc.get_loc info in *) + (* feedback (?newtip || eid) (Message(Error, loc, msg)) *) iraise (e, info)) () @@ -845,7 +847,7 @@ 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"); @@ -977,7 +979,7 @@ 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 (State id); + 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 @@ -1391,7 +1393,7 @@ end = struct (* {{{ *) 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 = @@ -1935,11 +1937,11 @@ end = struct (* {{{ *) Reach.known_state ~cache:`No r_where; try stm_vernac_interp r_for { r_what with verbose = true }; - feedback ~id:(State r_for) Processed + feedback ~id:r_for Processed with e when CErrors.noncritical e -> let e = CErrors.push e in let msg = iprint e in - feedback ~id:(State r_for) (Message (Error, None, msg)) + 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) @@ -2141,7 +2143,7 @@ let known_state ?(redefine_qed=false) ~cache id = | 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 -> stm_vernac_interp id { verbose = true; loc = Loc.ghost; expr; indentation = 0; @@ -2289,7 +2291,7 @@ let known_state ?(redefine_qed=false) ~cache id = if not delegate then ignore(Future.compute fp); reach view.next; stm_vernac_interp id ~proof x; - feedback ~id:(State id) Incomplete + feedback ~id:id Incomplete | { VCS.kind = `Master }, _ -> assert false end; Proof_global.discard_all () @@ -2715,13 +2717,13 @@ let ind_len_of id = indentation + strlen | _ -> 0 -let add ~ontop ?newtip ?(check=ignore) verb eid s = +let add ~ontop ?newtip ?(check=ignore) verb s = 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 + stm_parse ~indlen_prev:(fun () -> ind_len_of ontop) s in CWarnings.set_current_loc loc; check(loc,ast); let clas = classify_vernac ast in @@ -2742,8 +2744,7 @@ let query ~at ?(report_with=(Stateid.dummy,default_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 indentation, strlen, loc, ast = stm_parse s in CWarnings.set_current_loc loc; let clas = classify_vernac ast in let aast = { verbose = true; indentation; strlen; loc; expr = ast } in @@ -2932,8 +2933,8 @@ let get_all_proof_names () = (* 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 forward_feedback_hook = Hooks.forward_feedback_hook let unreachable_state_hook = Hooks.unreachable_state_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 a89062c298..d3e5dde39c 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -13,8 +13,8 @@ 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. +(* [add ontop check vebose eid s] adds a new command [s] on the state [ontop]. + [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]. @@ -23,7 +23,7 @@ open Loc val add : ontop:Stateid.t -> ?newtip:Stateid.t -> ?check:(vernac_expr located -> unit) -> - bool -> edit_id -> string -> + bool -> string -> Stateid.t * [ `NewTip | `Unfocus of Stateid.t ] (* parses and executes a command at a given state, throws away its side effects @@ -182,9 +182,8 @@ 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 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 -- cgit v1.2.3 From 4ed9c7ad75a7f09d723bdfce6f7dd086c60e0601 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 16 Feb 2017 22:31:13 +0100 Subject: [stm] Move main parsing entry point to the STM. Mainly due to notations, proof modes and plugins, parsing in Coq is stateful, so we expose a state-aware parsing API in the STM. This is a first move to unify all the parsing entry points in the Stm and the toplevel, and allows STM clients to control their input stream properly. This greatly helps for instance, with whole-document parsing. This commit supersedes PR#204. --- dev/doc/changes.txt | 17 +++++++ ide/ide_slave.ml | 27 +++++++---- stm/stm.ml | 130 +++++++++++++++++++++++++++++----------------------- stm/stm.mli | 41 ++++++++++------- 4 files changed, 131 insertions(+), 84 deletions(-) diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index af077bbb40..30edea7f2f 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -139,6 +139,23 @@ document type". This allows for a more uniform handling of printing module Tag +** Stm API ** + +- We have streamlined the `Stm` API, now `add` and `query` take a + `coq_parsable` instead a `string` so clients can have more control + over their input stream. As a consequence, their types have been + modified. + +- The main parsing entry point has also been moved to the + `Stm`. Parsing is considered a synchronous operation so it will + either succeed of emit an exception. + +- `Feedback` is now only emitted for asynchronous operations. As a + consequence, it always carries a valid stateid and the type has + changed to accommodate that. + +- A few unused hooks were removed due to cleanups, no clients known. + ========================================= = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 = ========================================= diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 2d2b54678f..8897577640 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -86,16 +86,19 @@ let ide_cmd_checks (loc,ast) = if is_debug ast then user_error "Debug mode not available in the IDE"; if is_known_option ast then - Feedback.msg_warning (strbrk "Set this option from the IDE menu instead"); + Feedback.msg_warning ~loc (strbrk "Set this option from the IDE menu instead"); if Vernac.is_navigation_vernac ast || is_undo ast then - Feedback.msg_warning (strbrk "Use IDE navigation instead"); + Feedback.msg_warning ~loc (strbrk "Use IDE navigation instead"); if is_query ast then - Feedback.msg_warning (strbrk "Query commands should not be inserted in scripts") + Feedback.msg_warning ~loc (strbrk "Query commands should not be inserted in scripts") (** Interpretation (cf. [Ide_intf.interp]) *) let add ((s,eid),(sid,verbose)) = - let newid, rc = Stm.add ~ontop:sid verbose ~check:ide_cmd_checks s in + let pa = Pcoq.Gram.parsable (Stream.of_string s) in + let loc_ast = Stm.parse_sentence sid pa in + ide_cmd_checks loc_ast; + let newid, rc = Stm.add ~ontop:sid verbose loc_ast in let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in (* TODO: the "" parameter is a leftover of the times the protocol * used to include stderr/stdout output. @@ -122,7 +125,9 @@ let edit_at id = * as not to break the core protocol for this minor change, but it should * be removed in the next version of the protocol. *) -let query (s,id) = Stm.query ~at:id s; "" +let query (s,id) = + let pa = Pcoq.Gram.parsable (Stream.of_string s) in + Stm.query ~at:id pa; "" let annotate phrase = let (loc, ast) = @@ -370,17 +375,19 @@ let init = fun file -> if !initialized then anomaly (str "Already initialized") else begin + let init_sid = Stm.get_current_state () in initialized := true; match file with - | None -> Stm.get_current_state () + | None -> init_sid | Some file -> let dir = Filename.dirname file in let open Loadpath in let open CUnix in let initial_id, _ = - if not (is_in_load_paths (physical_path_of_string dir)) then - Stm.add false ~ontop:(Stm.get_current_state ()) - (Printf.sprintf "Add LoadPath \"%s\". " dir) - else Stm.get_current_state (), `NewTip in + if not (is_in_load_paths (physical_path_of_string dir)) then begin + let pa = Pcoq.Gram.parsable (Stream.of_string (Printf.sprintf "Add LoadPath \"%s\". " dir)) in + let loc_ast = Stm.parse_sentence init_sid pa in + Stm.add false ~ontop:init_sid loc_ast + end else init_sid, `NewTip in if Filename.check_suffix file ".v" then Stm.set_compilation_hints file; Stm.finish (); diff --git a/stm/stm.ml b/stm/stm.ml index f8d959f97a..fb0a0514df 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -93,49 +93,6 @@ let may_pierce_opaque = function | { expr = VernacExtend (("ExtractionInductive",_), _) } -> true | _ -> false -(* 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 - -(* 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. -*) -let stm_parse ?(indlen_prev=fun() -> 0) s = - let indentation, precise, strlen = indentation_of_string s in - let indentation = - if precise then indentation else indlen_prev () + indentation in - 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 "stm_parse") - | Some (loc, ast) -> indentation, strlen, loc, ast - with e when CErrors.noncritical e -> - let (e, info) = CErrors.push e in - (* This is the old error recovery strategy. *) - (* let loc = Loc.get_loc info in *) - (* feedback (?newtip || eid) (Message(Error, loc, msg)) *) - 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 () @@ -2385,6 +2342,10 @@ let observe id = VCS.restore vcs; iraise e +let pr_open_cur_subgoals () = + try Printer.pr_open_subgoals () + with Proof_global.NoCurrentProof -> Pp.str "" + let finish ?(print_goals=false) () = let head = VCS.current_branch () in observe (VCS.get_branch_pos head); @@ -2706,26 +2667,80 @@ let get_ast id = 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 + 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."); + 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 com -> com + with e when CErrors.noncritical e -> + let (e, info) = CErrors.push e in + 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 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 sid 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 + + +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 = - stm_parse ~indlen_prev:(fun () -> ind_len_of ontop) s in + user_err ~hdr:"Stm.add" + (str "You used Stm.add on a different state than the tip" ++ fnl () ++ + str "This is not supported yet, sorry."); + let indentation, strlen = compute_indentation ontop loc 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 @@ -2744,7 +2759,8 @@ let query ~at ?(report_with=(Stateid.dummy,default_route)) s = Future.purify (fun s -> if Stateid.equal at Stateid.dummy then finish () else Reach.known_state ~cache:`Yes at; - let indentation, strlen, loc, ast = stm_parse s in + let loc, ast = parse_sentence at s in + let indentation, strlen = compute_indentation at loc in CWarnings.set_current_loc loc; let clas = classify_vernac ast in let aast = { verbose = true; indentation; strlen; loc; expr = ast } in diff --git a/stm/stm.mli b/stm/stm.mli index d3e5dde39c..a31e4289d9 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -13,24 +13,31 @@ open Loc (** state-transaction-machine interface *) -(* [add ontop check vebose eid s] adds a new command [s] on the state [ontop]. - [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 -> 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 -> (Loc.t * Vernacexpr.vernac_expr) -> + 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 -> ?report_with:(Stateid.t * 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 -- cgit v1.2.3 From ce2b2058587224ade9261cd4127ef4f6e94d356b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 27 Feb 2017 20:16:40 +0100 Subject: [stm] Port the toplevel to the STM. - We clean-up `Vernac` and make it use the STM API. - Now functions in `Vernac` for use in the toplevel and compiler take an starting `Stateid.t`. - Duplicated `Stm.interp` entry point is removed. - The XML protocol call `interp` is disabled. --- dev/doc/changes.txt | 13 ++++ ide/ide_slave.ml | 45 ++----------- lib/flags.ml | 2 - lib/flags.mli | 3 +- stm/stm.ml | 77 ++++++---------------- stm/stm.mli | 9 +-- toplevel/coqinit.ml | 11 ++-- toplevel/coqinit.mli | 2 +- toplevel/coqloop.ml | 31 +++++---- toplevel/coqloop.mli | 2 +- toplevel/coqtop.ml | 17 ++--- toplevel/vernac.ml | 179 +++++++++++++++++++------------------------------- toplevel/vernac.mli | 26 ++------ vernac/vernac.mllib | 1 + vernac/vernacprop.ml | 53 +++++++++++++++ vernac/vernacprop.mli | 19 ++++++ 16 files changed, 221 insertions(+), 269 deletions(-) create mode 100644 vernac/vernacprop.ml create mode 100644 vernac/vernacprop.mli diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 30edea7f2f..7e7bb98580 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -156,6 +156,19 @@ document type". This allows for a more uniform handling of printing - A few unused hooks were removed due to cleanups, no clients known. +** Toplevel and Vernacular API ** + +- The components related to vernacular interpretation have been moved + to their own folder `vernac/` whereas toplevel now contains the + proper toplevel shell and compiler. + +- Coq's toplevel has been ported to directly use the common `Stm` + API. The signature of a few functions has changed as a result. + +** XML Protocol ** + +- The legacy `interp` call has been turned into a noop. + ========================================= = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 = ========================================= diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 8897577640..bc7ce38836 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -8,6 +8,7 @@ (************************************************************************) open Vernacexpr +open Vernacprop open CErrors open Util open Pp @@ -60,25 +61,6 @@ let is_known_option cmd = match cmd with | VernacUnsetOption o -> coqide_known_option o | _ -> false -let is_debug cmd = match cmd with - | VernacSetOption (["Ltac";"Debug"], _) -> true - | _ -> false - -let is_query cmd = match cmd with - | VernacChdir None - | VernacMemOption _ - | VernacPrintOption _ - | VernacCheckMayEval _ - | VernacGlobalCheck _ - | VernacPrint _ - | VernacSearch _ - | VernacLocate _ -> true - | _ -> false - -let is_undo cmd = match cmd with - | VernacUndo _ | VernacUndoTo _ -> true - | _ -> false - (** Check whether a command is forbidden in the IDE *) let ide_cmd_checks (loc,ast) = @@ -87,7 +69,7 @@ let ide_cmd_checks (loc,ast) = user_error "Debug mode not available in the IDE"; if is_known_option ast then Feedback.msg_warning ~loc (strbrk "Set this option from the IDE menu instead"); - if Vernac.is_navigation_vernac ast || is_undo ast then + if is_navigation_vernac ast || is_undo ast then Feedback.msg_warning ~loc (strbrk "Use IDE navigation instead"); if is_query ast then Feedback.msg_warning ~loc (strbrk "Query commands should not be inserted in scripts") @@ -132,7 +114,7 @@ let query (s,id) = let annotate phrase = let (loc, ast) = let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in - Vernac.parse_sentence (pa,None) + Stm.parse_sentence (Stm.get_current_state ()) pa in (* XXX: Width should be a parameter of annotate... *) Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast) @@ -394,26 +376,9 @@ let init = initial_id end -(* Retrocompatibility stuff *) +(* Retrocompatibility stuff, disabled since 8.7 *) let interp ((_raw, verbose), s) = - let vernac_parse s = - let pa = Pcoq.Gram.parsable (Stream.of_string s) in - Flags.with_option Flags.we_are_parsing (fun () -> - match Pcoq.Gram.entry_parse Pcoq.main_entry pa with - | None -> raise (Invalid_argument "vernac_parse") - | Some ast -> ast) - () in - Stm.interp verbose (vernac_parse s); - (* TODO: the "" parameter is a leftover of the times the protocol - * used to include stderr/stdout output. - * - * Currently, we force all the output meant for the to go via the - * feedback mechanism, and we don't manipulate stderr/stdout, which - * are left to the client's discrection. The parameter is still there - * as not to break the core protocol for this minor change, but it should - * be removed in the next version of the protocol. - *) - Stm.get_current_state (), CSig.Inl "" + Stateid.dummy, CSig.Inr "The interp call has been disabled, please use Add." (** When receiving the Quit call, we don't directly do an [exit 0], but rather set this reference, in order to send a final answer diff --git a/lib/flags.ml b/lib/flags.ml index 5b080151cd..ef5eddfb29 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -86,8 +86,6 @@ let in_toplevel = ref false let profile = false let print_emacs = ref false -let coqtop_ui = ref false - let xml_export = ref false let ide_slave = ref false diff --git a/lib/flags.mli b/lib/flags.mli index bd365e6538..f5e1c96f9a 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -46,9 +46,8 @@ val in_toplevel : bool ref val profile : bool +(* Legacy flags *) val print_emacs : bool ref -val coqtop_ui : bool ref - val xml_export : bool ref val ide_slave : bool ref diff --git a/stm/stm.ml b/stm/stm.ml index fb0a0514df..8d212a6a08 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -323,6 +323,15 @@ 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 @@ -970,7 +979,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 @@ -2342,22 +2350,18 @@ let observe id = VCS.restore vcs; iraise e -let pr_open_cur_subgoals () = - try Printer.pr_open_subgoals () - with Proof_global.NoCurrentProof -> Pp.str "" - -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 | _ -> () - let wait () = Slaves.wait_all_done (); VCS.print () @@ -2435,29 +2439,17 @@ 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 = +let handle_failure (e, info) vcs = if e = CErrors.Drop then 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)) | Some (safe_id, 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) @@ -2471,7 +2463,7 @@ let snapshot_vio ldir long_f_dot_vo = 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 = stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x); let vcs = VCS.backup () in @@ -2517,13 +2509,6 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty anomaly(str"classifier: VtBack + VtLater must imply part_of_script") (* Query *) - | VtQuery (false,(report_id,route)), VtNow when tty = true -> - finish (); - (try Future.purify (stm_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 stm_vernac_interp report_id ~route x with e -> @@ -2655,7 +2640,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty 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 @@ -2743,7 +2728,7 @@ let add ~ontop ?newtip verb (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 ()) @@ -2766,10 +2751,9 @@ let query ~at ?(report_with=(Stateid.dummy,default_route)) s = 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,report_with), VtNow))) s let edit_at id = @@ -2898,32 +2882,11 @@ let edit_at id = 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 diff --git a/stm/stm.mli b/stm/stm.mli index a31e4289d9..30e9629c6f 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -30,7 +30,7 @@ exception End_of_input If [newtip] is provided, then the returned state id is guaranteed to be [newtip] *) val add : ontop:Stateid.t -> ?newtip:Stateid.t -> - bool -> (Loc.t * Vernacexpr.vernac_expr) -> + 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], @@ -205,13 +205,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 diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index ffd0d78051..2b9a04dad8 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -27,12 +27,12 @@ let set_rcfile s = rcfile := s; rcfile_specified := true let load_rc = ref true let no_load_rc () = load_rc := false -let load_rcfile() = +let load_rcfile sid = if !load_rc then try if !rcfile_specified then if CUnix.file_readable_p !rcfile then - Vernac.load_vernac false !rcfile + Vernac.load_vernac false sid !rcfile else raise (Sys_error ("Cannot read rcfile: "^ !rcfile)) else try @@ -43,8 +43,8 @@ let load_rcfile() = Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version; Envars.home ~warn / "."^rcdefaultname ] in - Vernac.load_vernac false inferedrc - with Not_found -> () + Vernac.load_vernac false sid inferedrc + with Not_found -> sid (* Flags.if_verbose mSGNL (str ("No coqrc or coqrc."^Coq_config.version^ @@ -55,7 +55,8 @@ let load_rcfile() = let () = Feedback.msg_info (str"Load of rcfile failed.") in iraise reraise else - Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading.") + (Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading."); + sid) (* Recursively puts dir in the LoadPath if -nois was not passed *) let add_stdlib_path ~unix_path ~coq_root ~with_ml = diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index 4ff87628c8..3b42289eec 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -13,7 +13,7 @@ val set_debug : unit -> unit val set_rcfile : string -> unit val no_load_rc : unit -> unit -val load_rcfile : unit -> unit +val load_rcfile : Stateid.t -> Stateid.t val push_include : string -> Names.DirPath.t -> bool -> unit (** [push_include phys_path log_path implicit] *) diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 2282932d47..17d8f5f49b 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -257,7 +257,7 @@ let set_prompt prompt = let parse_to_dot = let rec dot st = match Stream.next st with | Tok.KEYWORD ("."|"...") -> () - | Tok.EOI -> raise End_of_input + | Tok.EOI -> raise Stm.End_of_input | _ -> dot st in Gram.Entry.of_parser "Coqtoplevel.dot" dot @@ -271,13 +271,11 @@ let rec discard_to_dot () = Gram.entry_parse parse_to_dot top_buffer.tokens with | Token.Error _ | CLexer.Error.E _ -> discard_to_dot () - | End_of_input -> raise End_of_input + | Stm.End_of_input -> raise Stm.End_of_input | e when CErrors.noncritical e -> () -let read_sentence input = - try - let (loc, _ as r) = Vernac.parse_sentence input in - CWarnings.set_current_loc loc; r +let read_sentence sid input = + try Stm.parse_sentence sid input with reraise -> let reraise = CErrors.push reraise in discard_to_dot (); @@ -312,25 +310,24 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in is caught and handled (i.e. not re-raised). *) -let do_vernac () = +let do_vernac sid = top_stderr (fnl()); if !print_emacs then top_stderr (str (top_buffer.prompt())); resynch_buffer top_buffer; try let input = (top_buffer.tokens, None) in - Vernac.process_expr top_buffer.tokens (read_sentence input) + Vernac.process_expr sid top_buffer.tokens (read_sentence sid (fst input)) with - | End_of_input | CErrors.Quit -> + | Stm.End_of_input | CErrors.Quit -> top_stderr (fnl ()); raise CErrors.Quit | CErrors.Drop -> (* Last chance *) if Mltop.is_ocaml_top() then raise CErrors.Drop - else Feedback.msg_error (str "There is no ML toplevel.") + else (Feedback.msg_error (str "There is no ML toplevel."); sid) (* Exception printing is done now by the feedback listener. *) (* XXX: We need this hack due to the side effects of the exception printer and the reliance of Stm.define on attaching crutial state to exceptions *) - | any -> ignore (CErrors.(iprint (push any))) - + | any -> ignore (CErrors.(iprint (push any))); sid (** Main coq loop : read vernacular expressions until Drop is entered. Ctrl-C is handled internally as Sys.Break instead of aborting Coq. @@ -349,10 +346,16 @@ let loop_flush_all () = let rec loop () = Sys.catch_break true; if !Flags.print_emacs then Vernacentries.qed_display_script := false; - Flags.coqtop_ui := true; try reset_input_buffer stdin top_buffer; - while true do do_vernac(); loop_flush_all () done + (* Be careful to keep this loop tail-recursive *) + let rec vernac_loop sid = + let nsid = do_vernac sid in + loop_flush_all (); + vernac_loop nsid + (* We recover the current stateid, threading from the caller is + not possible due exceptions. *) + in vernac_loop (Stm.get_current_state ()) with | CErrors.Drop -> () | CErrors.Quit -> exit 0 diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli index 8a34ded6d9..66bbf43f62 100644 --- a/toplevel/coqloop.mli +++ b/toplevel/coqloop.mli @@ -31,7 +31,7 @@ val coqloop_feed : Feedback.feedback -> unit (** Parse and execute one vernac command. *) -val do_vernac : unit -> unit +val do_vernac : Stateid.t -> Stateid.t (** Main entry point of Coq: read and execute vernac commands. *) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 4968804fde..c8f3ca1aba 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -175,15 +175,15 @@ let set_include d p implicit = let load_vernacular_list = ref ([] : (string * bool) list) let add_load_vernacular verb s = load_vernacular_list := ((CUnix.make_suffix s ".v"),verb) :: !load_vernacular_list -let load_vernacular () = - List.iter - (fun (s,b) -> +let load_vernacular sid = + List.fold_left + (fun sid (s,v) -> let s = Loadpath.locate_file s in if !Flags.beautify then - with_option beautify_file (Vernac.load_vernac b) s + with_option beautify_file (Vernac.load_vernac v sid) s else - Vernac.load_vernac b s) - (List.rev !load_vernacular_list) + Vernac.load_vernac v sid s) + sid (List.rev !load_vernacular_list) let load_vernacular_obj = ref ([] : string list) let add_vernac_obj s = load_vernacular_obj := s :: !load_vernacular_obj @@ -641,8 +641,9 @@ let init_toplevel arglist = load_vernac_obj (); require (); Stm.init (); - load_rcfile(); - load_vernacular (); + let sid = load_rcfile (Stm.get_current_state ()) in + (* XXX: We ignore this for now, but should be threaded to the toplevels *) + let _sid = load_vernacular sid in compile_files (); schedule_vio_checking (); schedule_vio_compilation (); diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index d5ceeaccd7..98458a57a2 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -13,111 +13,30 @@ open CErrors open Util open Flags open Vernacexpr +open Vernacprop (* The functions in this module may raise (unexplainable!) exceptions. Use the module Coqtoplevel, which catches these exceptions (the exceptions are explained only at the toplevel). *) -let user_error loc s = CErrors.user_err ~loc (str s) - -(* Navigation commands are allowed in a coqtop session but not in a .v file *) - -let rec is_navigation_vernac = function - | VernacResetInitial - | VernacResetName _ - | VernacBacktrack _ - | VernacBackTo _ - | VernacBack _ - | VernacStm _ -> true - | VernacRedirect (_, (_,c)) - | VernacTime (_,c) -> - is_navigation_vernac c (* Time Back* is harmless *) - | c -> is_deep_navigation_vernac c - -and is_deep_navigation_vernac = function - | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c - | _ -> false - -(* NB: Reset is now allowed again as asked by A. Chlipala *) - -let is_reset = function - | VernacResetInitial | VernacResetName _ -> true - | _ -> false - -let checknav_simple loc cmd = +let checknav_simple (loc, cmd) = if is_navigation_vernac cmd && not (is_reset cmd) then - user_error loc "Navigation commands forbidden in files." + CErrors.user_err ~loc (str "Navigation commands forbidden in files.") -let checknav_deep loc ast = +let checknav_deep (loc, ast) = if is_deep_navigation_vernac ast then - user_error loc "Navigation commands forbidden in nested commands." - -(* When doing Load on a file, two behaviors are possible: - - - either the history stack is grown by only one command, - the "Load" itself. This is mandatory for command-counting - interfaces (CoqIDE). - - - either each individual sub-commands in the file is added - to the history stack. This allows commands like Show Script - to work across the loaded file boundary (cf. bug #2820). - - The best of the two could probably be combined someday, - in the meanwhile we use a flag. *) - -let atomic_load = ref true - -let _ = - Goptions.declare_bool_option - { Goptions.optsync = true; - Goptions.optdepr = false; - Goptions.optname = "atomic registration of commands in a Load"; - Goptions.optkey = ["Atomic";"Load"]; - Goptions.optread = (fun () -> !atomic_load); - Goptions.optwrite = ((:=) atomic_load) } + CErrors.user_err ~loc (str "Navigation commands forbidden in nested commands.") let disable_drop = function | Drop -> CErrors.error "Drop is forbidden." | e -> e -(* Opening and closing a channel. Open it twice when verbose: the first - channel is used to read the commands, and the second one to print them. - Note: we could use only one thanks to seek_in, but seeking on and on in - the file we parse seems a bit risky to me. B.B. *) - -let open_file_twice_if verbosely longfname = - let in_chan = open_utf8_file_in longfname in - let verb_ch = - if verbosely then Some (open_utf8_file_in longfname) else None in - let po = Pcoq.Gram.parsable ~file:longfname (Stream.of_channel in_chan) in - (in_chan, longfname, (po, verb_ch)) - -let close_input in_chan (_,verb) = - try - close_in in_chan; - match verb with - | Some verb_ch -> close_in verb_ch - | _ -> () - with e when CErrors.noncritical e -> () - -let verbose_phrase verbch loc = - let loc = Loc.unloc loc in - match verbch with - | Some ch -> - let len = snd loc - fst loc in - let s = Bytes.create len in - seek_in ch (fst loc); - really_input ch s 0 len; - Feedback.msg_notice (str (Bytes.to_string s)) - | None -> () - -exception End_of_input - -let parse_sentence = Flags.with_option Flags.we_are_parsing - (fun (po, verbch) -> - match Pcoq.Gram.entry_parse Pcoq.main_entry po with - | Some (loc,_ as com) -> verbose_phrase verbch loc; com - | None -> raise End_of_input) +(* Echo from a buffer based on position. + XXX: Should move to utility file. *) +let vernac_echo loc in_chan = let open Loc in + let len = loc.ep - loc.bp in + seek_in in_chan loc.bp; + Feedback.msg_notice @@ str @@ really_input_string in_chan len (* vernac parses the given stream, executes interpfun on the syntax tree it * parses, and is verbose on "primitives" commands if verbosely is true *) @@ -184,20 +103,43 @@ let print_cmd_header loc com = Pp.pp_with !Topfmt.std_ft (pp_cmd_header loc com); Format.pp_print_flush !Topfmt.std_ft () -let rec interp_vernac po chan_beautify checknav (loc,com) = +let pr_open_cur_subgoals () = + try Printer.pr_open_subgoals () + with Proof_global.NoCurrentProof -> Pp.str "" + +let rec interp_vernac sid po (loc,com) = let interp = function | VernacLoad (verbosely, fname) -> let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in let fname = CUnix.make_suffix fname ".v" in let f = Loadpath.locate_file fname in - load_vernac verbosely f - - | v -> Stm.interp (Flags.is_verbose()) (loc,v) + load_vernac verbosely sid f + | v -> + try + let nsid, ntip = Stm.add sid (Flags.is_verbose()) (loc,v) in + + (* Main STM interaction *) + if ntip <> `NewTip then + anomaly (str "vernac.ml: We got an unfocus operation on the toplevel!"); + (* Due to bug #5363 we cannot use observe here as we should, + it otherwise reveals bugs *) + (* Stm.observe nsid; *) + Stm.finish (); + + (* We could use a more refined criteria depending on the + vernac. For now we imitate the old approach. *) + let print_goals = not (!Flags.batch_mode || is_query v) in + + if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ()); + nsid + + with exn when CErrors.noncritical exn -> + ignore(Stm.edit_at sid); + raise exn in try - checknav loc com; - if !beautify then pr_new_syntax po chan_beautify loc (Some com); - (* XXX: This is not 100% correct if called from an IDE context *) + (* The -time option is only supported from console-based + clients due to the way it prints. *) if !Flags.time then print_cmd_header loc com; let com = if !Flags.time then VernacTime (loc,com) else com in interp com @@ -208,26 +150,39 @@ let rec interp_vernac po chan_beautify checknav (loc,com) = else iraise (reraise, info) (* Load a vernac file. CErrors are annotated with file and location *) -and load_vernac verbosely file = +and load_vernac verbosely sid file = let chan_beautify = if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout in - let (in_chan, fname, input) = open_file_twice_if verbosely file in + let in_chan = open_utf8_file_in file in + let in_echo = if verbosely then Some (open_utf8_file_in file) else None in + let in_pa = Pcoq.Gram.parsable ~file (Stream.of_channel in_chan) in + let rsid = ref sid in try (* we go out of the following infinite loop when a End_of_input is * raised, which means that we raised the end of the file being loaded *) while true do - let loc_ast = Flags.silently parse_sentence input in - CWarnings.set_current_loc (fst loc_ast); - Flags.silently (interp_vernac (fst input) chan_beautify checknav_simple) loc_ast; - done + let loc, ast = Stm.parse_sentence !rsid in_pa in + + (* Printing of vernacs *) + if !beautify then pr_new_syntax in_pa chan_beautify loc (Some ast); + Option.iter (vernac_echo loc) in_echo; + + checknav_simple (loc, ast); + let nsid = Flags.silently (interp_vernac !rsid in_pa) (loc, ast) in + rsid := nsid + done; + !rsid with any -> (* whatever the exception *) let (e, info) = CErrors.push any in - close_input in_chan input; (* we must close the file first *) + close_in in_chan; + Option.iter close_in in_echo; match e with - | End_of_input -> + | Stm.End_of_input -> + (* Is this called so comments at EOF are printed? *) if !beautify then - pr_new_syntax (fst input) chan_beautify (Loc.make_loc (max_int,max_int)) None; + pr_new_syntax in_pa chan_beautify (Loc.make_loc (max_int,max_int)) None; if !Flags.beautify_file then close_out chan_beautify; + !rsid | reraise -> if !Flags.beautify_file then close_out chan_beautify; iraise (disable_drop e, info) @@ -239,7 +194,9 @@ and load_vernac verbosely file = of a new state label). An example of state-preserving command is one coming from the query panel of Coqide. *) -let process_expr po loc_ast = interp_vernac po stdout checknav_deep loc_ast +let process_expr sid po loc_ast = + checknav_deep loc_ast; + interp_vernac sid po loc_ast (* XML output hooks *) let (f_xml_start_library, xml_start_library) = Hook.make ~default:ignore () @@ -308,7 +265,7 @@ let compile verbosely f = Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n"); if !Flags.xml_export then Hook.get f_xml_start_library (); let wall_clock1 = Unix.gettimeofday () in - let _ = load_vernac verbosely long_f_dot_v in + let _ = load_vernac verbosely (Stm.get_current_state ()) long_f_dot_v in Stm.join (); let wall_clock2 = Unix.gettimeofday () in check_pending_proofs (); @@ -328,7 +285,7 @@ let compile verbosely f = let ldir = Flags.verbosely Library.start_library long_f_dot_vio in Dumpglob.noglob (); Stm.set_compilation_hints long_f_dot_vio; - let _ = load_vernac verbosely long_f_dot_v in + let _ = load_vernac verbosely (Stm.get_current_state ()) long_f_dot_v in Stm.finish (); check_pending_proofs (); Stm.snapshot_vio ldir long_f_dot_vio; diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index 0d9f5871a3..e75f8f9e85 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -8,30 +8,16 @@ (** Parsing of vernacular. *) -(** Read a vernac command on the specified input (parse only). - Raises [End_of_file] if EOF (or Ctrl-D) is reached. *) - -val parse_sentence : Pcoq.Gram.coq_parsable * in_channel option -> - Loc.t * Vernacexpr.vernac_expr - (** Reads and executes vernac commands from a stream. *) +val process_expr : Stateid.t -> Pcoq.Gram.coq_parsable -> Vernacexpr.vernac_expr Loc.located -> Stateid.t -exception End_of_input +(** [load_vernac echo sid file] Loads [file] on top of [sid], will + echo the commands if [echo] is set. *) +val load_vernac : bool -> Stateid.t -> string -> Stateid.t -val process_expr : Pcoq.Gram.coq_parsable -> Loc.t * Vernacexpr.vernac_expr -> unit +(** Compile a vernac file, (f is assumed without .v suffix) *) +val compile : bool -> string -> unit (** Set XML hooks *) val xml_start_library : (unit -> unit) Hook.t val xml_end_library : (unit -> unit) Hook.t - -(** Load a vernac file, verbosely or not. Errors are annotated with file - and location *) - -val load_vernac : bool -> string -> unit - - -(** Compile a vernac file, verbosely or not (f is assumed without .v suffix) *) - -val compile : bool -> string -> unit - -val is_navigation_vernac : Vernacexpr.vernac_expr -> bool diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 283c095eb6..d631fae8a8 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -1,3 +1,4 @@ +Vernacprop Lemmas Himsg ExplainErr diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml new file mode 100644 index 0000000000..ec78d6012f --- /dev/null +++ b/vernac/vernacprop.ml @@ -0,0 +1,53 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* true + | VernacRedirect (_, (_,c)) + | VernacTime (_,c) -> + is_navigation_vernac c (* Time Back* is harmless *) + | c -> is_deep_navigation_vernac c + +and is_deep_navigation_vernac = function + | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c + | _ -> false + +(* NB: Reset is now allowed again as asked by A. Chlipala *) +let is_reset = function + | VernacResetInitial | VernacResetName _ -> true + | _ -> false + +let is_debug cmd = match cmd with + | VernacSetOption (["Ltac";"Debug"], _) -> true + | _ -> false + +let is_query cmd = match cmd with + | VernacChdir None + | VernacMemOption _ + | VernacPrintOption _ + | VernacCheckMayEval _ + | VernacGlobalCheck _ + | VernacPrint _ + | VernacSearch _ + | VernacLocate _ -> true + | _ -> false + +let is_undo cmd = match cmd with + | VernacUndo _ | VernacUndoTo _ -> true + | _ -> false diff --git a/vernac/vernacprop.mli b/vernac/vernacprop.mli new file mode 100644 index 0000000000..c235ecfb57 --- /dev/null +++ b/vernac/vernacprop.mli @@ -0,0 +1,19 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* bool +val is_deep_navigation_vernac : vernac_expr -> bool +val is_reset : vernac_expr -> bool +val is_query : vernac_expr -> bool +val is_debug : vernac_expr -> bool +val is_undo : vernac_expr -> bool -- cgit v1.2.3 From 46856a80958f1aaa3242b6d37f018df9528e5e5f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 22 Feb 2017 02:08:29 +0100 Subject: [vernac] vernacentries.mli cleanup This header file had accumulated quite a bit of cruft over the years, we clean it up while we are at it. No functional change as all the removed variables/methods were noops long time ago. --- ide/ide_slave.ml | 3 --- toplevel/coqloop.ml | 1 - toplevel/coqtop.ml | 1 - vernac/vernacentries.ml | 22 +++------------------- vernac/vernacentries.mli | 32 +------------------------------- 5 files changed, 4 insertions(+), 55 deletions(-) diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index bc7ce38836..65eececf7f 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -466,9 +466,6 @@ let loop () = let xml_ic = Xml_parser.make (Xml_parser.SLexbuf in_lb) in let () = Xml_parser.check_eof xml_ic false in ignore (Feedback.add_feeder (slave_feeder (!msg_format ()) xml_oc)); - (* We'll handle goal fetching and display in our own way *) - Vernacentries.enable_goal_printing := false; - Vernacentries.qed_display_script := false; while not !quit do try let xml_query = Xml_parser.parse xml_ic in diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 17d8f5f49b..9478542c17 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -345,7 +345,6 @@ let loop_flush_all () = let rec loop () = Sys.catch_break true; - if !Flags.print_emacs then Vernacentries.qed_display_script := false; try reset_input_buffer stdin top_buffer; (* Be careful to keep this loop tail-recursive *) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index c8f3ca1aba..6f9ffe02b1 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -250,7 +250,6 @@ let set_emacs () = if not (Option.is_empty !toploop) then error "Flag -emacs is incompatible with a custom toplevel loop"; Flags.print_emacs := true; - Vernacentries.qed_display_script := false; color := `OFF (** Options for CoqIDE *) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index ca03ba3f3a..5e5df99709 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -84,24 +84,10 @@ let show_universes () = Feedback.msg_notice (Evd.pr_evar_universe_context (Evd.evar_universe_context sigma)); Feedback.msg_notice (str"Normalized constraints: " ++ Univ.pr_universe_context_set (Evd.pr_evd_level sigma) ctx) -let show_prooftree () = - (* Spiwack: proof tree is currently not working *) - () - -let enable_goal_printing = ref true - -let print_subgoals () = - if !enable_goal_printing && is_verbose () - then begin - Feedback.msg_notice (pr_open_subgoals ()) - end - -let try_print_subgoals () = - try print_subgoals () with Proof_global.NoCurrentProof | UserError _ -> () - - - (* Simulate the Intro(s) tactic *) +(* Spiwack: proof tree is currently not working *) +let show_prooftree () = () +(* Simulate the Intro(s) tactic *) let show_intro all = let pf = get_pftreestate() in let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in @@ -511,8 +497,6 @@ let vernac_start_proof locality p kind l lettop = (str "Let declarations can only be used in proof editing mode."); start_proof_and_print (local, p, Proof kind) l no_hook -let qed_display_script = ref true - let vernac_end_proof ?proof = function | Admitted -> save_proof ?proof Admitted | Proved (_,_) as e -> save_proof ?proof e diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index 7cdc8dd064..fb2899515f 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -11,42 +11,15 @@ open Misctypes val dump_global : Libnames.reference or_by_notation -> unit (** Vernacular entries *) - -val show_prooftree : unit -> unit - -val show_node : unit -> unit - val vernac_require : Libnames.reference option -> bool option -> Libnames.reference list -> unit -(** This function can be used by any command that want to observe terms - in the context of the current goal *) -val get_current_context_of_args : int option -> Evd.evar_map * Environ.env - (** The main interpretation function of vernacular expressions *) -val interp : +val interp : ?verbosely:bool -> ?proof:Proof_global.closed_proof -> Loc.t * Vernacexpr.vernac_expr -> unit -(** Print subgoals when the verbose flag is on. - Meant to be used inside vernac commands from plugins. *) - -val print_subgoals : unit -> unit -val try_print_subgoals : unit -> unit - -(** The printing of goals via [print_subgoals] or during - [interp] can be controlled by the following flag. - Used for instance by coqide, since it has its own - goal-fetching mechanism. *) - -val enable_goal_printing : bool ref - -(** Should Qed try to display the proof script ? - True by default, but false in ProofGeneral and coqIDE *) - -val qed_display_script : bool ref - (** Prepare a "match" template for a given inductive type. For each branch of the match, we list the constructor name followed by enough pattern variables. @@ -55,9 +28,6 @@ val qed_display_script : bool ref val make_cases : string -> string list list -val vernac_end_proof : - ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit - val with_fail : bool -> (unit -> unit) -> unit val command_focus : unit Proof.focus_kind -- cgit v1.2.3 From 55bddb4bf35fa68318aa57a5fa8a113d1fe51159 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 22 Feb 2017 02:31:16 +0100 Subject: [flags] Documentation and a minor tweak. Mostly documentation and making a couple of local flags, local. --- interp/constrextern.ml | 16 +++++++++++++++- lib/flags.ml | 7 ------- lib/flags.mli | 23 ++++++++++++++++++----- printing/printer.ml | 17 +++++++++++++++-- vernac/vernacentries.ml | 18 ------------------ 5 files changed, 48 insertions(+), 33 deletions(-) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 925e9517c7..5bf49b7334 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -85,6 +85,20 @@ let without_specific_symbols l f = (**********************************************************************) (* Control printing of records *) +(* Set Record Printing flag *) +let record_print = ref true + +let _ = + let open Goptions in + declare_bool_option + { optsync = true; + optdepr = false; + optname = "record printing"; + optkey = ["Printing";"Records"]; + optread = (fun () -> !record_print); + optwrite = (fun b -> record_print := b) } + + let is_record indsp = try let _ = Recordops.lookup_structure indsp in @@ -658,7 +672,7 @@ let rec extern inctx scopes vars r = () else if PrintingConstructor.active (fst cstrsp) then raise Exit - else if not !Flags.record_print then + else if not !record_print then raise Exit; let projs = struc.Recordops.s_PROJ in let locals = struc.Recordops.s_PROJKIND in diff --git a/lib/flags.ml b/lib/flags.ml index ef5eddfb29..d87d9e7295 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -95,7 +95,6 @@ let time = ref false let raw_print = ref false -let record_print = ref true let univ_print = ref false @@ -181,12 +180,6 @@ let warn = ref true let make_warn flag = warn := flag; () let if_warn f x = if !warn then f x -(* The number of printed hypothesis in a goal *) - -let print_hyps_limit = ref (None : int option) -let set_print_hyps_limit n = print_hyps_limit := n -let print_hyps_limit () = !print_hyps_limit - (* Flags for external tools *) let browser_cmd_fmt = diff --git a/lib/flags.mli b/lib/flags.mli index f5e1c96f9a..c5c4a15aaa 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -8,6 +8,8 @@ (** Global options of the system. *) +(** Command-line flags *) + val boot : bool ref val load_init : bool ref @@ -16,8 +18,11 @@ type compilation_mode = BuildVo | BuildVio | Vio2Vo val compilation_mode : compilation_mode ref val compilation_output_name : string option ref +(* Flag set when the test-suite is called. Its only effect to display + verbose information for `Fail` *) val test_mode : bool ref +(** Async-related flags *) type async_proofs = APoff | APonLazy | APon val async_proofs_mode : async_proofs ref type cache = Force @@ -47,18 +52,26 @@ val in_toplevel : bool ref val profile : bool (* Legacy flags *) + +(* -emacs option: printing includes emacs tags, will affect stm caching. *) val print_emacs : bool ref +(* -xml option: xml hooks will be called *) val xml_export : bool ref +(* -ide_slave: printing will be more verbose, will affect stm caching *) val ide_slave : bool ref val ideslave_coqtop_flags : string option ref +(* -time option: every command will be wrapped with `Time` *) val time : bool ref +(* development flag to detect race conditions, it should go away. *) val we_are_parsing : bool ref +(* Set Printing All flag. For some reason it is a global flag *) val raw_print : bool ref -val record_print : bool ref + +(* Univ print flag, never set anywere. Maybe should belong to Univ? *) val univ_print : bool ref type compat_version = V8_2 | V8_3 | V8_4 | V8_5 | V8_6 | Current @@ -68,9 +81,12 @@ val version_strictly_greater : compat_version -> bool val version_less_or_equal : compat_version -> bool val pr_version : compat_version -> string +(* Beautify command line flags, should move to printing? *) val beautify : bool ref val beautify_file : bool ref +(* Silent/verbose, both actually controlled by a single flag so they + are mutually exclusive *) val make_silent : bool -> unit val is_silent : unit -> bool val is_verbose : unit -> bool @@ -79,6 +95,7 @@ val verbosely : ('a -> 'b) -> 'a -> 'b val if_silent : ('a -> unit) -> 'a -> unit val if_verbose : ('a -> unit) -> 'a -> unit +(* Miscellaneus flags for vernac *) val make_auto_intros : bool -> unit val is_auto_intros : unit -> bool @@ -110,10 +127,6 @@ val without_option : bool ref -> ('a -> 'b) -> 'a -> 'b (** Temporarily extends the reference to a list *) val with_extra_values : 'c list ref -> 'c list -> ('a -> 'b) -> 'a -> 'b -(** If [None], no limit *) -val set_print_hyps_limit : int option -> unit -val print_hyps_limit : unit -> int option - (** Options for external tools *) (** Returns string format for default browser to use from Coq or CoqIDE *) diff --git a/printing/printer.ml b/printing/printer.ml index 5e7e9ce548..f00350c6a5 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -365,8 +365,21 @@ let pr_context_limit_compact ?n env sigma = let pr_context_unlimited_compact env sigma = pr_context_limit_compact env sigma -let pr_context_of env sigma = - match Flags.print_hyps_limit () with +(* The number of printed hypothesis in a goal *) +(* If [None], no limit *) +let print_hyps_limit = ref (None : int option) + +let _ = + let open Goptions in + declare_int_option + { optsync = false; + optdepr = false; + optname = "the hypotheses limit"; + optkey = ["Hyps";"Limit"]; + optread = (fun () -> !print_hyps_limit); + optwrite = (fun x -> print_hyps_limit := x) } + +let pr_context_of env sigma = match !print_hyps_limit with | None -> hv 0 (pr_context_limit_compact env sigma) | Some n -> hv 0 (pr_context_limit_compact ~n env sigma) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 5e5df99709..89d069e804 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1358,15 +1358,6 @@ let _ = optread = (fun () -> !Flags.raw_print); optwrite = (fun b -> Flags.raw_print := b) } -let _ = - declare_bool_option - { optsync = true; - optdepr = false; - optname = "record printing"; - optkey = ["Printing";"Records"]; - optread = (fun () -> !Flags.record_print); - optwrite = (fun b -> Flags.record_print := b) } - let _ = declare_bool_option { optsync = true; @@ -1417,15 +1408,6 @@ let _ = optread = (fun _ -> None); optwrite = (fun _ -> ()) } -let _ = - declare_int_option - { optsync = false; - optdepr = false; - optname = "the hypotheses limit"; - optkey = ["Hyps";"Limit"]; - optread = Flags.print_hyps_limit; - optwrite = Flags.set_print_hyps_limit } - let _ = declare_int_option { optsync = true; -- cgit v1.2.3 From 2f0a56562112c4bd66082fb3eafffb8cf6f03a88 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 29 Mar 2017 17:47:06 +0200 Subject: [stm] Improve error messages on add/parse. As suggested by @psteckler in #524 , we give more explicit information about what is wrong. We also provide some debug information for the possible dangerous case of having the tip go out of sync with the real installed state (which will make parsing fail if there was some changes to the parser). We also fix a couple of typos noticed by Paul, thanks Paul. --- dev/doc/changes.txt | 4 ++-- stm/stm.ml | 18 ++++++++++++++++-- 2 files changed, 18 insertions(+), 4 deletions(-) diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 7e7bb98580..fe0b587b11 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -148,7 +148,7 @@ document type". This allows for a more uniform handling of printing - The main parsing entry point has also been moved to the `Stm`. Parsing is considered a synchronous operation so it will - either succeed of emit an exception. + either succeed or raise an exception. - `Feedback` is now only emitted for asynchronous operations. As a consequence, it always carries a valid stateid and the type has @@ -167,7 +167,7 @@ document type". This allows for a more uniform handling of printing ** XML Protocol ** -- The legacy `interp` call has been turned into a noop. +- The legacy `Interp` call has been turned into a noop. ========================================= = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 = diff --git a/stm/stm.ml b/stm/stm.ml index 8d212a6a08..d11aea6c41 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -699,6 +699,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 @@ -2669,9 +2672,19 @@ let parse_sentence sid pa = 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."); + (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) 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 @@ -2721,7 +2734,8 @@ let add ~ontop ?newtip verb (loc, ast) = let cur_tip = VCS.cur_tip () in if not (Stateid.equal ontop cur_tip) then user_err ~hdr:"Stm.add" - (str "You used Stm.add on a different state than the tip" ++ fnl () ++ + (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 ontop loc in CWarnings.set_current_loc loc; -- cgit v1.2.3 From cf24cedb2926fa00db222eeac48e88a6078b4444 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 30 Mar 2017 14:58:12 +0200 Subject: [stm] [nit] Centralize compile-time debug flag. --- stm/stm.ml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/stm/stm.ml b/stm/stm.ml index d11aea6c41..574426f92d 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -6,13 +6,16 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* enable in case of stm problems *) +let stm_debug = false + let stm_pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr let stm_pp_err pp = Format.eprintf "%s] @[%a@]\n" (System.process_id ()) Pp.pp_with pp; flush stderr -let stm_prerr_endline s = if false then begin stm_pr_err (s ()) end else () -let stm_prerr_debug s = if !Flags.debug then begin stm_pr_err (s ()) end else () +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_pperr_endline s = if false 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 @@ -2678,7 +2681,7 @@ let parse_sentence sid pa = (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) then + 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) ++ -- cgit v1.2.3 From b63b9a86b09856262b5b7bb2b3bb01f704032d41 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 7 Apr 2017 03:45:27 +0200 Subject: [toplevel] [stm] cleanup in module open --- stm/stm.ml | 129 +++++++++++++++++++++++++--------------------------- toplevel/coqloop.ml | 27 +++++------ toplevel/coqtop.ml | 21 ++++----- 3 files changed, 83 insertions(+), 94 deletions(-) diff --git a/stm/stm.ml b/stm/stm.ml index 574426f92d..0f963dca98 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -17,14 +17,11 @@ 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 let execution_error state_id loc msg = feedback ~id:state_id @@ -80,7 +77,7 @@ type aast = { 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 () @@ -115,13 +112,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; @@ -210,7 +207,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 @@ -346,7 +343,7 @@ end = struct (* {{{ *) | Sideff None -> "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 @@ -476,8 +473,8 @@ end = struct (* {{{ *) 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 + | VernacDefinition (_,((_,i),_),_) -> Names.string_of_id i + | VernacStartTheoremProof (_,[Some ((_,i),_),_],_) -> Names.string_of_id i | _ -> "branch") let edit_branch = Branch.make "edit" let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind @@ -533,7 +530,7 @@ end = struct (* {{{ *) | { 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 ^ + | _ -> anomaly Pp.(str("Cannot slice from "^ Stateid.to_string block_start ^ " to "^Stateid.to_string block_stop)) in aux block_stop @@ -586,11 +583,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 = @@ -601,7 +598,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 @@ -682,14 +679,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 @@ -765,13 +762,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 @@ -822,7 +819,7 @@ end = struct (* {{{ *) 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 stm_prerr_endline (fun () -> "defining "^str_id^" (cache="^ if cache = `Yes then "Y)" else if cache = `Shallow then "S)" else "N)"); @@ -897,9 +894,9 @@ let indent_script_item ((ng1,ngl1),nl,beginend,ppl) (cmd,ng) = | VernacBullet _ -> pred ind, nl, beginend | _ -> ind, nl, beginend in - let pp = + let pp = Pp.( (if nl then fnl () else mt ()) ++ - (hov (ind+1) (str (String.make ind ' ') ++ Ppvernac.pr_vernac cmd)) + (hov (ind+1) (str (String.make ind ' ') ++ Ppvernac.pr_vernac cmd))) in (new_ngl, new_nl, new_beginend, pp :: ppl) @@ -939,7 +936,7 @@ let show_script ?proof () = 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)) + msg_notice Pp.(v 0 (prlist_with_sep fnl (fun x -> x) indented_cmds)) with Vcs_aux.Expired -> () end @@ -966,15 +963,15 @@ let stm_vernac_interp ?proof id ?route { verbose; loc; expr } = in let aux_interp cmd = if is_filtered_command cmd then - stm_pperr_endline Pp.(fun () -> str "ignoring " ++ pr_vernac expr) + 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 " ++ pr_vernac expr); + stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr); try Vernacentries.interp ?verbosely:(Some verbose) ?proof (loc, expr) with e -> let e = CErrors.push e in - iraise Hooks.(call_process_error_once e) + Exninfo.iraise Hooks.(call_process_error_once e) in aux_interp expr (****************************** CRUFT *****************************************) @@ -1013,7 +1010,7 @@ end = struct (* {{{ *) let info = VCS.get_info oid in match info.vcs_backup with | None, _ -> - anomaly(str"Backtrack.backto "++str(Stateid.to_string oid)++ + anomaly Pp.(str"Backtrack.backto "++str(Stateid.to_string oid)++ str": a state with no vcs_backup") | Some vcs, _ -> VCS.restore vcs @@ -1021,8 +1018,8 @@ end = struct (* {{{ *) 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 = @@ -1083,7 +1080,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) @@ -1107,7 +1104,7 @@ end = struct (* {{{ *) with | Not_found -> CErrors.user_err ~hdr:"undo_vernac_classifier" - (str "Cannot undo") + Pp.(str "Cannot undo") end (* }}} *) @@ -1139,7 +1136,7 @@ let record_pb_time proof_name loc time = hints := Aux_file.set !hints Loc.ghost 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) @@ -1174,7 +1171,7 @@ let proof_block_delimiters = ref [] let register_proof_block_delimiter name static dynamic = if List.mem_assoc name !proof_block_delimiters then - CErrors.user_err ~hdr:"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 @@ -1210,7 +1207,7 @@ let detect_proof_block id name = end with Not_found -> CErrors.user_err ~hdr:"STM" - (str "Unknown proof block delimiter " ++ str name) + Pp.(str "Unknown proof block delimiter " ++ str name) ) (****************************** THE SCHEDULER *********************************) (******************************************************************************) @@ -1277,7 +1274,7 @@ 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 = @@ -1350,9 +1347,9 @@ 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); - execution_error start Loc.ghost (strbrk s); + execution_error start Loc.ghost (Pp.strbrk s); feedback (InProgress ~-1) let build_proof_here ~drop_pt (id,valid) loc eop = @@ -1433,7 +1430,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 @@ -1449,10 +1446,10 @@ 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)); @@ -1505,7 +1502,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 = @@ -1536,7 +1533,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) -> @@ -1546,16 +1543,16 @@ end = struct (* {{{ *) | { step = `Qed ( { qast = { loc } }, _) } | { step = `Sideff (`Ast ( { loc }, _)) } -> let start, stop = Loc.unloc loc in - msg_error ( + 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 @@ -1714,7 +1711,7 @@ end = struct (* {{{ *) type response = | RespBuiltSubProof of output - | RespError of std_ppcmds + | RespError of Pp.std_ppcmds | RespNoProgress exception NoProgress @@ -1773,7 +1770,7 @@ end = struct (* {{{ *) List.for_all (Context.Named.Declaration.for_all (Evarutil.is_ground_term sigma0)) Evd.(evar_context g)) then - CErrors.user_err ~hdr:"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 @@ -1786,7 +1783,7 @@ 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 CErrors.user_err ~hdr:"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) @@ -1974,7 +1971,7 @@ let collect_proof keep cur hd brkind 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 is_defined = function | _, { expr = VernacEndProof (Proved ((Transparent|Opaque (Some _)),_)) } -> @@ -2095,13 +2092,13 @@ 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 @@ -2215,7 +2212,7 @@ let known_state ?(redefine_qed=false) ~cache id = 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) -> @@ -2298,9 +2295,9 @@ let known_state ?(redefine_qed=false) ~cache id = | `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) @@ -2354,7 +2351,7 @@ let observe id = let e = CErrors.push e in VCS.print (); VCS.restore vcs; - iraise e + Exninfo.iraise e let finish () = let head = VCS.current_branch () in @@ -2441,12 +2438,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)) + 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 = - if e = CErrors.Drop then iraise (e, info) else + if e = CErrors.Drop then Exninfo.iraise (e, info) else match Stateid.get info with | None -> VCS.restore vcs; @@ -2457,7 +2454,7 @@ let handle_failure (e, info) vcs = stm_prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id); VCS.restore vcs; VCS.print (); - iraise (e, info) + Exninfo.iraise (e, info) let snapshot_vio ldir long_f_dot_vo = finish (); @@ -2519,7 +2516,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) (try stm_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 + Exninfo.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 @@ -2695,7 +2692,7 @@ let parse_sentence sid pa = | Some com -> com with e when CErrors.noncritical e -> let (e, info) = CErrors.push e in - iraise (e, info)) + Exninfo.iraise (e, info)) () (* You may need to know the len + indentation of previous command to compute @@ -2894,7 +2891,7 @@ let edit_at 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 @@ -2924,7 +2921,7 @@ let proofname b = match VCS.get_branch b with | _ -> None let get_all_proof_names () = - List.map unmangle (List.map_filter proofname (VCS.branches ())) + List.map unmangle (CList.map_filter proofname (VCS.branches ())) (* Export hooks *) let state_computed_hook = Hooks.state_computed_hook diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 9478542c17..4641a2bc86 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -7,11 +7,6 @@ (************************************************************************) open Pp -open CErrors -open Util -open Flags -open Vernac -open Pcoq let top_stderr x = Format.fprintf !Topfmt.err_ft "@[%a@]%!" pp_with x @@ -24,7 +19,7 @@ type input_buffer = { mutable str : Bytes.t; (* buffer of already read characters *) mutable len : int; (* number of chars in the buffer *) mutable bols : int list; (* offsets in str of beginning of lines *) - mutable tokens : Gram.coq_parsable; (* stream of tokens *) + mutable tokens : Pcoq.Gram.coq_parsable; (* stream of tokens *) mutable start : int } (* stream count of the first char of the buffer *) (* Double the size of the buffer. *) @@ -61,7 +56,7 @@ let prompt_char ic ibuf count = | ll::_ -> Int.equal ibuf.len ll | [] -> Int.equal ibuf.len 0 in - if bol && not !print_emacs then top_stderr (str (ibuf.prompt())); + if bol && not !Flags.print_emacs then top_stderr (str (ibuf.prompt())); try let c = input_char ic in if c == '\n' then ibuf.bols <- (ibuf.len+1) :: ibuf.bols; @@ -78,7 +73,7 @@ let reset_input_buffer ic ibuf = ibuf.str <- Bytes.empty; ibuf.len <- 0; ibuf.bols <- []; - ibuf.tokens <- Gram.parsable (Stream.from (prompt_char ic ibuf)); + ibuf.tokens <- Pcoq.Gram.parsable (Stream.from (prompt_char ic ibuf)); ibuf.start <- 0 (* Functions to print underlined locations from an input buffer. *) @@ -89,7 +84,7 @@ module TopErr = struct let get_bols_of_loc ibuf (bp,ep) = let add_line (b,e) lines = - if b < 0 || e < b then anomaly (Pp.str "Bad location"); + if b < 0 || e < b then CErrors.anomaly (Pp.str "Bad location"); match lines with | ([],None) -> ([], Some (b,e)) | (fl,oe) -> ((b,e)::fl, oe) @@ -174,7 +169,7 @@ let error_info_for_buffer ?loc buf = let fname = loc.Loc.fname in let hl, loc = (* We are in the toplevel *) - if String.equal fname "" then + if CString.equal fname "" then let nloc = adjust_loc_buf buf loc in if valid_buffer_loc buf loc then (fnl () ++ print_highlight_location buf nloc, nloc) @@ -223,7 +218,7 @@ let make_emacs_prompt() = let pending = Stm.get_all_proof_names() in let pendingprompt = List.fold_left - (fun acc x -> acc ^ (if String.is_empty acc then "" else "|") ^ Names.Id.to_string x) + (fun acc x -> acc ^ (if CString.is_empty acc then "" else "|") ^ Names.Id.to_string x) "" pending in let proof_info = if dpth >= 0 then string_of_int dpth else "0" in if !Flags.print_emacs then statnum ^ " |" ^ pendingprompt ^ "| " ^ proof_info ^ " < " @@ -243,7 +238,7 @@ let top_buffer = str = Bytes.empty; len = 0; bols = []; - tokens = Gram.parsable (Stream.of_list []); + tokens = Pcoq.Gram.parsable (Stream.of_list []); start = 0 } let set_prompt prompt = @@ -260,7 +255,7 @@ let parse_to_dot = | Tok.EOI -> raise Stm.End_of_input | _ -> dot st in - Gram.Entry.of_parser "Coqtoplevel.dot" dot + Pcoq.Gram.Entry.of_parser "Coqtoplevel.dot" dot (* If an error occurred while parsing, we try to read the input until a dot token is encountered. @@ -268,7 +263,7 @@ let parse_to_dot = let rec discard_to_dot () = try - Gram.entry_parse parse_to_dot top_buffer.tokens + Pcoq.Gram.entry_parse parse_to_dot top_buffer.tokens with | Token.Error _ | CLexer.Error.E _ -> discard_to_dot () | Stm.End_of_input -> raise Stm.End_of_input @@ -280,7 +275,7 @@ let read_sentence sid input = let reraise = CErrors.push reraise in discard_to_dot (); TopErr.print_toplevel_parse_error reraise top_buffer; - iraise reraise + Exninfo.iraise reraise (** Coqloop Console feedback handler *) let coqloop_feed (fb : Feedback.feedback) = let open Feedback in @@ -312,7 +307,7 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in let do_vernac sid = top_stderr (fnl()); - if !print_emacs then top_stderr (str (top_buffer.prompt())); + if !Flags.print_emacs then top_stderr (str (top_buffer.prompt())); resynch_buffer top_buffer; try let input = (top_buffer.tokens, None) in diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 6f9ffe02b1..d3c89ede80 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -8,11 +8,8 @@ open Pp open CErrors -open Util open Flags -open Names open Libnames -open States open Coqinit let () = at_exit flush_all @@ -133,10 +130,10 @@ let engage () = let set_batch_mode () = batch_mode := true -let toplevel_default_name = DirPath.make [Id.of_string "Top"] +let toplevel_default_name = Names.(DirPath.make [Id.of_string "Top"]) let toplevel_name = ref toplevel_default_name let set_toplevel_name dir = - if DirPath.is_empty dir then error "Need a non empty toplevel module name"; + if Names.DirPath.is_empty dir then error "Need a non empty toplevel module name"; toplevel_name := dir let remove_top_ml () = Mltop.remove () @@ -150,9 +147,9 @@ let set_inputstate s = warn_deprecated_inputstate (); inputstate:=s let inputstate () = - if not (String.is_empty !inputstate) then + if not (CString.is_empty !inputstate) then let fname = Loadpath.locate_file (CUnix.make_suffix !inputstate ".coq") in - intern_state fname + States.intern_state fname let warn_deprecated_outputstate = CWarnings.create ~name:"deprecated-outputstate" ~category:"deprecated" @@ -164,9 +161,9 @@ let set_outputstate s = warn_deprecated_outputstate (); outputstate:=s let outputstate () = - if not (String.is_empty !outputstate) then + if not (CString.is_empty !outputstate) then let fname = CUnix.make_suffix !outputstate ".coq" in - extern_state fname + States.extern_state fname let set_include d p implicit = let p = dirpath_of_string p in @@ -379,7 +376,7 @@ let get_host_port opt s = let get_error_resilience opt = function | "on" | "all" | "yes" -> `All | "off" | "no" -> `None - | s -> `Only (String.split ',' s) + | s -> `Only (CString.split ',' s) let get_task_list s = List.map int_of_string (Str.split (Str.regexp ",") s) @@ -624,7 +621,7 @@ let init_toplevel arglist = init_load_path (); Option.iter Mltop.load_ml_object_raw !toploop; let extras = !toploop_init extras in - if not (List.is_empty extras) then begin + if not (CList.is_empty extras) then begin prerr_endline ("Don't know what to do with "^String.concat " " extras); prerr_endline "See -help for the list of supported options"; exit 1 @@ -633,7 +630,7 @@ let init_toplevel arglist = inputstate (); Mltop.init_known_plugins (); engage (); - if (not !batch_mode || List.is_empty !compile_list) + if (not !batch_mode || CList.is_empty !compile_list) && Global.env_is_initial () then Declaremods.start_library !toplevel_name; init_library_roots (); -- cgit v1.2.3