From 5436ca063dd8a1ae22f2b70bd8f69277c64a0624 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 23 Sep 2017 15:34:32 +0200 Subject: After testing it in live, writing metas using an ?INTERNAL#42 style is ugly. Printing metas still happens relatively often. From the user point of view, no need to know that it is different from an evar, so the notation ?M42 as it was before is much lighter. As for developers looking for debugging information, they will easily suspect that it is internally a meta because of the "M". This reverts "Proposing meta names more distinguishable from evar names than ?M42." (dc5b8f1793c6f7104f0b4762d9887be255709ead). --- pretyping/detyping.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 5e14307418..f61638db81 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -464,7 +464,7 @@ and detype_r d flags avoid env sigma t = (* Using a dash to be unparsable *) GEvar (Id.of_string_soft "CONTEXT-HOLE", []) else - GEvar (Id.of_string_soft ("INTERNAL#" ^ string_of_int n), []) + GEvar (Id.of_string_soft ("M" ^ string_of_int n), []) | Var id -> (try let _ = Global.lookup_named id in GRef (VarRef id, None) with Not_found -> GVar id) -- cgit v1.2.3 From b789106117653fec8340ecbd88866c254fe1201d Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 25 Sep 2017 18:01:38 +0200 Subject: Fixing a little parsing bug with level 90 introduced in 3e70ea9c. Unfortunately, some manual synchronization is needed between the constr parser and the table of constr/pattern levels. We do this synchronization which was missing in the commit moving "x -> y" to a user-level notation. --- parsing/egramcoq.ml | 2 ++ parsing/g_constr.ml4 | 1 + 2 files changed, 3 insertions(+) diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 870137ca11..d51b8b54e5 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -34,6 +34,7 @@ let default_levels = [200,Extend.RightA,false; 100,Extend.RightA,false; 99,Extend.RightA,true; + 90,Extend.RightA,true; 10,Extend.RightA,false; 9,Extend.RightA,false; 8,Extend.RightA,true; @@ -44,6 +45,7 @@ let default_pattern_levels = [200,Extend.RightA,true; 100,Extend.RightA,false; 99,Extend.RightA,true; + 90,Extend.RightA,true; 11,Extend.LeftA,false; 10,Extend.RightA,false; 1,Extend.LeftA,false; diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 7d0728458b..ad8c1c3987 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -376,6 +376,7 @@ GEXTEND Gram | "100" RIGHTA [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> CAst.make ~loc:!@loc @@ CPatOr (p::pl) ] | "99" RIGHTA [ ] + | "90" RIGHTA [ ] | "11" LEFTA [ p = pattern; "as"; id = ident -> CAst.make ~loc:!@loc @@ CPatAlias (p, id) ] -- cgit v1.2.3 From c0b244260badedf27fe2b66d3c058ad681af4371 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 26 Sep 2017 14:34:51 +0200 Subject: Properly display the "only" prefix for selectors (bug #5760). This commit also fixes range selectors being incorrectly displayed. --- plugins/ltac/g_ltac.ml4 | 11 +---------- plugins/ltac/pptactic.ml | 16 +++++++++------- plugins/ltac/pptactic.mli | 2 ++ 3 files changed, 12 insertions(+), 17 deletions(-) diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 2ea0f60ebc..86c983bdd9 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -388,16 +388,7 @@ let vernac_solve n info tcom b = p,status) in if not status then Feedback.feedback Feedback.AddedAxiom -let pr_range_selector (i, j) = - if Int.equal i j then int i - else int i ++ str "-" ++ int j - -let pr_ltac_selector = function -| SelectNth i -> int i ++ str ":" -| SelectList l -> str "[" ++ prlist_with_sep (fun () -> str ", ") pr_range_selector l ++ - str "]" ++ str ":" -| SelectId id -> str "[" ++ Id.print id ++ str "]" ++ str ":" -| SelectAll -> str "all" ++ str ":" +let pr_ltac_selector s = Pptactic.pr_goal_selector ~toplevel:true s VERNAC ARGUMENT EXTEND ltac_selector PRINTED BY pr_ltac_selector | [ toplevel_selector(s) ] -> [ s ] diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index f4e3ba633f..7fe17ceb7b 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -477,12 +477,14 @@ type 'a extra_genarg_printer = if Int.equal i j then int i else int i ++ str "-" ++ int j - let pr_goal_selector = function - | SelectNth i -> int i ++ str ":" - | SelectList l -> str "[" ++ prlist_with_sep (fun () -> str ", ") pr_range_selector l ++ - str "]" ++ str ":" - | SelectId id -> str "[" ++ Id.print id ++ str "]" ++ str ":" - | SelectAll -> str "all" ++ str ":" +let pr_goal_selector toplevel = function + | SelectNth i -> int i ++ str ":" + | SelectList l -> prlist_with_sep (fun () -> str ", ") pr_range_selector l ++ str ":" + | SelectId id -> str "[" ++ Id.print id ++ str "]:" + | SelectAll -> assert toplevel; str "all:" + +let pr_goal_selector ~toplevel s = + (if toplevel then mt () else str "only ") ++ pr_goal_selector toplevel s let pr_lazy = function | General -> keyword "multi" @@ -988,7 +990,7 @@ type 'a extra_genarg_printer = keyword "solve" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet | TacComplete t -> pr_tac (lcomplete,E) t, lcomplete - | TacSelect (s, tac) -> pr_goal_selector s ++ spc () ++ pr_tac ltop tac, latom + | TacSelect (s, tac) -> pr_goal_selector ~toplevel:false s ++ spc () ++ pr_tac ltop tac, latom | TacId l -> keyword "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom | TacAtom (loc,t) -> diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 1f6ebaf448..c79d5b389f 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -53,6 +53,8 @@ type pp_tactic = { pptac_prods : grammar_terminals; } +val pr_goal_selector : toplevel:bool -> goal_selector -> Pp.t + val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit val pr_with_occurrences : -- cgit v1.2.3 From d6188188c444a95e3d40c3926274b7e526e96b82 Mon Sep 17 00:00:00 2001 From: Paul Steckler Date: Tue, 26 Sep 2017 15:23:37 -0400 Subject: look for Obligation num or Next Obligation to start proof --- tools/coqwc.mll | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/coqwc.mll b/tools/coqwc.mll index a0b6bfbbed..6ddeeb9b28 100644 --- a/tools/coqwc.mll +++ b/tools/coqwc.mll @@ -94,7 +94,7 @@ let rcs = "\036" rcs_keyword [^ '$']* "\036" let stars = "(*" '*'* "*)" let dot = '.' (' ' | '\t' | '\n' | '\r' | eof) let proof_start = - "Theorem" | "Lemma" | "Fact" | "Remark" | "Goal" | "Correctness" | "Obligation" | "Next" + "Theorem" | "Lemma" | "Fact" | "Remark" | "Goal" | "Correctness" | "Obligation" space+ (['0' - '9'])+ | "Next" space+ "Obligation" let def_start = "Definition" | "Fixpoint" | "Instance" let proof_end = -- cgit v1.2.3 From 77d95ecd65a6bbebfcd89193fb3e2c43ebc6469a Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 27 Sep 2017 00:38:25 +0200 Subject: Avoid looping when searching for CoqProject. This could happen with paths on Windows, or even relative paths on all OSs. Fixes #5730: CoqIDE becomes unresponsive on file open. --- lib/coqProject_file.ml4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4 index 13de731f54..970666638c 100644 --- a/lib/coqProject_file.ml4 +++ b/lib/coqProject_file.ml4 @@ -206,7 +206,7 @@ let rec find_project_file ~from ~projfile_name = if Sys.file_exists fname then Some fname else let newdir = Filename.dirname from in - if newdir = "" || newdir = "/" then None + if newdir = from then None else find_project_file ~from:newdir ~projfile_name ;; -- cgit v1.2.3 From 1db34c8565729a6a2967f4e9444278a7be275b57 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 27 Sep 2017 16:05:03 +0200 Subject: Browser userscript to turn BZ#XXXX occurences into links. --- dev/Coq_Bugzilla_autolink.user.js | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) create mode 100644 dev/Coq_Bugzilla_autolink.user.js diff --git a/dev/Coq_Bugzilla_autolink.user.js b/dev/Coq_Bugzilla_autolink.user.js new file mode 100644 index 0000000000..371c5adc00 --- /dev/null +++ b/dev/Coq_Bugzilla_autolink.user.js @@ -0,0 +1,34 @@ +// ==UserScript== +// @name Coq Bugzilla autolink +// @namespace SkySkimmer +// @include https://github.com/coq/coq/* +// @description Makes BZ#XXXX into links to bugzilla for GitHub +// @version 1 +// @grant none +// ==/UserScript== + +var regex = /BZ#(\d+)/g; +var substr = '$&'; + +function doNode(node) +{ + node.innerHTML = node.innerHTML.replace(regex,substr); +} + +var comments = document.getElementsByClassName("comment-body"); + +for(var i=0; i true | ast -> may_pierce_opaque ast in let parent = function Some (p, _) -> p | None -> assert false in - let is_empty = function `Async(_,_,[],_,_) | `MaybeASync(_,_,[],_,_) -> true | _ -> false in + let is_empty = function `Async(_,[],_,_) | `MaybeASync(_,[],_,_) -> true | _ -> false in let rec collect last accn id = let view = VCS.visit id in match view.step with | (`Sideff (ReplayCommand x,_) | `Cmd { cast = x }) - when too_complex_to_delegate x -> `Sync(no_name,None,`Print) + when too_complex_to_delegate x -> `Sync(no_name,`Print) | `Cmd { cast = x } -> collect (Some (id,x)) (id::accn) view.next | `Sideff (ReplayCommand x,_) -> collect (Some (id,x)) (id::accn) view.next (* An Alias could jump everywhere... we hope we can ignore it*) - | `Alias _ -> `Sync (no_name,None,`Alias) + | `Alias _ -> `Sync (no_name,`Alias) | `Fork((_,_,_,_::_::_), _) -> - `Sync (no_name,proof_using_ast last,`MutualProofs) + `Sync (no_name,`MutualProofs) | `Fork((_,_,Doesn'tGuaranteeOpacity,_), _) -> - `Sync (no_name,proof_using_ast last,`Doesn'tGuaranteeOpacity) + `Sync (no_name,`Doesn'tGuaranteeOpacity) | `Fork((_,hd',GuaranteesOpacity,ids), _) when has_proof_using last -> assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch); let name = name ids in - `ASync (parent last,proof_using_ast last,accn,name,delegate name) + `ASync (parent last,accn,name,delegate name) | `Fork((_, hd', GuaranteesOpacity, ids), _) when has_proof_no_using last && not (State.is_cached_and_valid (parent last)) && !Flags.compilation_mode = Flags.BuildVio -> @@ -2027,31 +2027,32 @@ let collect_proof keep cur hd brkind id = let name, hint = name ids, get_hint_ctx loc in let t, v = proof_no_using last in v.expr <- VernacProof(t, Some hint); - `ASync (parent last,proof_using_ast last,accn,name,delegate name) + `ASync (parent last,accn,name,delegate name) with Not_found -> let name = name ids in - `MaybeASync (parent last, None, accn, name, delegate name)) + `MaybeASync (parent last, accn, name, delegate name)) | `Fork((_, hd', GuaranteesOpacity, ids), _) -> assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch); let name = name ids in - `MaybeASync (parent last, None, accn, name, delegate name) + `MaybeASync (parent last, accn, name, delegate name) | `Sideff _ -> warn_deprecated_nested_proofs (); - `Sync (no_name,None,`NestedProof) - | _ -> `Sync (no_name,None,`Unknown) in + `Sync (no_name,`NestedProof) + | _ -> `Sync (no_name,`Unknown) in let make_sync why = function - | `Sync(name,pua,_) -> `Sync (name,pua,why) - | `MaybeASync(_,pua,_,name,_) -> `Sync (name,pua,why) - | `ASync(_,pua,_,name,_) -> `Sync (name,pua,why) in + | `Sync(name,_) -> `Sync (name,why) + | `MaybeASync(_,_,name,_) -> `Sync (name,why) + | `ASync(_,_,name,_) -> `Sync (name,why) in + let check_policy rc = if async_policy () then rc else make_sync `Policy rc in match cur, (VCS.visit id).step, brkind with | (parent, { expr = VernacExactProof _ }), `Fork _, _ | (parent, { expr = VernacTime (_, VernacExactProof _) }), `Fork _, _ -> - `Sync (no_name,None,`Immediate) + `Sync (no_name,`Immediate) | _, _, { VCS.kind = `Edit _ } -> check_policy (collect (Some cur) [] id) | _ -> - if is_defined cur then `Sync (no_name,None,`Transparent) - else if keep == VtDrop then `Sync (no_name,None,`Aborted) + if is_defined cur then `Sync (no_name,`Transparent) + else if keep == VtDrop then `Sync (no_name,`Aborted) else let rc = collect (Some cur) [] id in if is_empty rc then make_sync `AlreadyEvaluated rc @@ -2223,7 +2224,7 @@ let known_state ?(redefine_qed=false) ~cache id = ), `Yes, true | `Qed ({ qast = x; keep; brinfo; brname } as qed, eop) -> let rec aux = function - | `ASync (block_start, pua, nodes, name, delegate) -> (fun () -> + | `ASync (block_start, nodes, name, delegate) -> (fun () -> assert(keep == VtKeep || keep == VtKeepAsAxiom); let drop_pt = keep == VtKeepAsAxiom in let block_stop, exn_info, loc = eop, (id, eop), x.loc in @@ -2270,10 +2271,10 @@ let known_state ?(redefine_qed=false) ~cache id = end; Proof_global.discard_all () ), (if redefine_qed then `No else `Yes), true - | `Sync (name, _, `Immediate) -> (fun () -> + | `Sync (name, `Immediate) -> (fun () -> reach eop; stm_vernac_interp id x; Proof_global.discard_all () ), `Yes, true - | `Sync (name, pua, reason) -> (fun () -> + | `Sync (name, reason) -> (fun () -> log_processing_sync id name reason; reach eop; let wall_clock = Unix.gettimeofday () in @@ -2298,12 +2299,12 @@ let known_state ?(redefine_qed=false) ~cache id = (Printf.sprintf "%.3f" (wall_clock3 -. wall_clock2)); Proof_global.discard_all () ), `Yes, true - | `MaybeASync (start, pua, nodes, name, delegate) -> (fun () -> + | `MaybeASync (start, nodes, name, delegate) -> (fun () -> reach ~cache:`Shallow start; (* no sections *) 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))) () + then Util.pi1 (aux (`ASync (start, nodes, name, delegate))) () + else Util.pi1 (aux (`Sync (name, `NoPU_NoHint_NoES))) () ), (if redefine_qed then `No else `Yes), true in aux (collect_proof keep (view.next, x) brname brinfo eop) -- cgit v1.2.3 From d14215865ec702897fd22a8d9272fede00cda11f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 24 Sep 2017 15:58:52 +0200 Subject: [ide] Avoid duplicate error printing (BZ#5583) See the discussion in the bug tracker, basically the STM delays the feedback error message to a point where CoqIDE has forgotten about the sentence, thus we were processing such errors in the generic case, printing them twice as the Fail case will also do it. We could indeed revert back to the 8.6 strategy for error (print always from Fail and ignore Feedback), however I feel that time will be better spent by fixing the STM than adding more CoqIDE workarounds. --- ide/coqOps.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 9be70e6d38..0dd08293c8 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -480,8 +480,11 @@ object(self) | Message(lvl, loc, msg), Some (id,sentence) -> log_pp ?id Pp.(str "Msg " ++ msg); messages#push lvl msg + (* We do nothing here as for BZ#5583 *) + | Message(Error, loc, msg), None -> + log_pp Pp.(str "Error Msg without a sentence" ++ msg) | Message(lvl, loc, msg), None -> - log_pp Pp.(str "Msg " ++ msg); + log_pp Pp.(str "Msg without a sentence " ++ msg); messages#push lvl msg | InProgress n, _ -> if n < 0 then processed <- processed + abs n @@ -655,7 +658,7 @@ object(self) with Doc.Empty -> initial_state | Invalid_argument _ -> assert false in loop tip [] in Coq.bind fill_queue process_queue - + method join_document = let next = function | Good _ -> -- cgit v1.2.3 From 8bf34547d21d417140b726fab5fdbf8625c5be95 Mon Sep 17 00:00:00 2001 From: Tej Chajed Date: Wed, 6 Sep 2017 09:13:42 -0400 Subject: Mention requiring extraction/funind in CHANGES --- CHANGES | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/CHANGES b/CHANGES index ca5172d7b7..fdf0c9d6be 100644 --- a/CHANGES +++ b/CHANGES @@ -133,6 +133,13 @@ Plugins - The mathematical proof language (also known as declarative mode) was removed. - A new command Extraction TestCompile has been introduced, not meant for the general user but instead for Coq's test-suite. +- The extraction plugin is no longer loaded by default. It must be + explicitly loaded with [Require Extraction], which is backwards + compatible. +- The functional induction plugin (which provides the [Function] + vernacular) is no longer loaded by default. It must be explicitly + loaded with [Require FunInd], which is backwards compatible. + Dependencies -- cgit v1.2.3