From da0d6da035206778c1d99ef51f471b4b22016492 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 24 Apr 2017 18:42:03 +0200 Subject: [toplevel] Don't mask critical exceptions in vernac interpretation. Indeed we were not correctly backtracking in the case of StackOverflow. It makes sense to remove the inner handler which is a leftover of a previous attempt, and handle interpretation errors in load as non-recoverable. This fixes: https://coq.inria.fr/bugs/show_bug.cgi?id=5485 --- toplevel/vernac.ml | 40 ++++++++++++++++++---------------------- 1 file changed, 18 insertions(+), 22 deletions(-) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 3359a16721..19753b6f64 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -115,28 +115,23 @@ let rec interp_vernac sid po (loc,com) = let f = Loadpath.locate_file fname in load_vernac verbosely sid f | v -> - try - let nsid, ntip = Stm.add sid (not !Flags.quiet) (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 that depends on the - vernac. For now we imitate the old approach. *) - let hide_goals = !Flags.batch_mode || is_query v || !Flags.quiet || - not (Proof_global.there_are_pending_proofs ()) in - - if not hide_goals then Feedback.msg_notice (pr_open_cur_subgoals ()); - nsid - - with exn when CErrors.noncritical exn -> - ignore(Stm.edit_at sid); - raise exn + let nsid, ntip = Stm.add sid (not !Flags.quiet) (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 that depends on the + vernac. For now we imitate the old approach. *) + let hide_goals = !Flags.batch_mode || is_query v || !Flags.quiet || + not (Proof_global.there_are_pending_proofs ()) in + + if not hide_goals then Feedback.msg_notice (pr_open_cur_subgoals ()); + nsid in try (* The -time option is only supported from console-based @@ -145,6 +140,7 @@ let rec interp_vernac sid po (loc,com) = let com = if !Flags.time then VernacTime (loc,com) else com in interp com with reraise -> + ignore(Stm.edit_at sid); let (reraise, info) = CErrors.push reraise in let loc' = Option.default Loc.ghost (Loc.get_loc info) in if Loc.is_ghost loc' then iraise (reraise, Loc.add_loc info loc) -- cgit v1.2.3 From 0fd7d060e0872a6ae3662dfb7a1fb940b80ef9df Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 24 Apr 2017 19:10:19 +0200 Subject: [toplevel] Don't check proofs in -quick mode. This fixes a logical error introduced in ce2b2058587224ade9261cd4127ef4f6e94d356b Patch by @gares, closes https://coq.inria.fr/bugs/show_bug.cgi?id=5484 --- toplevel/vernac.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 19753b6f64..f81f77e6ec 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -123,7 +123,9 @@ let rec interp_vernac sid po (loc,com) = (* Due to bug #5363 we cannot use observe here as we should, it otherwise reveals bugs *) (* Stm.observe nsid; *) - Stm.finish (); + + let check_proof = Flags.(!compilation_mode = BuildVo || not !batch_mode) in + if check_proof then Stm.finish (); (* We could use a more refined criteria that depends on the vernac. For now we imitate the old approach. *) -- cgit v1.2.3 From 4abb41d008fc754f21916dcac9cce49f2d04dd6d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 24 Apr 2017 19:25:48 +0200 Subject: [toplevel] Use exception information for error printing. This is a partial backtrack on 63cfc77ddf3586262d905dc351b58669d185a55e. In that commit, we disregarded exception and tried to print error messages just by listening to feedback. However, feedback error messages are not always emitted due to https://coq.inria.fr/bugs/show_bug.cgi?id=5479 Thus meanwhile it is safer to go back to printing the information present in exceptions until we tweak the STM. This fixes https://coq.inria.fr/bugs/show_bug.cgi?id=5467 and many other glitches not reported, such errors in nested proofs. --- toplevel/coqloop.ml | 33 +++++++++++++-------------------- toplevel/coqtop.ml | 25 ++++++++++--------------- toplevel/vernac.ml | 50 +++++++++++++++++++++++++++++++++----------------- vernac/topfmt.ml | 23 +++++++++++++++++++++++ vernac/topfmt.mli | 11 +++++++---- 5 files changed, 86 insertions(+), 56 deletions(-) diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 4641a2bc86..b608488c8c 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -149,20 +149,6 @@ let valid_buffer_loc ib loc = not (Loc.is_ghost loc) && let (b,e) = Loc.unloc loc in b-ib.start >= 0 && e-ib.start < ib.len && b<=e -(* This is specific to the toplevel *) -let pr_loc loc = - if Loc.is_ghost loc then str"" - else - let fname = loc.Loc.fname in - if CString.equal fname "" then - Loc.(str"Toplevel input, characters " ++ int loc.bp ++ - str"-" ++ int loc.ep ++ str":") - else - Loc.(str"File " ++ str "\"" ++ str fname ++ str "\"" ++ - str", line " ++ int loc.line_nb ++ str", characters " ++ - int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++ - str":") - (* Toplevel error explanation. *) let error_info_for_buffer ?loc buf = Option.map (fun loc -> @@ -177,7 +163,7 @@ let error_info_for_buffer ?loc buf = else (mt (), nloc) (* we are in batch mode, don't adjust location *) else (mt (), loc) - in pr_loc loc ++ hl + in Topfmt.pr_loc loc ++ hl ) loc (* Actual printing routine *) @@ -292,6 +278,9 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in | FileDependency (_,_) -> () | FileLoaded (_,_) -> () | Custom (_,_,_) -> () + (* Re-enable when we switch back to feedback-based error printing *) + | Message (Error,loc,msg) -> () + (* TopErr.print_error_for_buffer ?loc lvl msg top_buffer *) | Message (lvl,loc,msg) -> TopErr.print_error_for_buffer ?loc lvl msg top_buffer @@ -318,11 +307,15 @@ let do_vernac sid = | CErrors.Drop -> (* Last chance *) if Mltop.is_ocaml_top() then raise CErrors.Drop 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))); sid + (* Exception printing should be done by the feedback listener, + however this is not yet ready so we rely on the exception for + now. *) + | any -> + let (e, info) = CErrors.push any in + let loc = Loc.get_loc info in + let msg = CErrors.iprint (e, info) in + TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer; + sid (** Main coq loop : read vernacular expressions until Drop is entered. Ctrl-C is handled internally as Sys.Break instead of aborting Coq. diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index f5f43ff66f..9cf0750654 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -430,10 +430,10 @@ let get_native_name s = (** Prints info which is either an error or an anomaly and then exits with the appropriate error code *) -let fatal_error info anomaly = - let msg = info ++ fnl () in - Format.fprintf !Topfmt.err_ft "@[%a@]%!" pp_with msg; - exit (if anomaly then 129 else 1) +let fatal_error ?extra exn = + Topfmt.print_err_exn ?extra exn; + let exit_code = if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1 in + exit exit_code let parse_args arglist = let args = ref arglist in @@ -596,11 +596,7 @@ let parse_args arglist = in try parse () - with - | UserError(_, s) as e -> - if ismt s then exit 1 - else fatal_error (CErrors.print e) false - | any -> fatal_error (CErrors.print any) (CErrors.is_anomaly any) + with any -> fatal_error any let init_toplevel arglist = init_gc (); @@ -646,14 +642,13 @@ let init_toplevel arglist = check_vio_tasks (); outputstate () with any -> - let any = CErrors.push any in flush_all(); - let msg = - if !batch_mode && not Stateid.(equal (Stm.get_current_state ()) dummy) then mt () - else str "Error during initialization: " ++ CErrors.iprint any ++ fnl () + let extra = + if !batch_mode && not Stateid.(equal (Stm.get_current_state ()) dummy) + then None + else Some (str "Error during initialization: ") in - let is_anomaly e = CErrors.is_anomaly e || not (CErrors.handled e) in - fatal_error msg (is_anomaly (fst any)) + fatal_error ?extra any end; if !batch_mode then begin flush_all(); diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index f81f77e6ec..8bcf2114b2 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -107,6 +107,16 @@ let pr_open_cur_subgoals () = try Printer.pr_open_subgoals () with Proof_global.NoCurrentProof -> Pp.str "" +let vernac_error msg = + Format.fprintf !Topfmt.err_ft "@[%a@]%!" Pp.pp_with msg; + flush_all (); + exit 1 + +(* Reenable when we get back to feedback printing *) +(* let is_end_of_input any = match any with *) +(* Stm.End_of_input -> true *) +(* | _ -> false *) + let rec interp_vernac sid po (loc,com) = let interp = function | VernacLoad (verbosely, fname) -> @@ -161,17 +171,25 @@ and load_vernac verbosely sid file = * raised, which means that we raised the end of the file being loaded *) while true do let loc, ast = + Stm.parse_sentence !rsid in_pa + (* If an error in parsing occurs, we propagate the exception + so the caller of load_vernac will take care of it. However, + in the future it could be possible that we want to handle + all the errors as feedback events, thus in this case we + should relay the exception here for convenience. A + possibility is shown below, however we may want to refactor + this code: + try Stm.parse_sentence !rsid in_pa with - | Stm.End_of_input -> raise Stm.End_of_input - | any -> + | any when not is_end_of_input any -> let (e, info) = CErrors.push any in let loc = Loc.get_loc info in let msg = CErrors.iprint (e, info) in Feedback.msg_error ?loc msg; iraise (e, info) + *) in - (* Printing of vernacs *) if !beautify then pr_new_syntax in_pa chan_beautify loc (Some ast); Option.iter (vernac_echo loc) in_echo; @@ -231,13 +249,10 @@ let chop_extension f = let ensure_bname src tgt = let src, tgt = Filename.basename src, Filename.basename tgt in let src, tgt = chop_extension src, chop_extension tgt in - if src <> tgt then begin - Feedback.msg_error (str "Source and target file names must coincide, directories can differ" ++ fnl () ++ - str "Source: " ++ str src ++ fnl () ++ - str "Target: " ++ str tgt); - flush_all (); - exit 1 - end + if src <> tgt then + vernac_error (str "Source and target file names must coincide, directories can differ" ++ fnl () ++ + str "Source: " ++ str src ++ fnl () ++ + str "Target: " ++ str tgt) let ensure ext src tgt = ensure_bname src tgt; ensure_ext ext tgt @@ -246,17 +261,15 @@ let ensure_vo v vo = ensure ".vo" v vo let ensure_vio v vio = ensure ".vio" v vio let ensure_exists f = - if not (Sys.file_exists f) then begin - Feedback.msg_error (hov 0 (str "Can't find file" ++ spc () ++ str f)); - exit 1 - end + if not (Sys.file_exists f) then + vernac_error (hov 0 (str "Can't find file" ++ spc () ++ str f)) (* Compile a vernac file *) let compile verbosely f = let check_pending_proofs () = let pfs = Pfedit.get_all_proof_names () in - if not (List.is_empty pfs) then - (Feedback.msg_error (str "There are pending proofs"); flush_all (); exit 1) in + if not (List.is_empty pfs) then vernac_error (str "There are pending proofs") + in match !Flags.compilation_mode with | BuildVo -> let long_f_dot_v = ensure_v f in @@ -311,5 +324,8 @@ let compile verbosely f = let compile v f = ignore(CoqworkmgrApi.get 1); - compile v f; + begin + try compile v f + with any -> Topfmt.print_err_exn any + end; CoqworkmgrApi.giveback 1 diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index c25dd55fb7..a1835959c2 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -260,6 +260,29 @@ let init_color_output () = *) let emacs_logger = gen_logger Emacs.quote_info Emacs.quote_warning + +(* This is specific to the toplevel *) +let pr_loc loc = + if Loc.is_ghost loc then str"" + else + let fname = loc.Loc.fname in + if CString.equal fname "" then + Loc.(str"Toplevel input, characters " ++ int loc.bp ++ + str"-" ++ int loc.ep ++ str":") + else + Loc.(str"File " ++ str "\"" ++ str fname ++ str "\"" ++ + str", line " ++ int loc.line_nb ++ str", characters " ++ + int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++ + str":") + +let print_err_exn ?extra any = + let (e, info) = CErrors.push any in + let loc = Loc.get_loc info in + let msg_loc = pr_loc (Option.default Loc.ghost loc) in + let pre_hdr = pr_opt_no_spc (fun x -> x) extra ++ msg_loc in + let msg = CErrors.iprint (e, info) ++ fnl () in + std_logger ~pre_hdr Feedback.Error msg + (* Output to file, used only in extraction so a candidate for removal *) let ft_logger old_logger ft ?loc level mesg = let id x = x in diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli index 909dd70775..6c8e0ae2fa 100644 --- a/vernac/topfmt.mli +++ b/vernac/topfmt.mli @@ -36,19 +36,22 @@ val get_depth_boxes : unit -> int option val set_margin : int option -> unit val get_margin : unit -> int option -(** Headers for tagging *) -val err_hdr : Pp.std_ppcmds -val ann_hdr : Pp.std_ppcmds - (** Console display of feedback, we may add some location information *) val std_logger : ?pre_hdr:Pp.std_ppcmds -> Feedback.level -> Pp.std_ppcmds -> unit val emacs_logger : ?pre_hdr:Pp.std_ppcmds -> Feedback.level -> Pp.std_ppcmds -> unit +(** Color output *) val init_color_output : unit -> unit val clear_styles : unit -> unit val parse_color_config : string -> unit val dump_tags : unit -> (string * Terminal.style) list +(** Error printing *) +(* To be deprecated when we can fully move to feedback-based error + printing. *) +val pr_loc : Loc.t -> Pp.std_ppcmds +val print_err_exn : ?extra:Pp.std_ppcmds -> exn -> unit + (** [with_output_to_file file f x] executes [f x] with logging redirected to a file [file] *) val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b -- cgit v1.2.3 From e699313c7a3829016c853b2a1541c2e9151d709c Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 25 Apr 2017 18:36:09 +0200 Subject: [toplevel] Remove unused parameter from `Vernac.process_expr`. --- toplevel/coqloop.ml | 2 +- toplevel/vernac.ml | 8 ++++---- toplevel/vernac.mli | 10 +++++++--- 3 files changed, 12 insertions(+), 8 deletions(-) diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index b608488c8c..9a4f476bd3 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -300,7 +300,7 @@ let do_vernac sid = resynch_buffer top_buffer; try let input = (top_buffer.tokens, None) in - Vernac.process_expr sid top_buffer.tokens (read_sentence sid (fst input)) + Vernac.process_expr sid (read_sentence sid (fst input)) with | Stm.End_of_input | CErrors.Quit -> top_stderr (fnl ()); raise CErrors.Quit diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 8bcf2114b2..9ff320ee80 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -117,7 +117,7 @@ let vernac_error msg = (* Stm.End_of_input -> true *) (* | _ -> false *) -let rec interp_vernac sid po (loc,com) = +let rec interp_vernac sid (loc,com) = let interp = function | VernacLoad (verbosely, fname) -> let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in @@ -195,7 +195,7 @@ and load_vernac verbosely sid file = Option.iter (vernac_echo loc) in_echo; checknav_simple (loc, ast); - let nsid = Flags.silently (interp_vernac !rsid in_pa) (loc, ast) in + let nsid = Flags.silently (interp_vernac !rsid) (loc, ast) in rsid := nsid done; !rsid @@ -221,9 +221,9 @@ and load_vernac verbosely sid file = of a new state label). An example of state-preserving command is one coming from the query panel of Coqide. *) -let process_expr sid po loc_ast = +let process_expr sid loc_ast = checknav_deep loc_ast; - interp_vernac sid po loc_ast + interp_vernac sid loc_ast (* XML output hooks *) let (f_xml_start_library, xml_start_library) = Hook.make ~default:ignore () diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index e75f8f9e85..bbc095c687 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -8,11 +8,15 @@ (** Parsing of vernacular. *) -(** Reads and executes vernac commands from a stream. *) -val process_expr : Stateid.t -> Pcoq.Gram.coq_parsable -> Vernacexpr.vernac_expr Loc.located -> Stateid.t +(** [process_expr sid cmd] Executes vernac command [cmd]. Callers are + expected to handle and print errors in form of exceptions, however + care is taken so the state machine is left in a consistent + state. *) +val process_expr : Stateid.t -> Vernacexpr.vernac_expr Loc.located -> Stateid.t (** [load_vernac echo sid file] Loads [file] on top of [sid], will - echo the commands if [echo] is set. *) + echo the commands if [echo] is set. Callers are expected to handle + and print errors in form of exceptions. *) val load_vernac : bool -> Stateid.t -> string -> Stateid.t (** Compile a vernac file, (f is assumed without .v suffix) *) -- cgit v1.2.3