From 9b54bda96f51cc5387f195614620fae53dec5bd1 Mon Sep 17 00:00:00 2001 From: Cyprien Mangin Date: Wed, 3 May 2017 10:47:53 +0200 Subject: FIx bug #5300: uncaught exception in "Print Assumptions". --- toplevel/assumptions.ml | 21 +++++++++++++++++++-- 1 file changed, 19 insertions(+), 2 deletions(-) (limited to 'toplevel') diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml index 45c539e229..a865ee987f 100644 --- a/toplevel/assumptions.ml +++ b/toplevel/assumptions.ml @@ -42,6 +42,11 @@ let rec search_cst_label lab = function | (l, SFBconst cb) :: _ when Label.equal l lab -> cb | _ :: fields -> search_cst_label lab fields +let rec search_mind_label lab = function + | [] -> raise Not_found + | (l, SFBmind mind) :: _ when Label.equal l lab -> mind + | _ :: fields -> search_mind_label lab fields + (* TODO: using [empty_delta_resolver] below is probably slightly incorrect. But: a) I don't see currently what should be used instead b) this shouldn't be critical for Print Assumption. At worse some @@ -133,6 +138,18 @@ let lookup_constant cst = else lookup_constant_in_impl cst (Some cb) with Not_found -> lookup_constant_in_impl cst None +let lookup_mind_in_impl mind = + try + let mp,dp,lab = repr_kn (canonical_mind mind) in + let fields = memoize_fields_of_mp mp in + search_mind_label lab fields + with Not_found -> + anomaly (str "Print Assumption: unknown inductive " ++ MutInd.print mind) + +let lookup_mind mind = + try Global.lookup_mind mind + with Not_found -> lookup_mind_in_impl mind + (** Graph traversal of an object, collecting on the way the dependencies of traversed objects *) @@ -204,7 +221,7 @@ and traverse_inductive (curr, data, ax2ty) mind obj = where I_0, I_1, ... are in the same mutual definition and c_ij are all their constructors. *) if Refmap_env.mem firstind_ref data then data, ax2ty else - let mib = Global.lookup_mind mind in + let mib = lookup_mind mind in (* Collects references of parameters *) let param_ctx = mib.mind_params_ctxt in let nparam = List.length param_ctx in @@ -308,7 +325,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = else accu | IndRef (m,_) | ConstructRef ((m,_),_) -> - let mind = Global.lookup_mind m in + let mind = lookup_mind m in if mind.mind_typing_flags.check_guarded then accu else -- cgit v1.2.3 From 1fe73e6af81759fa8b78c8660745492ed886d477 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Wed, 26 Apr 2017 11:57:58 +0200 Subject: Adding an option "Printing Unfocused". Off by default. + small refactoring of emacs hacks in printer.ml. --- toplevel/coqtop.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'toplevel') diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index c3a7558609..5687418f2d 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -247,6 +247,7 @@ let set_emacs () = if not (Option.is_empty !toploop) then error "Flag -emacs is incompatible with a custom toplevel loop"; Flags.print_emacs := true; + Printer.enable_goal_tags_printing := true; color := `OFF (** Options for CoqIDE *) -- cgit v1.2.3 From cf0e030f3aebecb316852fc4a152fb212f9e7ef5 Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Fri, 5 May 2017 15:58:52 +0200 Subject: coqtop -help: don't die if coqlib can't be found --- toplevel/coqtop.ml | 10 +++++++++- toplevel/usage.ml | 1 + 2 files changed, 10 insertions(+), 1 deletion(-) (limited to 'toplevel') diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 5687418f2d..8f50bfb3d8 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -292,9 +292,17 @@ let init_gc () = We no longer use [Arg.parse], in order to use share [Usage.print_usage] between coqtop and coqc. *) +let usage_no_coqlib = CWarnings.create ~name:"usage-no-coqlib" ~category:"filesystem" + (fun () -> Pp.str "cannot guess a path for Coq libraries; dynaminally loaded flags will not be mentioned") + +exception NoCoqLib let usage () = - Envars.set_coqlib ~fail:CErrors.error; + begin + try + Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib); init_load_path (); + with NoCoqLib -> usage_no_coqlib () + end; if !batch_mode then Usage.print_usage_coqc () else begin Mltop.load_ml_objects_raw_rex diff --git a/toplevel/usage.ml b/toplevel/usage.ml index e457ca61d0..e290480354 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -30,6 +30,7 @@ let print_usage_channel co command = \n -R dir coqdir recursively map physical dir to logical coqdir\ \n -Q dir coqdir map physical dir to logical coqdir\ \n -top coqdir set the toplevel name to be coqdir instead of Top\ +\n -coqlib dir set the coq standard library directory\ \n -exclude-dir f exclude subdirectories named f for option -R\ \n\ \n -noinit start without loading the Init library\ -- cgit v1.2.3 From 787a2c911b88bff399b37bfa8e11c0f1acecc6cd Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 4 May 2017 08:50:27 +0200 Subject: Fix bug #3659: -time should understand multibyte encodings. We assume Coq always outputs UTF-8 (is it really the case?) and cut strings after 30 UTF-8 characters instead of using the standard String function. --- toplevel/vernac.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'toplevel') diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index bfdae85d50..2a599444c2 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -160,7 +160,9 @@ let pr_new_syntax po loc chan_beautify ocom = and a glimpse of the executed command *) let pp_cmd_header loc com = - let shorten s = try (String.sub s 0 30)^"..." with _ -> s in + let shorten s = + if Unicode.utf8_length s > 33 then (Unicode.utf8_sub s 0 30) ^ "..." else s + in let noblank s = for i = 0 to String.length s - 1 do match s.[i] with -- cgit v1.2.3 From d411a796341a138cacd72350715871f48f82920b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 5 May 2017 21:31:14 +0200 Subject: [toplevel] Fix a couple of logical errors in error printing. In 4abb41d008fc754f21916dcac9cce49f2d04dd6d we switched back to use exceptions for error printing. However a couple of mistakes were present in that commit: - We wrongly absorbed the exception on `Vernac.compile`. However, it should be propagated as the caller will correctly print the error now. This introduced a critical bug as now `coqc` return the wrong exit status on error, breaking all sort of things. - We printed parsing exceptions twice; now it is not necessary to print the exception in the parsing handler as it will be propagated. I've checked this commit versus all previously reported bugs and it seems to work; we should definitively add a test-suite case to check that the exit code of `coqc` is correct, plus several other cases such as bugs https://coq.inria.fr/bugs/show_bug.cgi?id=5467 https://coq.inria.fr/bugs/show_bug.cgi?id=5485 https://coq.inria.fr/bugs/show_bug.cgi?id=5484 etc... See also PR #583 --- toplevel/coqloop.ml | 8 ++++++-- toplevel/vernac.ml | 5 +---- 2 files changed, 7 insertions(+), 6 deletions(-) (limited to 'toplevel') diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 9a4f476bd3..a80599cd57 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -173,12 +173,13 @@ let print_error_for_buffer ?loc lvl msg buf = then Topfmt.emacs_logger ?pre_hdr lvl msg else Topfmt.std_logger ?pre_hdr lvl msg +(* let print_toplevel_parse_error (e, info) buf = let loc = Loc.get_loc info in let lvl = Feedback.Error in let msg = CErrors.iprint (e, info) in print_error_for_buffer ?loc lvl msg buf - +*) end (*s The Coq prompt is the name of the focused proof, if any, and "Coq" @@ -260,7 +261,10 @@ let read_sentence sid input = with reraise -> let reraise = CErrors.push reraise in discard_to_dot (); - TopErr.print_toplevel_parse_error reraise top_buffer; + (* The caller of read_sentence does the error printing now, this + should be re-enabled once we rely on the feedback error + printer again *) + (* TopErr.print_toplevel_parse_error reraise top_buffer; *) Exninfo.iraise reraise (** Coqloop Console feedback handler *) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 9f6f77ef1d..4fca4ea184 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -323,8 +323,5 @@ let compile verbosely f = let compile v f = ignore(CoqworkmgrApi.get 1); - begin - try compile v f - with any -> Topfmt.print_err_exn any - end; + compile v f; CoqworkmgrApi.giveback 1 -- cgit v1.2.3 From 684dd06c538ea6024e5dd01bfc6eb416b08ddc14 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 14 May 2017 00:26:16 +0200 Subject: Removing a variable warned unused. --- toplevel/metasyntax.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'toplevel') diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 349c05a38d..0787b058ae 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -520,7 +520,7 @@ let warn_skip_spaces_curly = (fun () ->strbrk "Skipping spaces inside curly brackets") let rec drop_spacing = function - | UnpCut _ as u :: fmt -> warn_skip_spaces_curly (); drop_spacing fmt + | UnpCut _ :: fmt -> warn_skip_spaces_curly (); drop_spacing fmt | UnpTerminal s' :: fmt when String.equal s' (String.make (String.length s') ' ') -> warn_skip_spaces_curly (); drop_spacing fmt | fmt -> fmt -- cgit v1.2.3