From 17ec7a0c875014e5322f6098dcd2014072cde9d8 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 18 Oct 2016 14:23:23 +0200 Subject: Improve the documentation of eauto. Improve the description of what auto/eauto do. These two tactics rely on the simple version of apply/eapply. Since this simple version is available to the end user, it is better to mention it. See also the confusion that such description can create in the thread "Understanding auto" on Coq-Club. --- doc/refman/RefMan-tac.tex | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 5eb8cedd9..fc6d9c143 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3513,8 +3513,8 @@ intact. \texttt{auto} and \texttt{trivial} never fail. This tactic generalizes {\tt auto}. While {\tt auto} does not try resolution hints which would leave existential variables in the goal, -{\tt eauto} does try them (informally speaking, it uses {\tt eapply} -where {\tt auto} uses {\tt apply}). +{\tt eauto} does try them (informally speaking, it uses +{\tt simple eapply} where {\tt auto} uses {\tt simple apply}). As a consequence, {\tt eauto} can solve such a goal: \begin{coq_eval} @@ -3529,8 +3529,7 @@ eauto. Abort. \end{coq_eval} -Note that {\tt ex\_intro} should be declared as an -hint. +Note that {\tt ex\_intro} should be declared as a hint. \SeeAlso Section~\ref{Hints-databases} -- cgit v1.2.3 From 60354f102ab60c1df24ebb269b51e6664eb70aa3 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 18 Oct 2016 15:52:11 +0200 Subject: [stm] Fix record field name clash. PR#173 introduced a record field name clash in `stm.mli`, with duplicate fields `start/stop` for the types `focus` and `static_block_declaration`. We fix by renaming the younger ones (as to minimize code incompatibilities), but other options are possible/could be preferred, however they would be quite more invasive so I think they should be postponed for the day the Stm API is cleaned up. --- stm/proofBlockDelimiter.ml | 8 ++--- stm/stm.ml | 82 +++++++++++++++++++++++----------------------- stm/stm.mli | 4 +-- 3 files changed, 47 insertions(+), 47 deletions(-) diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index ce12185cb..8162fc3bb 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -83,7 +83,7 @@ let static_bullet ({ entry_point; prev_node } as view) = if node.indentation > base then `Cont node else match node.ast with | Vernacexpr.VernacBullet b' when b = b' -> - `Found { stop = entry_point.id; start = prev.id; + `Found { block_stop = entry_point.id; block_start = prev.id; dynamic_switch = node.id; carry_on_data = of_bullet_val b } | _ -> `Stop) entry_point | _ -> assert false @@ -108,7 +108,7 @@ let static_curly_brace ({ entry_point; prev_node } as view) = crawl view (fun (nesting,prev) node -> match node.ast with | Vernacexpr.VernacSubproof _ when nesting = 0 -> - `Found { stop = entry_point.id; start = prev.id; + `Found { block_stop = entry_point.id; block_start = prev.id; dynamic_switch = node.id; carry_on_data = unit_val } | Vernacexpr.VernacSubproof _ -> `Cont (nesting - 1,node) @@ -135,7 +135,7 @@ let static_par { entry_point; prev_node } = match prev_node entry_point with | None -> None | Some { id = pid } -> - Some { stop = entry_point.id; start = pid; + Some { block_stop = entry_point.id; block_start = pid; dynamic_switch = pid; carry_on_data = unit_val } let dynamic_par { dynamic_switch = id } = @@ -162,7 +162,7 @@ let static_indent ({ entry_point; prev_node } as view) = crawl view ~init:(Some last_tac) (fun prev node -> if node.indentation >= last_tac.indentation then `Cont node else - `Found { stop = entry_point.id; start = node.id; + `Found { block_stop = entry_point.id; block_start = node.id; dynamic_switch = node.id; carry_on_data = of_vernac_expr_val entry_point.ast } ) last_tac diff --git a/stm/stm.ml b/stm/stm.ml index bb4f5f72f..32185247f 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -256,8 +256,8 @@ and pt = { (* TODO: inline records in OCaml 4.03 *) qed : Stateid.t; } and static_block_declaration = { - start : Stateid.t; - stop : Stateid.t; + block_start : Stateid.t; + block_stop : Stateid.t; dynamic_switch : Stateid.t; carry_on_data : DynBlockData.t; } @@ -362,10 +362,10 @@ module VCS : sig val get_state : id -> cached_state (* cuts from start -> stop, raising Expired if some nodes are not there *) - val slice : start:id -> stop:id -> vcs - val nodes_in_slice : start:id -> stop:id -> Stateid.t list + val slice : block_start:id -> block_stop:id -> vcs + val nodes_in_slice : block_start:id -> block_stop:id -> Stateid.t list - val create_proof_task_box : id list -> qed:id -> start:id -> unit + val create_proof_task_box : id list -> qed:id -> block_start:id -> unit val create_proof_block : static_block_declaration -> string -> unit val box_of : id -> box list val delete_boxes_of : id -> unit @@ -582,20 +582,20 @@ end = struct (* {{{ *) let visit id = Vcs_aux.visit !vcs id - let nodes_in_slice ~start ~stop = + let nodes_in_slice ~block_start ~block_stop = let rec aux id = - if Stateid.equal id start then [] else + if Stateid.equal id block_start then [] else match visit id with | { next = n; step = `Cmd x } -> (id,Cmd x) :: aux n | { next = n; step = `Alias x } -> (id,Alias x) :: aux n | { next = n; step = `Sideff (`Ast (x,_)) } -> (id,Sideff (Some x)) :: aux n - | _ -> anomaly(str("Cannot slice from "^ Stateid.to_string start ^ - " to "^Stateid.to_string stop)) - in aux stop + | _ -> anomaly(str("Cannot slice from "^ Stateid.to_string block_start ^ + " to "^Stateid.to_string block_stop)) + in aux block_stop - let slice ~start ~stop = - let l = nodes_in_slice ~start ~stop in + let slice ~block_start ~block_stop = + let l = nodes_in_slice ~block_start ~block_stop in let copy_info v id = Vcs_.set_info v id { (get_info id) with state = Empty; vcs_backup = None,None } in @@ -611,27 +611,27 @@ end = struct (* {{{ *) (Stateid.Set.elements (Vcs_.Dag.Property.having_it p)) (Vcs_.Dag.Property.data p)) v props in - let v = Vcs_.empty start in - let v = copy_info v start in + let v = Vcs_.empty block_start in + let v = copy_info v block_start in let v = List.fold_right (fun (id,tr) v -> let v = Vcs_.commit v id tr in let v = copy_info v id in v) l v in (* Stm should have reached the beginning of proof *) - assert (match (get_info start).state with Valid _ -> true | _ -> false); + assert (match (get_info block_start).state with Valid _ -> true | _ -> false); (* We put in the new dag the most recent state known to master *) let rec fill id = match (get_info id).state with | Empty | Error _ -> fill (Vcs_aux.visit v id).next | Valid _ -> copy_info_w_state v id in - let v = fill stop in + let v = fill block_stop in (* We put in the new dag the first state (since Qed shall run on it, * see check_task_aux) *) - let v = copy_info_w_state v start in + let v = copy_info_w_state v block_start in copy_proof_blockes v - let nodes_in_slice ~start ~stop = - List.rev (List.map fst (nodes_in_slice ~start ~stop)) + let nodes_in_slice ~block_start ~block_stop = + List.rev (List.map fst (nodes_in_slice ~block_start ~block_stop)) let topo_invariant l = let all = List.fold_right Stateid.Set.add l Stateid.Set.empty in @@ -642,11 +642,11 @@ end = struct (* {{{ *) List.for_all (fun s -> Stateid.Set.(subset s all || subset all s)) sets) l - let create_proof_task_box l ~qed ~start:lemma = + let create_proof_task_box l ~qed ~block_start:lemma = if not (topo_invariant l) then anomaly (str "overlapping boxes"); vcs := create_property !vcs l (ProofTask { qed; lemma }) - let create_proof_block ({ start; stop} as decl) name = - let l = nodes_in_slice ~start ~stop in + let create_proof_block ({ block_start; block_stop} as decl) name = + let l = nodes_in_slice ~block_start ~block_stop in if not (topo_invariant l) then anomaly (str "overlapping boxes"); vcs := create_property !vcs l (ProofBlock (decl, name)) let box_of id = List.map Dag.Property.data (property_of !vcs id) @@ -1139,7 +1139,7 @@ let detect_proof_block id name = let static, _ = List.assoc name !proof_block_delimiters in begin match static { prev_node; entry_point } with | None -> () - | Some ({ start; stop } as decl) -> + | Some ({ block_start; block_stop } as decl) -> VCS.create_proof_block decl name end with Not_found -> @@ -1251,7 +1251,7 @@ end = struct (* {{{ *) try Some (ReqBuildProof ({ Stateid.exn_info = t_exn_info; stop = t_stop; - document = VCS.slice ~start:t_start ~stop:t_stop; + document = VCS.slice ~block_start:t_start ~block_stop:t_stop; loc = t_loc; uuid = t_uuid; name = t_name }, t_drop, t_states)) @@ -1401,7 +1401,7 @@ and Slaves : sig (* (eventually) remote calls *) val build_proof : loc:Loc.t -> drop_pt:bool -> - exn_info:(Stateid.t * Stateid.t) -> start:Stateid.t -> stop:Stateid.t -> + exn_info:(Stateid.t * Stateid.t) -> block_start:Stateid.t -> block_stop:Stateid.t -> name:string -> future_proof * cancel_switch (* blocking function that waits for the task queue to be empty *) @@ -1560,7 +1560,7 @@ end = struct (* {{{ *) BuildProof { t_states = s2 } -> overlap_rel s1 s2 | _ -> 0) - let build_proof ~loc ~drop_pt ~exn_info ~start ~stop ~name:pname = + let build_proof ~loc ~drop_pt ~exn_info ~block_start ~block_stop ~name:pname = let id, valid as t_exn_info = exn_info in let cancel_switch = ref false in if TaskQueue.n_workers (Option.get !queue) = 0 then @@ -1569,21 +1569,21 @@ end = struct (* {{{ *) Future.create_delegate ~blocking:true ~name:pname (State.exn_on id ~valid) in let t_uuid = Future.uuid f in let task = ProofTask.(BuildProof { - t_exn_info; t_start = start; t_stop = stop; t_drop = drop_pt; + t_exn_info; t_start = block_start; t_stop = block_stop; t_drop = drop_pt; t_assign = assign; t_loc = loc; t_uuid; t_name = pname; - t_states = VCS.nodes_in_slice ~start ~stop }) in + t_states = VCS.nodes_in_slice ~block_start ~block_stop }) in TaskQueue.enqueue_task (Option.get !queue) (task,cancel_switch); f, cancel_switch end else - ProofTask.build_proof_here ~drop_pt t_exn_info loc stop, cancel_switch + ProofTask.build_proof_here ~drop_pt t_exn_info loc block_stop, cancel_switch else let f, t_assign = Future.create_delegate ~name:pname (State.exn_on id ~valid) in let t_uuid = Future.uuid f in feedback (InProgress 1); let task = ProofTask.(BuildProof { - t_exn_info; t_start = start; t_stop = stop; t_assign; t_drop = drop_pt; + t_exn_info; t_start = block_start; t_stop = block_stop; t_assign; t_drop = drop_pt; t_loc = loc; t_uuid; t_name = pname; - t_states = VCS.nodes_in_slice ~start ~stop }) in + t_states = VCS.nodes_in_slice ~block_start ~block_stop }) in TaskQueue.enqueue_task (Option.get !queue) (task,cancel_switch); f, cancel_switch @@ -1665,7 +1665,7 @@ end = struct (* {{{ *) r_state_fb = t_state_fb; r_document = if age <> `Fresh then None - else Some (VCS.slice ~start:t_state ~stop:t_state); + else Some (VCS.slice ~block_start:t_state ~block_stop:t_state); r_ast = t_ast; r_goal = t_goal; r_name = t_name } @@ -1823,7 +1823,7 @@ end = struct (* {{{ *) try Some { r_where = t_where; r_for = t_for; - r_doc = VCS.slice ~start:t_where ~stop:t_where; + r_doc = VCS.slice ~block_start:t_where ~block_stop:t_where; r_what = t_what } with VCS.Expired -> None @@ -2026,7 +2026,7 @@ let known_state ?(redefine_qed=false) ~cache id = let boxes = VCS.box_of id in let valid_boxes = CList.map_filter (function - | ProofBlock ({ stop } as decl, name) when Stateid.equal stop id -> + | ProofBlock ({ block_stop } as decl, name) when Stateid.equal block_stop id -> Some (decl, name) | _ -> None) boxes in assert(List.length valid_boxes < 2); @@ -2156,12 +2156,12 @@ let known_state ?(redefine_qed=false) ~cache id = ), `Yes, true | `Qed ({ qast = x; keep; brinfo; brname } as qed, eop) -> let rec aux = function - | `ASync (start, pua, nodes, name, delegate) -> (fun () -> + | `ASync (block_start, pua, nodes, name, delegate) -> (fun () -> assert(keep == VtKeep || keep == VtKeepAsAxiom); let drop_pt = keep == VtKeepAsAxiom in - let stop, exn_info, loc = eop, (id, eop), x.loc in + let block_stop, exn_info, loc = eop, (id, eop), x.loc in log_processing_async id name; - VCS.create_proof_task_box nodes ~qed:id ~start; + VCS.create_proof_task_box nodes ~qed:id ~block_start; begin match brinfo, qed.fproof with | { VCS.kind = `Edit _ }, None -> assert false | { VCS.kind = `Edit (_,_,_, okeep, _) }, Some (ofp, cancel) -> @@ -2175,7 +2175,7 @@ let known_state ?(redefine_qed=false) ~cache id = ^"the proof's statement to avoid that.")); let fp, cancel = Slaves.build_proof - ~loc ~drop_pt ~exn_info ~start ~stop ~name in + ~loc ~drop_pt ~exn_info ~block_start ~block_stop ~name in Future.replace ofp fp; qed.fproof <- Some (fp, cancel); (* We don't generate a new state, but we still need @@ -2183,14 +2183,14 @@ let known_state ?(redefine_qed=false) ~cache id = State.install_cached id | { VCS.kind = `Proof _ }, Some _ -> assert false | { VCS.kind = `Proof _ }, None -> - reach ~cache:`Shallow start; + reach ~cache:`Shallow block_start; let fp, cancel = if delegate then Slaves.build_proof - ~loc ~drop_pt ~exn_info ~start ~stop ~name + ~loc ~drop_pt ~exn_info ~block_start ~block_stop ~name else ProofTask.build_proof_here - ~drop_pt exn_info loc stop, ref false + ~drop_pt exn_info loc block_stop, ref false in qed.fproof <- Some (fp, cancel); let proof = diff --git a/stm/stm.mli b/stm/stm.mli index 37ec1f0a1..b8a2a3859 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -139,8 +139,8 @@ module QueryTask : AsyncTaskQueue.Task module DynBlockData : Dyn.S type static_block_declaration = { - start : Stateid.t; - stop : Stateid.t; + block_start : Stateid.t; + block_stop : Stateid.t; dynamic_switch : Stateid.t; carry_on_data : DynBlockData.t; } -- cgit v1.2.3 From 6791a37b4e4ba9be829959b419e37a96e2eb5b84 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 18 Oct 2016 16:51:21 +0200 Subject: Document info_auto. Now that this tactic has been fixed (commit 58d1381), it needed to get documented. --- doc/refman/RefMan-tac.tex | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index fc6d9c143..dccd6f590 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3490,6 +3490,12 @@ hints of the database named {\tt core}. This combines the effects of the {\tt using} and {\tt with} options. +\item {\tt info\_auto} + + Behaves like {\tt auto} but shows the tactics it uses to solve the goal. + This variant is very useful for getting a better understanding of automation, + or to know what lemmas/assumptions were used. + \item {\tt trivial}\tacindex{trivial} This tactic is a restriction of {\tt auto} that is not recursive and -- cgit v1.2.3 From 8d77523f8883fae56a8a338060bb2a52b0fd566c Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 18 Oct 2016 16:56:58 +0200 Subject: Extending the doc with a general summary of auto variants. This way of giving the summary avoids redundancy as much as possible. It is helpful for the auto-completion of Company-Coq of @cpitclaudel. --- doc/refman/RefMan-tac.tex | 30 +++++++++++++++++++++++++----- 1 file changed, 25 insertions(+), 5 deletions(-) diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index dccd6f590..49a5b7983 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3472,7 +3472,7 @@ hints of the database named {\tt core}. Uses the hint databases $\ident_1$ \dots\ $\ident_n$ in addition to the database {\tt core}. See Section~\ref{Hints-databases} for the list of pre-defined databases and the way to create or extend a - database. This option can be combined with the previous one. + database. \item {\tt auto with *} @@ -3486,16 +3486,18 @@ hints of the database named {\tt core}. $lemma_i$ is an inductive type, it is the collection of its constructors which is added as hints. -\item \texttt{auto using} \nterm{lemma}$_1$ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$ with \ident$_1$ {\ldots} \ident$_n$ - - This combines the effects of the {\tt using} and {\tt with} options. - \item {\tt info\_auto} Behaves like {\tt auto} but shows the tactics it uses to solve the goal. This variant is very useful for getting a better understanding of automation, or to know what lemmas/assumptions were used. +\item {\tt \zeroone{info\_}auto \zeroone{\num}} \zeroone{{\tt using} \nterm{lemma}$_1$ + {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with} + \ident$_1$ {\ldots} \ident$_n$} + + This is the most general form, combining the various options. + \item {\tt trivial}\tacindex{trivial} This tactic is a restriction of {\tt auto} that is not recursive and @@ -3506,6 +3508,14 @@ hints of the database named {\tt core}. \item \texttt{trivial with *} +\item \texttt{trivial using} \nterm{lemma}$_1$ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$ + +\item {\tt info\_trivial} + +\item {\tt \zeroone{info\_}trivial} \zeroone{{\tt using} \nterm{lemma}$_1$ + {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with} + \ident$_1$ {\ldots} \ident$_n$} + \end{Variants} \Rem {\tt auto} either solves completely the goal or else leaves it @@ -3537,6 +3547,16 @@ Abort. Note that {\tt ex\_intro} should be declared as a hint. +\begin{Variants} + +\item {\tt \zeroone{info\_}eauto \zeroone{\num}} \zeroone{{\tt using} \nterm{lemma}$_1$ + {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with} + \ident$_1$ {\ldots} \ident$_n$} + + The various options for eauto are the same as for auto. + +\end{Variants} + \SeeAlso Section~\ref{Hints-databases} \subsection{\tt autounfold with \ident$_1$ \mbox{\dots} \ident$_n$} -- cgit v1.2.3 From e6f6cff7b88a70fe694507efe12885a776ab6730 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 19 Oct 2016 12:07:38 +0200 Subject: Change the order of arguments of fig2dev. For some reason, with my version of transfig (which seems to be the latest), the order of arguments of the fig2dev command matters: -L png must come before -m 2. I suppose that this fix shouldn't break things for others. --- Makefile.doc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile.doc b/Makefile.doc index b7251ce57..cea6f9b1a 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -61,7 +61,7 @@ endif (cd `dirname $<`; $(DVIPS) -q -o `basename $@` `basename $<`) %.png: %.fig - $(FIG2DEV) -m 2 -L png $< $@ + $(FIG2DEV) -L png -m 2 $< $@ %.pdf: %.fig $(FIG2DEV) -L pdftex $< $@ -- cgit v1.2.3 From 5be957316c23db6366aefc246d1d24480aa2f1ea Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 19 Oct 2016 14:18:52 +0200 Subject: Making the doc of auto hints more precise. The doc of auto hints now mention again that sometimes a hint will be used with simple apply and sometimes it will be used with exact. It does not try to be fully precise in that we don't necessarily want to document the behaviors of auto that we might like to change. See also the discussion on commit 9227d6e. --- doc/refman/RefMan-tac.tex | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 49a5b7983..263766b27 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3709,11 +3709,12 @@ The {\hintdef} is one of the following expressions: the number of subgoals generated by {\tt simple apply {\term}}. %{\tt auto} actually uses a slightly modified variant of {\tt simple apply} with use_metas_eagerly_in_conv_on_closed_terms set to false - % Is it really needed? - %% In case the inferred type of \term\ does not start with a product - %% the tactic added in the hint list is {\tt exact {\term}}. In case - %% this type can however be reduced to a type starting with a product, - %% the tactic {\tt apply {\term}} is also stored in the hints list. + In case the inferred type of \term\ does not start with a product + the tactic added in the hint list is {\tt exact {\term}}. +% Actually, a slightly restricted version is used (no conversion on the head symbol) + In case + this type can however be reduced to a type starting with a product, + the tactic {\tt simple apply {\term}} is also stored in the hints list. If the inferred type of \term\ contains a dependent quantification on a variable which occurs only in the premisses of the type and not -- cgit v1.2.3 From 1124ff6dd8fe4d04de8321375de101a42a2131f8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 19 Oct 2016 14:31:30 +0200 Subject: Error Resiliency: more conservative default (only curly braces) --- lib/flags.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/flags.ml b/lib/flags.ml index 35681804f..0e2f7e5a6 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -70,7 +70,7 @@ let priority_of_string = function | "high" -> High | _ -> raise (Invalid_argument "priority_of_string") type tac_error_filter = [ `None | `Only of string list | `All ] -let async_proofs_tac_error_resilience = ref (`Only [ "par" ; "curly" ]) +let async_proofs_tac_error_resilience = ref (`Only [ "curly" ]) let async_proofs_cmd_error_resilience = ref true let async_proofs_is_worker () = -- cgit v1.2.3 From 6fbe3c850bac9cbdfa64dbdcca7bd60dc7862190 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 19 Oct 2016 14:46:25 +0200 Subject: More comments in VM. --- kernel/byterun/coq_instruct.h | 2 ++ kernel/byterun/coq_interp.c | 15 ++++++++------- kernel/cbytegen.ml | 1 + kernel/make-opcodes | 3 ++- kernel/vconv.ml | 1 + 5 files changed, 14 insertions(+), 8 deletions(-) diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h index 8c5ab0ecb..885594ac7 100644 --- a/kernel/byterun/coq_instruct.h +++ b/kernel/byterun/coq_instruct.h @@ -14,6 +14,8 @@ /* Nota: this list of instructions is parsed to produce derived files */ /* coq_jumptbl.h and copcodes.ml. Instructions should be uppercase */ /* and alone on lines starting by two spaces. */ +/* If adding an instruction, DON'T FORGET TO UPDATE coq_fix_code.c */ +/* with the arity of the instruction and maybe coq_tcode_of_code. */ enum instructions { ACC0, ACC1, ACC2, ACC3, ACC4, ACC5, ACC6, ACC7, ACC, diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index df5fdce75..ddf40e2eb 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -539,6 +539,7 @@ value coq_interprete pc++;/* On saute le Restart */ } else { if (coq_extra_args < rec_pos) { + /* Partial application */ mlsize_t num_args, i; num_args = 1 + coq_extra_args; /* arg1 + extra args */ Alloc_small(accu, num_args + 2, Closure_tag); @@ -553,10 +554,10 @@ value coq_interprete } else { /* The recursif argument is an accumulator */ mlsize_t num_args, i; - /* Construction of partially applied PF */ + /* Construction of fixpoint applied to its [rec_pos-1] first arguments */ Alloc_small(accu, rec_pos + 2, Closure_tag); - Field(accu, 1) = coq_env; - for (i = 0; i < rec_pos; i++) Field(accu, i + 2) = sp[i]; + Field(accu, 1) = coq_env; // We store the fixpoint in the first field + for (i = 0; i < rec_pos; i++) Field(accu, i + 2) = sp[i]; // Storing args Code_val(accu) = pc; sp += rec_pos; *--sp = accu; @@ -1024,7 +1025,7 @@ value coq_interprete annot = *pc++; sz = *pc++; *--sp=Field(coq_global_data, annot); - /* On sauve la pile */ + /* We save the stack */ if (sz == 0) accu = Atom(0); else { Alloc_small(accu, sz, Default_tag); @@ -1035,17 +1036,17 @@ value coq_interprete } } *--sp = accu; - /* On cree le zipper switch */ + /* We create the switch zipper */ Alloc_small(accu, 5, Default_tag); Field(accu, 0) = (value)typlbl; Field(accu, 1) = (value)swlbl; Field(accu, 2) = sp[1]; Field(accu, 3) = sp[0]; Field(accu, 4) = coq_env; sp++;sp[0] = accu; - /* On cree l'atome */ + /* We create the atom */ Alloc_small(accu, 2, ATOM_SWITCH_TAG); Field(accu, 0) = sp[1]; Field(accu, 1) = sp[0]; sp++;sp[0] = accu; - /* On cree l'accumulateur */ + /* We create the accumulator */ Alloc_small(accu, 2, Accu_tag); Code_val(accu) = accumulate; Field(accu,1) = *sp++; diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 008955d80..7d08f9e2d 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -506,6 +506,7 @@ let comp_args comp_expr reloc args sz cont = done; !c +(* Precondition: args not empty *) let comp_app comp_fun comp_arg reloc f args sz cont = let nargs = Array.length args in match is_tailcall cont with diff --git a/kernel/make-opcodes b/kernel/make-opcodes index c8f573c68..e1371b3d0 100644 --- a/kernel/make-opcodes +++ b/kernel/make-opcodes @@ -1,2 +1,3 @@ $1=="enum" {n=0; next; } - {for (i = 1; i <= NF; i++) {printf("let op%s = %d\n", $i, n++);}} + {printf("(* THIS FILE IS GENERATED. DON'T EDIT. *)\n\n"); + for (i = 1; i <= NF; i++) {printf("let op%s = %d\n", $i, n++);}} diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 894f5296a..74d956bef 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -77,6 +77,7 @@ and conv_whd env pb k whd1 whd2 cu = | Vatom_stk(a1,stk1), Vatom_stk(a2,stk2) -> conv_atom env pb k a1 stk1 a2 stk2 cu | Vfun _, _ | _, Vfun _ -> + (* on the fly eta expansion *) conv_val env CONV (k+1) (apply_whd k whd1) (apply_whd k whd2) cu | Vsort _, _ | Vprod _, _ | Vfix _, _ | Vcofix _, _ | Vconstr_const _, _ -- cgit v1.2.3 From 21e1d501e17c9989d9cd689988a510e1864f817a Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 19 Oct 2016 15:43:39 +0200 Subject: Attempt to improve error rendering in pattern-matching compilation (#5142). When trying different possible return predicates, returns the error given by the first try, assuming this is the most interesting one. --- pretyping/cases.ml | 11 ++++++----- test-suite/output/Cases.out | 3 +++ test-suite/output/Cases.v | 12 ++++++++++++ 3 files changed, 21 insertions(+), 5 deletions(-) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 0ac34b718..5c9ce2624 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -62,13 +62,14 @@ let error_wrong_numarg_constructor_loc loc env c n = let error_wrong_numarg_inductive_loc loc env c n = raise_pattern_matching_error (loc, env, Evd.empty, WrongNumargInductive(c,n)) -let rec list_try_compile f = function - | [a] -> f a - | [] -> anomaly (str "try_find_f") +let list_try_compile f l = + let rec aux errors = function + | [] -> if errors = [] then anomaly (str "try_find_f") else raise (List.last errors) | h::t -> try f h - with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ -> - list_try_compile f t + with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ as e -> + aux (e::errors) t in + aux [] l let force_name = let nx = Name default_dependent_ident in function Anonymous -> nx | na -> na diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index 2b828d382..95fcd362e 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -56,3 +56,6 @@ match H with else fun _ : P false => Logic.I) x end : B -> True +The command has indeed failed with message: +Non exhaustive pattern-matching: no clause found for pattern +gadtTy _ _ diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index 3c2eaf42c..1903753cc 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -77,3 +77,15 @@ destruct b as [|] ; exact Logic.I. Defined. Print f. + +(* Was enhancement request #5142 (error message reported on the most + general return clause heuristic) *) + +Inductive gadt : Type -> Type := +| gadtNat : nat -> gadt nat +| gadtTy : forall T, T -> gadt T. + +Fail Definition gadt_id T (x: gadt T) : gadt T := + match x with + | gadtNat n => gadtNat n + end. -- cgit v1.2.3 From 00978cddf6e2da71892de6362e69c372429e159f Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 19 Oct 2016 17:20:06 +0200 Subject: Test for variant of #5142 (good error message on pattern-matching failure). --- test-suite/output/Cases.out | 13 +++++++++++++ test-suite/output/Cases.v | 17 +++++++++++++++++ 2 files changed, 30 insertions(+) diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index 95fcd362e..8ce6f9795 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -59,3 +59,16 @@ end The command has indeed failed with message: Non exhaustive pattern-matching: no clause found for pattern gadtTy _ _ +The command has indeed failed with message: +In environment +texpDenote : forall t : type, texp t -> typeDenote t +t : type +e : texp t +t1 : type +t2 : type +t0 : type +b : tbinop t1 t2 t0 +e1 : texp t1 +e2 : texp t2 +The term "0" has type "nat" while it is expected to have type + "typeDenote t0". diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index 1903753cc..407489642 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -89,3 +89,20 @@ Fail Definition gadt_id T (x: gadt T) : gadt T := match x with | gadtNat n => gadtNat n end. + +(* A variant of #5142 (see Satrajit Roy's example on coq-club (Oct 17, 2016)) *) + +Inductive type:Set:=Nat. +Inductive tbinop:type->type->type->Set:= TPlus : tbinop Nat Nat Nat. +Inductive texp:type->Set:= + |TNConst:nat->texp Nat + |TBinop:forall t1 t2 t, tbinop t1 t2 t->texp t1->texp t2->texp t. +Definition typeDenote(t:type):Set:= match t with Nat => nat end. + +(* We expect a failure on TBinop *) +Fail Fixpoint texpDenote t (e:texp t):typeDenote t:= + match e with + | TNConst n => n + | TBinop t1 t2 _ b e1 e2 => O + end. + -- cgit v1.2.3 From 3a507c03c91efe67afa9f2dd51bf77c7af6df0f5 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 19 Oct 2016 18:09:36 +0200 Subject: Documenting Hint Resolve -> and <- variants. These variants are from 8.3 but were never documented except in CHANGES. --- doc/refman/RefMan-tac.tex | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 263766b27..11de4f35e 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3744,6 +3744,17 @@ The {\hintdef} is one of the following expressions: Adds each \texttt{Resolve} {\term$_i$}. + \item {\tt Resolve -> \term} + + Adds the left-to-right implication of an equivalence as a hint + (informally the hint will be used as {\tt apply <- \term}, + although as mentionned before, the tactic actually used is + a restricted version of apply). + + \item {\tt Resolve <- \term} + + Adds the right-to-left implication of an equivalence as a hint. + \end{Variants} \item \texttt{Immediate {\term}} -- cgit v1.2.3 From b7f8221739ea0822b67e463774e108f8813ffaf3 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 19 Oct 2016 14:14:42 +0200 Subject: Refine printing of pending unification constraints It now prints evars with candidates as well if there are any. --- printing/printer.ml | 46 +++++++++++++++++++++++++++++++++++++--------- 1 file changed, 37 insertions(+), 9 deletions(-) diff --git a/printing/printer.ml b/printing/printer.ml index 6d54a5b3d..608bca62a 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -424,7 +424,16 @@ let pr_evgl_sign sigma evi = (str "(" ++ prlist_with_sep pr_comma pr_id ids ++ str " cannot be used)") in let pc = pr_lconstr_env env sigma evi.evar_concl in - hov 0 (str"[" ++ ps ++ spc () ++ str"|- " ++ pc ++ str"]" ++ spc () ++ warn) + let candidates = + match evi.evar_body, evi.evar_candidates with + | Evar_empty, Some l -> + spc () ++ str "= {" ++ + prlist_with_sep (fun () -> str "|") (pr_lconstr_env env sigma) l ++ str "}" + | _ -> + mt () + in + hov 0 (str"[" ++ ps ++ spc () ++ str"|- " ++ pc ++ str"]" ++ + candidates ++ spc () ++ warn) (* Print an existential variable *) @@ -471,7 +480,7 @@ let default_pr_subgoal n sigma = let pr_internal_existential_key ev = str (string_of_existential ev) -let print_evar_constraints gl sigma cstrs = +let print_evar_constraints gl sigma = let pr_env = match gl with | None -> fun e' -> pr_context_of e' sigma @@ -487,6 +496,14 @@ let print_evar_constraints gl sigma cstrs = let pr_evconstr (pbty,env,t1,t2) = let t1 = Evarutil.nf_evar sigma t1 and t2 = Evarutil.nf_evar sigma t2 in + let env = + (** We currently allow evar instances to refer to anonymous de Bruijn + indices, so we protect the error printing code in this case by giving + names to every de Bruijn variable in the rel_context of the conversion + problem. MS: we should rather stop depending on anonymous variables, they + can be used to indicate independency. Also, this depends on a strategy for + naming/renaming *) + Namegen.make_all_name_different env in str" " ++ hov 2 (pr_env env ++ pr_lconstr_env env sigma t1 ++ spc () ++ str (match pbty with @@ -494,7 +511,23 @@ let print_evar_constraints gl sigma cstrs = | Reduction.CUMUL -> "<=") ++ spc () ++ pr_lconstr_env env sigma t2) in - prlist_with_sep fnl pr_evconstr cstrs + let pr_candidate ev evi (candidates,acc) = + if Option.has_some evi.evar_candidates then + (succ candidates, acc ++ pr_evar sigma (ev,evi) ++ fnl ()) + else (candidates, acc) + in + let constraints = + let _, cstrs = Evd.extract_all_conv_pbs sigma in + if List.is_empty cstrs then mt () + else fnl () ++ str (String.plural (List.length cstrs) "unification constraint") + ++ str":" ++ fnl () ++ hov 0 (prlist_with_sep fnl pr_evconstr cstrs) + in + let candidates, ppcandidates = Evd.fold_undefined pr_candidate sigma (0,mt ()) in + constraints ++ + if candidates > 0 then + fnl () ++ str (String.plural candidates "existential") ++ + str" with candidates:" ++ fnl () ++ hov 0 ppcandidates + else mt () let should_print_dependent_evars = ref true @@ -509,12 +542,7 @@ let _ = optwrite = (fun v -> should_print_dependent_evars := v) } let print_dependent_evars gl sigma seeds = - let constraints = - let _, cstrs = Evd.extract_all_conv_pbs sigma in - if List.is_empty cstrs then mt () - else fnl () ++ str (String.plural (List.length cstrs) "unification constraint") - ++ str":" ++ fnl () ++ hov 0 (print_evar_constraints gl sigma cstrs) - in + let constraints = print_evar_constraints gl sigma in let evars () = if !should_print_dependent_evars then let evars = Evarutil.gather_dependent_evars sigma seeds in -- cgit v1.2.3 From 2dfe032fd42f2489320936fe1e60c9cf7dafe8cf Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 3 Mar 2016 18:26:12 +0100 Subject: [search] Don't build intermediate lists in search. This patch converts the `search_*` functions to use an iter-style API. Consequently, the Search Vernac will produce a message for each search result, greatly improving roundtrip time as IDEs can effectively display the results in a streaming way. It also allows different printers to be used. I didn't observe a performance difference (as things seem to be dominated by printing and `Declaremods`). As a minor tweak, we make search with "Output Name Only" more efficient. Motivation: ----------- Currently, the main search API `Search.generic_search` is an effectful, iteration-based function: ```ocaml val generic_search : int option -> display_function -> unit ``` This type is imposed by `Declaremods`, which exposes an effectful, iteration-based API to traverse Coq library objects. The `Search.search_*` functions try to offer a more functional API by returning a list of pretty printing commands. They need to build an internal intermediate list for that purpose. However, this is a waste of time, as the destination of these lists is to be flushed out by the printer right away. --- dev/doc/changes.txt | 6 ++++ test-suite/output/SearchPattern.out | 2 -- toplevel/search.ml | 55 ++++++++----------------------------- toplevel/search.mli | 11 +++++--- toplevel/vernacentries.ml | 41 +++++++++++++++++++++++---- 5 files changed, 61 insertions(+), 54 deletions(-) diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 6dd7cb970..79a0c6312 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -256,6 +256,12 @@ define_evar_* mostly used internally in the unification engine. - `Tacexpr.TacDynamic(Loc.dummy_loc, Pretyping.constr_in c)` --> `Tacinterp.Value.of_constr c` +** Search API ** + +The main search functions now take a function iterating over the +results. This allows for clients to use streaming or more economic +printing. + ========================================= = CHANGES BETWEEN COQ V8.4 AND COQ V8.5 = ========================================= diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out index 1eb7eca8f..f3c12effc 100644 --- a/test-suite/output/SearchPattern.out +++ b/test-suite/output/SearchPattern.out @@ -40,7 +40,6 @@ Nat.land: nat -> nat -> nat Nat.lor: nat -> nat -> nat Nat.ldiff: nat -> nat -> nat Nat.lxor: nat -> nat -> nat - S: nat -> nat Nat.succ: nat -> nat Nat.pred: nat -> nat @@ -74,7 +73,6 @@ le_n: forall n : nat, n <= n pair: forall A B : Type, A -> B -> A * B conj: forall A B : Prop, A -> B -> A /\ B Nat.divmod: nat -> nat -> nat -> nat -> nat * nat - h: n <> newdef n h: n <> newdef n h: P n diff --git a/toplevel/search.ml b/toplevel/search.ml index 921308f78..ff3c7a4f4 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -29,17 +29,6 @@ query, separated by a newline. This type of output is useful for editors (like emacs), to generate a list of completion candidates without having to parse thorugh the types of all symbols. *) -let search_output_name_only = ref false - -let _ = - declare_bool_option - { optsync = true; - optdepr = false; - optname = "output-name-only search"; - optkey = ["Search";"Output";"Name";"Only"]; - optread = (fun () -> !search_output_name_only); - optwrite = (:=) search_output_name_only } - type glob_search_about_item = | GlobSearchSubPattern of constr_pattern | GlobSearchString of string @@ -118,18 +107,6 @@ let generic_search glnumopt fn = | Some glnum -> iter_hypothesis glnum fn); iter_declarations fn -(** Standard display *) -let plain_display accu ref env c = - let pr = pr_global ref in - if !search_output_name_only then - accu := pr :: !accu - else begin - let pc = pr_lconstr_env env Evd.empty c in - accu := hov 2 (pr ++ str":" ++ spc () ++ pc) :: !accu - end - -let format_display l = prlist_with_sep fnl (fun x -> x) (List.rev l) - (** Filters *) (** This function tries to see whether the conclusion matches a pattern. *) @@ -181,8 +158,7 @@ let search_about_filter query gr env typ = match query with (** SearchPattern *) -let search_pattern gopt pat mods = - let ans = ref [] in +let search_pattern gopt pat mods pr_search = let blacklist_filter = blacklist_filter_aux () in let filter ref env typ = module_filter mods ref env typ && @@ -190,10 +166,9 @@ let search_pattern gopt pat mods = blacklist_filter ref env typ in let iter ref env typ = - if filter ref env typ then plain_display ans ref env typ + if filter ref env typ then pr_search ref env typ in - let () = generic_search gopt iter in - format_display !ans + generic_search gopt iter (** SearchRewrite *) @@ -205,10 +180,9 @@ let rewrite_pat1 pat = let rewrite_pat2 pat = PApp (PRef eq, [| PMeta None; PMeta None; pat |]) -let search_rewrite gopt pat mods = +let search_rewrite gopt pat mods pr_search = let pat1 = rewrite_pat1 pat in let pat2 = rewrite_pat2 pat in - let ans = ref [] in let blacklist_filter = blacklist_filter_aux () in let filter ref env typ = module_filter mods ref env typ && @@ -217,15 +191,13 @@ let search_rewrite gopt pat mods = blacklist_filter ref env typ in let iter ref env typ = - if filter ref env typ then plain_display ans ref env typ + if filter ref env typ then pr_search ref env typ in - let () = generic_search gopt iter in - format_display !ans + generic_search gopt iter (** Search *) -let search_by_head gopt pat mods = - let ans = ref [] in +let search_by_head gopt pat mods pr_search = let blacklist_filter = blacklist_filter_aux () in let filter ref env typ = module_filter mods ref env typ && @@ -233,15 +205,13 @@ let search_by_head gopt pat mods = blacklist_filter ref env typ in let iter ref env typ = - if filter ref env typ then plain_display ans ref env typ + if filter ref env typ then pr_search ref env typ in - let () = generic_search gopt iter in - format_display !ans + generic_search gopt iter (** SearchAbout *) -let search_about gopt items mods = - let ans = ref [] in +let search_about gopt items mods pr_search = let blacklist_filter = blacklist_filter_aux () in let filter ref env typ = let eqb b1 b2 = if b1 then b2 else not b2 in @@ -251,10 +221,9 @@ let search_about gopt items mods = blacklist_filter ref env typ in let iter ref env typ = - if filter ref env typ then plain_display ans ref env typ + if filter ref env typ then pr_search ref env typ in - let () = generic_search gopt iter in - format_display !ans + generic_search gopt iter type search_constraint = | Name_Pattern of Str.regexp diff --git a/toplevel/search.mli b/toplevel/search.mli index 9f209a17e..ba3d48efc 100644 --- a/toplevel/search.mli +++ b/toplevel/search.mli @@ -39,11 +39,14 @@ val search_about_filter : glob_search_about_item -> filter_function goal and the global environment for things matching [pattern] and satisfying module exclude/include clauses of [modinout]. *) -val search_by_head : int option -> constr_pattern -> DirPath.t list * bool -> std_ppcmds -val search_rewrite : int option -> constr_pattern -> DirPath.t list * bool -> std_ppcmds -val search_pattern : int option -> constr_pattern -> DirPath.t list * bool -> std_ppcmds +val search_by_head : int option -> constr_pattern -> DirPath.t list * bool + -> display_function -> unit +val search_rewrite : int option -> constr_pattern -> DirPath.t list * bool + -> display_function -> unit +val search_pattern : int option -> constr_pattern -> DirPath.t list * bool + -> display_function -> unit val search_about : int option -> (bool * glob_search_about_item) list - -> DirPath.t list * bool -> std_ppcmds + -> DirPath.t list * bool -> display_function -> unit type search_constraint = (** Whether the name satisfies a regexp (uses Ocaml Str syntax) *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index df83f7685..f69bac437 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1665,6 +1665,28 @@ let interp_search_about_item env = errorlabstrm "interp_search_about_item" (str "Unable to interp \"" ++ str s ++ str "\" either as a reference or as an identifier component") +(* 05f22a5d6d5b8e3e80f1a37321708ce401834430 introduced the + `search_output_name_only` option to avoid excessive printing when + searching. + + The motivation was to make search usable for IDE completion, + however, it is still too slow due to the non-indexed nature of the + underlying search mechanism. + + In the future we should deprecate the option and provide a fast, + indexed name-searching interface. +*) +let search_output_name_only = ref false + +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "output-name-only search"; + optkey = ["Search";"Output";"Name";"Only"]; + optread = (fun () -> !search_output_name_only); + optwrite = (:=) search_output_name_only } + let vernac_search s gopt r = let r = interp_search_restriction r in let env,gopt = @@ -1676,16 +1698,25 @@ let vernac_search s gopt r = | Some g -> snd (Pfedit.get_goal_context g) , Some g in let get_pattern c = snd (intern_constr_pattern env c) in - let open Feedback in + let pr_search ref env c = + let pr = pr_global ref in + let pp = if !search_output_name_only + then pr + else begin + let pc = pr_lconstr_env env Evd.empty c in + hov 2 (pr ++ str":" ++ spc () ++ pc) + end + in Feedback.msg_notice pp + in match s with | SearchPattern c -> - msg_notice (Search.search_pattern gopt (get_pattern c) r) + Search.search_pattern gopt (get_pattern c) r pr_search | SearchRewrite c -> - msg_notice (Search.search_rewrite gopt (get_pattern c) r) + Search.search_rewrite gopt (get_pattern c) r pr_search | SearchHead c -> - msg_notice (Search.search_by_head gopt (get_pattern c) r) + Search.search_by_head gopt (get_pattern c) r pr_search | SearchAbout sl -> - msg_notice (Search.search_about gopt (List.map (on_snd (interp_search_about_item env)) sl) r) + Search.search_about gopt (List.map (on_snd (interp_search_about_item env)) sl) r pr_search let vernac_locate = let open Feedback in function | LocateAny (AN qid) -> msg_notice (print_located_qualid qid) -- cgit v1.2.3 From 474a58b15ca41f1b3287ef3e29e80cca9988598c Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 28 Sep 2016 17:26:14 +0200 Subject: Fix bug #5036 autorewrite, sections and universes Universe context not properly declared. Improve API and code in declare.ml to allow declaration of universe contexts, used by declaration of universes and constraints (separately). --- library/declare.ml | 28 +++++++++++++++++++++++----- library/declare.mli | 4 +++- ltac/extratactics.ml4 | 5 ++++- test-suite/bugs/closed/5036.v | 10 ++++++++++ 4 files changed, 40 insertions(+), 7 deletions(-) create mode 100644 test-suite/bugs/closed/5036.v diff --git a/library/declare.ml b/library/declare.ml index 3d063225f..b83f2dee0 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -434,6 +434,23 @@ let assumption_message id = (** Global universe names, in a different summary *) +type universe_context_decl = polymorphic * Univ.universe_context_set + +let cache_universe_context (p, ctx) = + Global.push_context_set p ctx; + if p then Lib.add_section_context ctx + +let input_universe_context : universe_context_decl -> Libobject.obj = + declare_object + { (default_object "Global universe context state") with + cache_function = (fun (na, pi) -> cache_universe_context pi); + load_function = (fun _ (_, pi) -> cache_universe_context pi); + discharge_function = (fun (_, (p, _ as x)) -> if p then None else Some x); + classify_function = (fun a -> Keep a) } + +let declare_universe_context poly ctx = + Lib.add_anonymous_leaf (input_universe_context (poly, ctx)) + (* Discharged or not *) type universe_decl = polymorphic * (Id.t * Univ.universe_level) list @@ -446,9 +463,8 @@ let cache_universes (p, l) = Univ.ContextSet.add_universe lev ctx)) (glob, Univ.ContextSet.empty) l in - Global.push_context_set p ctx; - if p then Lib.add_section_context ctx; - Universes.set_global_universe_names glob' + cache_universe_context (p, ctx); + Universes.set_global_universe_names glob' let input_universes : universe_decl -> Libobject.obj = declare_object @@ -475,8 +491,10 @@ let do_universe poly l = type constraint_decl = polymorphic * Univ.constraints let cache_constraints (na, (p, c)) = - Global.add_constraints c; - if p then Lib.add_section_context (Univ.ContextSet.add_constraints c Univ.ContextSet.empty) + let ctx = + Univ.ContextSet.add_constraints c + Univ.ContextSet.empty (* No declared universes here, just constraints *) + in cache_universe_context (p,ctx) let discharge_constraints (_, (p, c as a)) = if p then None else Some a diff --git a/library/declare.mli b/library/declare.mli index 7824506da..e614f5206 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -87,7 +87,9 @@ val exists_name : Id.t -> bool -(** Global universe names and constraints *) +(** Global universe contexts, names and constraints *) + +val declare_universe_context : polymorphic -> Univ.universe_context_set -> unit val do_universe : polymorphic -> Id.t Loc.located list -> unit val do_constraint : polymorphic -> (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index e50b0520b..db7318469 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -263,7 +263,10 @@ let add_rewrite_hint bases ort t lcsr = let ctx = let ctx = UState.context_set ctx in if poly then ctx - else (Global.push_context_set false ctx; Univ.ContextSet.empty) + else (** This is a global universe context that shouldn't be + refreshed at every use of the hint, declare it globally. *) + (Declare.declare_universe_context false ctx; + Univ.ContextSet.empty) in Constrexpr_ops.constr_loc ce, (c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t in let eqs = List.map f lcsr in diff --git a/test-suite/bugs/closed/5036.v b/test-suite/bugs/closed/5036.v new file mode 100644 index 000000000..12c958be6 --- /dev/null +++ b/test-suite/bugs/closed/5036.v @@ -0,0 +1,10 @@ +Section foo. + Context (F : Type -> Type). + Context (admit : forall {T}, F T = True). + Hint Rewrite (fun T => @admit T). + Lemma bad : F False. + Proof. + autorewrite with core. + constructor. + Qed. +End foo. (* Anomaly: Universe Top.16 undefined. Please report. *) \ No newline at end of file -- cgit v1.2.3 From ecaea9a428c052ea431ec7c392e81aaf918d5d96 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 10 Oct 2016 17:28:05 +0200 Subject: Fix minimization to be insensitive to redundant arcs. The new algorithm produces different sets of arcs than in 8.5, hence existing developments may fail to pass now because they relied on the (correct but more approximate) result of minimization in 8.5 which wasn't insensitive. The algorithm works bottom-up on the (well-founded) graph to find lower levels that an upper level can be minimized to. We filter said lower levels according to the lower sets of the other levels we consider. If they appear in any of them then we don't need their constraints. Does not seem to have a huge impact on performance in HoTT, but this should be evaluated further. Adapt test-suite files accordingly. --- library/universes.ml | 133 ++++++++++++++++++++++++++++++------------ library/universes.mli | 13 +++-- test-suite/bugs/closed/4527.v | 6 +- test-suite/bugs/closed/4544.v | 4 +- 4 files changed, 110 insertions(+), 46 deletions(-) diff --git a/library/universes.ml b/library/universes.ml index db95607f1..08ff2ced8 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -702,12 +702,43 @@ let pr_universe_body = function let pr_universe_opt_subst = Univ.LMap.pr pr_universe_body -exception Found of Level.t +let compare_constraint_type d d' = + match d, d' with + | Eq, Eq | Le, Le | Lt, Lt -> 0 + | Eq, _ -> -1 + | Le, Eq -> 1 + | Le, Lt -> -1 + | Lt, (Eq | Le) -> 1 + +type lowermap = constraint_type LMap.t + +let lower_union = + let merge k a b = + match a, b with + | Some _, None -> a + | None, Some _ -> b + | None, None -> None + | Some l, Some r -> + if compare_constraint_type l r >= 0 then a + else b + in LMap.merge merge + +let lower_add l c m = + try let c' = LMap.find l m in + if compare_constraint_type c c' > 0 then + LMap.add l c m + else m + with Not_found -> LMap.add l c m + +let lower_of_list l = + List.fold_left (fun acc (d,l) -> LMap.add l d acc) LMap.empty l + +exception Found of Level.t * lowermap let find_inst insts v = - try LMap.iter (fun k (enf,alg,v') -> - if not alg && enf && Universe.equal v' v then raise (Found k)) + try LMap.iter (fun k (enf,alg,v',lower) -> + if not alg && enf && Universe.equal v' v then raise (Found (k, lower))) insts; raise Not_found - with Found l -> l + with Found (f,l) -> (f,l) let compute_lbound left = (** The universe variable was not fixed yet. @@ -726,27 +757,33 @@ let compute_lbound left = else None)) None left -let instantiate_with_lbound u lbound alg enforce (ctx, us, algs, insts, cstrs) = +let instantiate_with_lbound u lbound lower alg enforce (ctx, us, algs, insts, cstrs) = if enforce then let inst = Universe.make u in let cstrs' = enforce_leq lbound inst cstrs in (ctx, us, LSet.remove u algs, - LMap.add u (enforce,alg,lbound) insts, cstrs'), (enforce, alg, inst) + LMap.add u (enforce,alg,lbound,lower) insts, cstrs'), + (enforce, alg, inst, lower) else (* Actually instantiate *) (Univ.LSet.remove u ctx, Univ.LMap.add u (Some lbound) us, algs, - LMap.add u (enforce,alg,lbound) insts, cstrs), (enforce, alg, lbound) + LMap.add u (enforce,alg,lbound,lower) insts, cstrs), + (enforce, alg, lbound, lower) type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t let pr_constraints_map cmap = LMap.fold (fun l cstrs acc -> Level.pr l ++ str " => " ++ - prlist_with_sep spc (fun (d,r) -> pr_constraint_type d ++ Level.pr r) cstrs ++ fnl () - ++ acc) + prlist_with_sep spc (fun (d,r) -> pr_constraint_type d ++ Level.pr r) cstrs ++ + fnl () ++ acc) cmap (mt ()) let remove_alg l (ctx, us, algs, insts, cstrs) = (ctx, us, LSet.remove l algs, insts, cstrs) + +let remove_lower u lower = + let levels = Universe.levels u in + LSet.fold (fun l acc -> LMap.remove l acc) levels lower let minimize_univ_variables ctx us algs left right cstrs = let left, lbounds = @@ -756,22 +793,44 @@ let minimize_univ_variables ctx us algs left right cstrs = let lbounds' = match compute_lbound (List.map (fun (d,l) -> d, Universe.make l) lower) with | None -> lbounds - | Some lbound -> LMap.add r (true, false, lbound) lbounds + | Some lbound -> LMap.add r (true, false, lbound, lower_of_list lower) + lbounds in (Univ.LMap.remove r left, lbounds')) left (left, Univ.LMap.empty) in let rec instance (ctx', us, algs, insts, cstrs as acc) u = - let acc, left = + let acc, left, lower = try let l = LMap.find u left in - List.fold_left - (fun (acc, left') (d, l) -> - let acc', (enf,alg,l') = aux acc l in - let l' = - if enf then Universe.make l - else l' - in acc', (d, l') :: left') - (acc, []) l - with Not_found -> acc, [] + let acc, left, newlow, lower = + List.fold_left + (fun (acc, left', newlow, lower') (d, l) -> + let acc', (enf,alg,l',lower) = aux acc l in + let l' = + if enf then Universe.make l + else l' + in acc', (d, l') :: left', + lower_add l d newlow, lower_union lower lower') + (acc, [], LMap.empty, LMap.empty) l + in + let not_lower (d,l) = + Univ.Universe.exists + (fun (l,i) -> + let d = + if i == 0 then d + else match d with + | Le -> Lt + | d -> d + in + try let d' = LMap.find l lower in + (* If d is stronger than the already implied lower + * constraints we must keep it *) + compare_constraint_type d d' > 0 + with Not_found -> + (** No constraint existing on l *) true) l + in + let left = List.uniquize (List.filter not_lower left) in + (acc, left, LMap.union newlow lower) + with Not_found -> acc, [], LMap.empty and right = try Some (LMap.find u right) with Not_found -> None @@ -779,31 +838,33 @@ let minimize_univ_variables ctx us algs left right cstrs = let instantiate_lbound lbound = let alg = LSet.mem u algs in if alg then - (* u is algebraic: we instantiate it with it's lower bound, if any, + (* u is algebraic: we instantiate it with its lower bound, if any, or enforce the constraints if it is bounded from the top. *) - instantiate_with_lbound u lbound true false acc + let lower = remove_lower lbound lower in + instantiate_with_lbound u lbound lower true false acc else (* u is non algebraic *) match Universe.level lbound with | Some l -> (* The lowerbound is directly a level *) (* u is not algebraic but has no upper bounds, we instantiate it with its lower bound if it is a different level, otherwise we keep it. *) + let lower = LMap.remove l lower in if not (Level.equal l u) then (* Should check that u does not have upper constraints that are not already in right *) let acc' = remove_alg l acc in - instantiate_with_lbound u lbound false false acc' - else acc, (true, false, lbound) - | None -> - try - (* if right <> None then raise Not_found; *) - (* Another universe represents the same lower bound, - we can share them with no harm. *) - let can = find_inst insts lbound in - instantiate_with_lbound u (Universe.make can) false false acc + instantiate_with_lbound u lbound lower false false acc' + else acc, (true, false, lbound, lower) + | None -> + try + (* Another universe represents the same lower bound, + we can share them with no harm. *) + let can, lower = find_inst insts lbound in + let lower = LMap.remove can lower in + instantiate_with_lbound u (Universe.make can) lower false false acc with Not_found -> (* We set u as the canonical universe representing lbound *) - instantiate_with_lbound u lbound false true acc + instantiate_with_lbound u lbound lower false true acc in let acc' acc = match right with @@ -812,7 +873,7 @@ let minimize_univ_variables ctx us algs left right cstrs = let dangling = List.filter (fun (d, r) -> not (LMap.mem r us)) cstrs in if List.is_empty dangling then acc else - let ((ctx', us, algs, insts, cstrs), (enf,_,inst as b)) = acc in + let ((ctx', us, algs, insts, cstrs), (enf,_,inst,lower as b)) = acc in let cstrs' = List.fold_left (fun cstrs (d, r) -> if d == Univ.Le then enforce_leq inst (Universe.make r) cstrs @@ -824,15 +885,15 @@ let minimize_univ_variables ctx us algs left right cstrs = in (ctx', us, algs, insts, cstrs'), b in - if not (LSet.mem u ctx) then acc' (acc, (true, false, Universe.make u)) + if not (LSet.mem u ctx) then acc' (acc, (true, false, Universe.make u, lower)) else let lbound = compute_lbound left in match lbound with | None -> (* Nothing to do *) - acc' (acc, (true, false, Universe.make u)) + acc' (acc, (true, false, Universe.make u, lower)) | Some lbound -> try acc' (instantiate_lbound lbound) - with Failure _ -> acc' (acc, (true, false, Universe.make u)) + with Failure _ -> acc' (acc, (true, false, Universe.make u, lower)) and aux (ctx', us, algs, seen, cstrs as acc) u = try acc, LMap.find u seen with Not_found -> instance acc u diff --git a/library/universes.mli b/library/universes.mli index a5740ec49..c8cf7047e 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -243,28 +243,31 @@ val choose_canonical : universe_set -> (Level.t -> bool) (* flexibles *) -> univ val compute_lbound : (constraint_type * Univ.universe) list -> universe option +type lowermap = constraint_type Univ.LMap.t + val instantiate_with_lbound : Univ.LMap.key -> Univ.universe -> + lowermap -> bool -> bool -> Univ.LSet.t * Univ.universe option Univ.LMap.t * Univ.LSet.t * - (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints -> + (bool * bool * Univ.universe * lowermap) Univ.LMap.t * Univ.constraints -> (Univ.LSet.t * Univ.universe option Univ.LMap.t * Univ.LSet.t * - (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints) * - (bool * bool * Univ.universe) + (bool * bool * Univ.universe * lowermap) Univ.LMap.t * Univ.constraints) * + (bool * bool * Univ.universe * lowermap) val minimize_univ_variables : Univ.LSet.t -> Univ.universe option Univ.LMap.t -> Univ.LSet.t -> - constraints_map -> constraints_map -> + constraints_map -> constraints_map -> Univ.constraints -> Univ.LSet.t * Univ.universe option Univ.LMap.t * Univ.LSet.t * - (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints + (bool * bool * Univ.universe * lowermap) Univ.LMap.t * Univ.constraints (** {6 Support for old-style sort-polymorphism } *) diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v index 4ca6fe78c..08628377f 100644 --- a/test-suite/bugs/closed/4527.v +++ b/test-suite/bugs/closed/4527.v @@ -249,10 +249,10 @@ Section Reflective_Subuniverse. exact H. Defined. - Definition inO_paths@{i j} (S : Type@{i}) {S_inO : In@{Ou Oa i} O S} (x y : + Definition inO_paths@{i} (S : Type@{i}) {S_inO : In@{Ou Oa i} O S} (x y : S) : In@{Ou Oa i} O (x=y). Proof. - simple refine (inO_to_O_retract@{i j} _ _ _); intro u. + simple refine (inO_to_O_retract@{i} _ _ _); intro u. - assert (p : (fun _ : O (x=y) => x) == (fun _=> y)). { @@ -264,4 +264,4 @@ S) : In@{Ou Oa i} O (x=y). hnf. rewrite O_indpaths_beta; reflexivity. Qed. - Check inO_paths@{Type Type}. + Check inO_paths@{Type}. diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v index 048f31ce3..da140c931 100644 --- a/test-suite/bugs/closed/4544.v +++ b/test-suite/bugs/closed/4544.v @@ -652,7 +652,7 @@ Defined. Definition ReflectiveSubuniverse := Modality. - Definition O_reflector := O_reflector. + Definition O_reflector@{u a i} := O_reflector@{u a i}. Definition In@{u a i} : forall (O : ReflectiveSubuniverse@{u a}), Type2le@{i a} -> Type2le@{i a} @@ -660,7 +660,7 @@ Defined. Definition O_inO@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}), In@{u a i} O (O_reflector@{u a i} O T) := O_inO@{u a i}. - Definition to := to. + Definition to@{u a i} := to@{u a i}. Definition inO_equiv_inO@{u a i j k} : forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}) (U : Type@{j}) (T_inO : In@{u a i} O T) (f : T -> U) (feq : IsEquiv f), -- cgit v1.2.3 From 1df663324385c9958df76f3f464b6afab4c17ad7 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 20 Oct 2016 17:51:20 +0200 Subject: Cleanup code according to comments. --- library/universes.ml | 76 ++++++++++++++++++++++++++++----------------------- library/universes.mli | 37 ------------------------- 2 files changed, 42 insertions(+), 71 deletions(-) diff --git a/library/universes.ml b/library/universes.ml index 08ff2ced8..112b20a4c 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -704,11 +704,13 @@ let pr_universe_opt_subst = Univ.LMap.pr pr_universe_body let compare_constraint_type d d' = match d, d' with - | Eq, Eq | Le, Le | Lt, Lt -> 0 + | Eq, Eq -> 0 | Eq, _ -> -1 - | Le, Eq -> 1 - | Le, Lt -> -1 - | Lt, (Eq | Le) -> 1 + | _, Eq -> 1 + | Le, Le -> 0 + | Le, _ -> -1 + | _, Le -> 1 + | Lt, Lt -> 0 type lowermap = constraint_type LMap.t @@ -800,36 +802,42 @@ let minimize_univ_variables ctx us algs left right cstrs = in let rec instance (ctx', us, algs, insts, cstrs as acc) u = let acc, left, lower = - try let l = LMap.find u left in - let acc, left, newlow, lower = - List.fold_left - (fun (acc, left', newlow, lower') (d, l) -> - let acc', (enf,alg,l',lower) = aux acc l in - let l' = - if enf then Universe.make l - else l' - in acc', (d, l') :: left', - lower_add l d newlow, lower_union lower lower') - (acc, [], LMap.empty, LMap.empty) l - in - let not_lower (d,l) = - Univ.Universe.exists - (fun (l,i) -> - let d = - if i == 0 then d - else match d with - | Le -> Lt - | d -> d - in - try let d' = LMap.find l lower in - (* If d is stronger than the already implied lower - * constraints we must keep it *) - compare_constraint_type d d' > 0 - with Not_found -> - (** No constraint existing on l *) true) l - in - let left = List.uniquize (List.filter not_lower left) in - (acc, left, LMap.union newlow lower) + try + let l = LMap.find u left in + let acc, left, newlow, lower = + List.fold_left + (fun (acc, left', newlow, lower') (d, l) -> + let acc', (enf,alg,l',lower) = aux acc l in + let l' = + if enf then Universe.make l + else l' + in acc', (d, l') :: left', + lower_add l d newlow, lower_union lower lower') + (acc, [], LMap.empty, LMap.empty) l + in + let not_lower (d,l) = + (* We're checking if (d,l) is already implied by the lower + constraints on some level u. If it represents l < u (d is Lt + or d is Le and i > 0, the i < 0 case is impossible due to + invariants of Univ), and the lower constraints only have l <= + u then it is not implied. *) + Univ.Universe.exists + (fun (l,i) -> + let d = + if i == 0 then d + else match d with + | Le -> Lt + | d -> d + in + try let d' = LMap.find l lower in + (* If d is stronger than the already implied lower + * constraints we must keep it. *) + compare_constraint_type d d' > 0 + with Not_found -> + (** No constraint existing on l *) true) l + in + let left = List.uniquize (List.filter not_lower left) in + (acc, left, LMap.union newlow lower) with Not_found -> acc, [], LMap.empty and right = try Some (LMap.find u right) diff --git a/library/universes.mli b/library/universes.mli index c8cf7047e..d3a271b8d 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -232,43 +232,6 @@ val refresh_constraints : UGraph.t -> universe_context_set -> universe_context_s val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds -(* For tracing *) - -type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t - -val pr_constraints_map : constraints_map -> Pp.std_ppcmds - -val choose_canonical : universe_set -> (Level.t -> bool) (* flexibles *) -> universe_set -> universe_set -> - universe_level * (universe_set * universe_set * universe_set) - -val compute_lbound : (constraint_type * Univ.universe) list -> universe option - -type lowermap = constraint_type Univ.LMap.t - -val instantiate_with_lbound : - Univ.LMap.key -> - Univ.universe -> - lowermap -> - bool -> - bool -> - Univ.LSet.t * Univ.universe option Univ.LMap.t * - Univ.LSet.t * - (bool * bool * Univ.universe * lowermap) Univ.LMap.t * Univ.constraints -> - (Univ.LSet.t * Univ.universe option Univ.LMap.t * - Univ.LSet.t * - (bool * bool * Univ.universe * lowermap) Univ.LMap.t * Univ.constraints) * - (bool * bool * Univ.universe * lowermap) - -val minimize_univ_variables : - Univ.LSet.t -> - Univ.universe option Univ.LMap.t -> - Univ.LSet.t -> - constraints_map -> constraints_map -> - Univ.constraints -> - Univ.LSet.t * Univ.universe option Univ.LMap.t * - Univ.LSet.t * - (bool * bool * Univ.universe * lowermap) Univ.LMap.t * Univ.constraints - (** {6 Support for old-style sort-polymorphism } *) val solve_constraints_system : universe option array -> universe array -> universe array -> -- cgit v1.2.3 From a07f67f6f1deba8b14672c618c003ec345d7970a Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 24 Sep 2016 16:37:04 +0200 Subject: A fix for #5097 (status of evars refined by "clear" in ltac: closed wrt evars). If an existing evar was cleared in pretyping (typically while processing "ltac:"), it created an evar considered as new. Updating them instead along the "cleared" flag. If correct, I suspect similar treatment should be done for refining along "change", "rename" and "move". --- pretyping/evarutil.ml | 22 ++++++++++++++++++++++ pretyping/evarutil.mli | 6 ++++++ pretyping/pretyping.ml | 31 ++++++++++++++++++------------- proofs/proofview.ml | 36 ++++++------------------------------ test-suite/bugs/closed/5097.v | 7 +++++++ 5 files changed, 59 insertions(+), 43 deletions(-) create mode 100644 test-suite/bugs/closed/5097.v diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 759e0e4d6..9a9c946ae 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -600,6 +600,28 @@ let gather_dependent_evars evm l = (* /spiwack *) +(** [advance sigma g] returns [Some g'] if [g'] is undefined and is + the current avatar of [g] (for instance [g] was changed by [clear] + into [g']). It returns [None] if [g] has been (partially) + solved. *) +(* spiwack: [advance] is probably performance critical, and the good + behaviour of its definition may depend sensitively to the actual + definition of [Evd.find]. Currently, [Evd.find] starts looking for + a value in the heap of undefined variable, which is small. Hence in + the most common case, where [advance] is applied to an unsolved + goal ([advance] is used to figure if a side effect has modified the + goal) it terminates quickly. *) +let rec advance sigma evk = + let evi = Evd.find sigma evk in + match evi.evar_body with + | Evar_empty -> Some evk + | Evar_defined v -> + if Option.default false (Store.get evi.evar_extra cleared) then + let (evk,_) = Term.destEvar v in + advance sigma evk + else + None + (** The following functions return the set of undefined evars contained in the object, the defined evars being traversed. This is roughly a combination of the previous functions and diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index f68651a74..b60daae6d 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -123,6 +123,12 @@ val evar_absorb_arguments : env -> evar_map -> existential -> constr list -> its (partial) definition. *) val gather_dependent_evars : evar_map -> evar list -> (Evar.Set.t option) Evar.Map.t +(** [advance sigma g] returns [Some g'] if [g'] is undefined and is + the current avatar of [g] (for instance [g] was changed by [clear] + into [g']). It returns [None] if [g] has been (partially) + solved. *) +val advance : evar_map -> evar -> evar option + (** The following functions return the set of undefined evars contained in the object, the defined evars being traversed. This is roughly a combination of the previous functions and diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 2e164e540..c4ea79f95 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -183,17 +183,24 @@ type inference_flags = { expand_evars : bool } -let frozen_holes (sigma, sigma') = - (); fun ev -> Evar.Map.mem ev (Evd.undefined_map sigma) - -let pending_holes (sigma, sigma') = - let fold evk _ accu = - if not (Evd.mem sigma evk) then Evar.Set.add evk accu else accu - in - Evd.fold_undefined fold sigma' Evar.Set.empty +(* Compute the set of still-undefined initial evars up to restriction + (e.g. clearing) and the set of yet-unsolved evars freshly created + in the extension [sigma'] of [sigma] (excluding the restrictions of + the undefined evars of [sigma] to be freshly created evars of + [sigma']). Otherwise said, we partition the undefined evars of + [sigma'] into those already in [sigma] or deriving from an evar in + [sigma] by restriction, and the evars properly created in [sigma'] *) + +let frozen_and_pending_holes (sigma, sigma') = + let add_derivative_of evk evi acc = + match advance sigma' evk with None -> acc | Some evk' -> Evar.Set.add evk' acc in + let frozen = Evd.fold_undefined add_derivative_of sigma Evar.Set.empty in + let fold evk _ accu = if not (Evar.Set.mem evk frozen) then Evar.Set.add evk accu else accu in + let pending = Evd.fold_undefined fold sigma' Evar.Set.empty in + (frozen,pending) let apply_typeclasses env evdref frozen fail_evar = - let filter_frozen = frozen in + let filter_frozen evk = Evar.Set.mem evk frozen in evdref := Typeclasses.resolve_typeclasses ~filter:(if Flags.is_program_mode () then (fun evk evi -> Typeclasses.no_goals_or_obligations evk evi && not (filter_frozen evk)) @@ -244,8 +251,7 @@ let check_evars_are_solved env current_sigma frozen pending = (* Try typeclasses, hooks, unification heuristics ... *) let solve_remaining_evars flags env current_sigma pending = - let frozen = frozen_holes pending in - let pending = pending_holes pending in + let frozen,pending = frozen_and_pending_holes pending in let evdref = ref current_sigma in if flags.use_typeclasses then apply_typeclasses env evdref frozen false; if Option.has_some flags.use_hook then @@ -255,8 +261,7 @@ let solve_remaining_evars flags env current_sigma pending = !evdref let check_evars_are_solved env current_sigma pending = - let frozen = frozen_holes pending in - let pending = pending_holes pending in + let frozen,pending = frozen_and_pending_holes pending in check_evars_are_solved env current_sigma frozen pending let process_inference_flags flags env initial_sigma (sigma,c) = diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 2fc404235..46a370d53 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -146,33 +146,9 @@ let focus i j sp = let (new_comb, context) = focus_sublist i j sp.comb in ( { sp with comb = new_comb } , context ) - -(** [advance sigma g] returns [Some g'] if [g'] is undefined and is - the current avatar of [g] (for instance [g] was changed by [clear] - into [g']). It returns [None] if [g] has been (partially) - solved. *) -(* spiwack: [advance] is probably performance critical, and the good - behaviour of its definition may depend sensitively to the actual - definition of [Evd.find]. Currently, [Evd.find] starts looking for - a value in the heap of undefined variable, which is small. Hence in - the most common case, where [advance] is applied to an unsolved - goal ([advance] is used to figure if a side effect has modified the - goal) it terminates quickly. *) -let rec advance sigma g = - let open Evd in - let evi = Evd.find sigma g in - match evi.evar_body with - | Evar_empty -> Some g - | Evar_defined v -> - if Option.default false (Store.get evi.evar_extra Evarutil.cleared) then - let (e,_) = Term.destEvar v in - advance sigma e - else - None - (** [undefined defs l] is the list of goals in [l] which are still unsolved (after advancing cleared goals). *) -let undefined defs l = CList.map_filter (advance defs) l +let undefined defs l = CList.map_filter (Evarutil.advance defs) l (** Unfocuses a proofview with respect to a context. *) let unfocus c sp = @@ -429,7 +405,7 @@ let iter_goal i = Comb.get >>= fun initial -> Proof.List.fold_left begin fun (subgoals as cur) goal -> Solution.get >>= fun step -> - match advance step goal with + match Evarutil.advance step goal with | None -> return cur | Some goal -> Comb.set [goal] >> @@ -453,7 +429,7 @@ let fold_left2_goal i s l = in Proof.List.fold_left2 err begin fun ((r,subgoals) as cur) goal a -> Solution.get >>= fun step -> - match advance step goal with + match Evarutil.advance step goal with | None -> return cur | Some goal -> Comb.set [goal] >> @@ -497,7 +473,7 @@ let tclDISPATCHGEN0 join tacs = let open Proof in Pv.get >>= function | { comb=[goal] ; solution } -> - begin match advance solution goal with + begin match Evarutil.advance solution goal with | None -> tclUNIT (join []) | Some _ -> Proof.map (fun res -> join [res]) tac end @@ -1012,7 +988,7 @@ module Goal = struct Pv.get >>= fun step -> let sigma = step.solution in let map goal = - match advance sigma goal with + match Evarutil.advance sigma goal with | None -> None (** ppedrot: Is this check really necessary? *) | Some goal -> let gl = @@ -1026,7 +1002,7 @@ module Goal = struct let unsolved { self=self } = tclEVARMAP >>= fun sigma -> - tclUNIT (not (Option.is_empty (advance sigma self))) + tclUNIT (not (Option.is_empty (Evarutil.advance sigma self))) (* compatibility *) let goal { self=self } = self diff --git a/test-suite/bugs/closed/5097.v b/test-suite/bugs/closed/5097.v new file mode 100644 index 000000000..37b239cf6 --- /dev/null +++ b/test-suite/bugs/closed/5097.v @@ -0,0 +1,7 @@ +(* Tracing existing evars along the weakening rule ("clear") *) +Goal forall y, exists x, x=0->x=y. +intros. +eexists ?[x]. +intros. +let x:=constr:(ltac:(clear y; exact 0)) in idtac x. +Abort. -- cgit v1.2.3 From 6d5fe92efbe3f6269666644a0f2e8e9aab8ab307 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 19 Oct 2016 10:08:49 +0200 Subject: Adding dependency of the test-suite subsystems in prerequisite (fixing #5150). --- test-suite/Makefile | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/test-suite/Makefile b/test-suite/Makefile index f1cb21ecd..8500ef1b3 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -221,7 +221,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v fi; \ } > "$@" -$(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.v +$(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.v prerequisite @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ opts="$(if $(findstring modules/,$<),-R modules Mods -impredicative-set)"; \ @@ -253,7 +253,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v fi; \ } > "$@" -$(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v +$(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v prerequisite @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ @@ -267,7 +267,7 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v fi; \ } > "$@" -$(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out +$(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out prerequisite @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ @@ -289,7 +289,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out rm $$tmpoutput; \ } > "$@" -$(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v +$(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v prerequisite @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ @@ -307,7 +307,7 @@ $(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v # the .v file with exactly two digits after the dot. The reference for # time is a 6120 bogomips cpu. ifneq (,$(bogomips)) -$(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v +$(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v prerequisite @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ @@ -338,7 +338,7 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v endif # Ideal-features tests -$(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v +$(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v prerequisite @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ -- cgit v1.2.3 From 6b02759513b1ccc7debe87ad9ae6bc6f1341ff6c Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 21 Oct 2016 11:29:05 +0200 Subject: Remove no longer exported debug printer --- dev/top_printers.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/dev/top_printers.ml b/dev/top_printers.ml index e34385e5c..a3d5cf5c1 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -215,7 +215,6 @@ let ppuniverse_subst l = pp (Univ.pr_universe_subst l) let ppuniverse_opt_subst l = pp (Universes.pr_universe_opt_subst l) let ppuniverse_level_subst l = pp (Univ.pr_universe_level_subst l) let ppevar_universe_context l = pp (Evd.pr_evar_universe_context l) -let ppconstraints_map c = pp (Universes.pr_constraints_map c) let ppconstraints c = pp (pr_constraints Level.pr c) let ppuniverseconstraints c = pp (Universes.Constraints.pr c) let ppuniverse_context_future c = -- cgit v1.2.3 From 5b0b6c92354c34a4f0d5551f88b16264fb08be5f Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 21 Oct 2016 10:49:15 +0200 Subject: Revert 214b9ab7969fae71dcf553c399cb1674e463d0e3 This makes [refine] typecheck the term only once (instead of twice), (Qed excluded of course). Fix test-suite file for output of constraints accordingly. --- ltac/extratactics.ml4 | 2 +- test-suite/output/unifconstraints.out | 26 ++++---------------------- 2 files changed, 5 insertions(+), 23 deletions(-) diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index db7318469..d0318fb5f 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -355,7 +355,7 @@ let refine_tac ist simple c = let expected_type = Pretyping.OfType concl in let c = Pretyping.type_uconstr ~flags ~expected_type ist c in let update = { run = fun sigma -> c.delayed env sigma } in - let refine = Refine.refine ~unsafe:false update in + let refine = Refine.refine ~unsafe:true update in if simple then refine else refine <*> Tactics.New.reduce_after_refine <*> diff --git a/test-suite/output/unifconstraints.out b/test-suite/output/unifconstraints.out index d152052ba..ae8460362 100644 --- a/test-suite/output/unifconstraints.out +++ b/test-suite/output/unifconstraints.out @@ -8,11 +8,7 @@ subgoal 2 is: forall n : nat, ?Goal n -> ?Goal (S n) subgoal 3 is: nat -unification constraints: - ?Goal ?Goal2 <= - True /\ True /\ True \/ - veeryyyyyyyyyyyyloooooooooooooonggidentifier = - veeryyyyyyyyyyyyloooooooooooooonggidentifier +unification constraint: ?Goal ?Goal2 <= True /\ True /\ True \/ veeryyyyyyyyyyyyloooooooooooooonggidentifier = @@ -28,11 +24,7 @@ subgoal 2 is: forall n0 : nat, ?Goal@{n:=n; m:=m} n0 -> ?Goal@{n:=n; m:=m} (S n0) subgoal 3 is: nat -unification constraints: - ?Goal@{n:=n; m:=m} ?Goal2@{n:=n; m:=m} <= - True /\ True /\ True \/ - veeryyyyyyyyyyyyloooooooooooooonggidentifier = - veeryyyyyyyyyyyyloooooooooooooonggidentifier +unification constraint: ?Goal@{n:=n; m:=m} ?Goal2@{n:=n; m:=m} <= True /\ True /\ True \/ veeryyyyyyyyyyyyloooooooooooooonggidentifier = @@ -48,12 +40,7 @@ subgoal 2 is: forall n0 : nat, ?Goal1@{m:=m} n0 -> ?Goal1@{m:=m} (S n0) subgoal 3 is: nat -unification constraints: - - n, m : nat |- ?Goal1@{m:=m} ?Goal0@{n:=n; m:=m} <= - True /\ True /\ True \/ - veeryyyyyyyyyyyyloooooooooooooonggidentifier = - veeryyyyyyyyyyyyloooooooooooooonggidentifier +unification constraint: n, m : nat |- ?Goal1@{m:=m} ?Goal0@{n:=n; m:=m} <= True /\ True /\ True \/ @@ -70,12 +57,7 @@ subgoal 2 is: forall n0 : nat, ?Goal0@{m:=m} n0 -> ?Goal0@{m:=m} (S n0) subgoal 3 is: nat -unification constraints: - - n, m : nat |- ?Goal0@{m:=m} ?Goal2@{n:=n} <= - True /\ True /\ True \/ - veeryyyyyyyyyyyyloooooooooooooonggidentifier = - veeryyyyyyyyyyyyloooooooooooooonggidentifier +unification constraint: n, m : nat |- ?Goal0@{m:=m} ?Goal2@{n:=n} <= True /\ True /\ True \/ -- cgit v1.2.3 From 5609da1e08f950fab85b87b257ed343b491f1ef5 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 21 Oct 2016 17:57:18 +0200 Subject: Revert "unification.ml: fix for bug #4763, unif regression" This reverts commit 0b417c12eb10bb29bcee04384b6c0855cb9de73a. A good fix requires to review a bit the design of unification constraint postponement, which we do in 8.6. We leave things as they are in 8.5 for compatibility. --- pretyping/evarsolve.ml | 2 -- pretyping/unification.ml | 3 ++- test-suite/bugs/closed/4763.v | 13 ------------- 3 files changed, 2 insertions(+), 16 deletions(-) delete mode 100644 test-suite/bugs/closed/4763.v diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 4a99246bb..d639208fb 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1588,8 +1588,6 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs = * ass. *) -(* This criterion relies on the fact that we postpone only problems of the form: -?x [?x1 ... ?xn] = t or the symmetric case. *) let status_changed lev (pbty,_,t1,t2) = (try Evar.Set.mem (head_evar t1) lev with NoHeadEvar -> false) || (try Evar.Set.mem (head_evar t2) lev with NoHeadEvar -> false) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index b7edd6fcd..9f8238513 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1244,7 +1244,8 @@ let solve_simple_evar_eqn ts env evd ev rhs = match solve_simple_eqn (Evarconv.evar_conv_x ts) env evd (None,ev,rhs) with | UnifFailure (evd,reason) -> error_cannot_unify env evd ~reason (mkEvar ev,rhs); - | Success evd -> evd + | Success evd -> + Evarconv.consider_remaining_unif_problems env evd (* [w_merge env sigma b metas evars] merges common instances in metas or in evars, possibly generating new unification problems; if [b] diff --git a/test-suite/bugs/closed/4763.v b/test-suite/bugs/closed/4763.v deleted file mode 100644 index ae8ed0e6e..000000000 --- a/test-suite/bugs/closed/4763.v +++ /dev/null @@ -1,13 +0,0 @@ -Require Import Coq.Arith.Arith Coq.Classes.Morphisms Coq.Classes.RelationClasses. -Coercion is_true : bool >-> Sortclass. -Global Instance: Transitive leb. -Admitted. - -Goal forall x y z, leb x y -> leb y z -> True. - intros ??? H H'. - lazymatch goal with - | [ H : is_true (?R ?x ?y), H' : is_true (?R ?y ?z) |- _ ] - => pose proof (transitivity H H' : is_true (R x z)) - end. - exact I. -Qed. \ No newline at end of file -- cgit v1.2.3 From cef86ed6f78e2efa703bd8772a43fbeba597bbe3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 20 Oct 2016 11:45:10 +0200 Subject: Adding a primitive to recover the set of keywords from the lexer. This is useful for debugging purposes. --- parsing/cLexer.ml4 | 11 +++++++++++ parsing/cLexer.mli | 1 + 2 files changed, 12 insertions(+) diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index 31025075c..8a8e41956 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -69,6 +69,15 @@ let ttree_remove ttree str = in remove ttree 0 +let ttree_elements ttree = + let rec elts tt accu = + let accu = match tt.node with + | None -> accu + | Some s -> CString.Set.add s accu + in + CharMap.fold (fun _ tt accu -> elts tt accu) tt.branch accu + in + elts ttree CString.Set.empty (* Errors occurring while lexing (explained as "Lexer error: ...") *) @@ -221,6 +230,8 @@ let add_keyword str = let remove_keyword str = token_tree := ttree_remove !token_tree str +let keywords () = ttree_elements !token_tree + (* Freeze and unfreeze the state of the lexer *) type frozen_t = ttree diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli index f69d95335..e0fdf8cb5 100644 --- a/parsing/cLexer.mli +++ b/parsing/cLexer.mli @@ -9,6 +9,7 @@ val add_keyword : string -> unit val remove_keyword : string -> unit val is_keyword : string -> bool +val keywords : unit -> CString.Set.t val check_ident : string -> unit val is_ident : string -> bool -- cgit v1.2.3 From 78eb89f254d699f1024573c39ad8ed5808245210 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 21 Oct 2016 18:25:58 +0200 Subject: Oops, my bad, didn't expect a merge issue! --- engine/proofview.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/engine/proofview.ml b/engine/proofview.ml index 208837f6a..855235d2b 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -941,7 +941,7 @@ module Unsafe = struct let mark_as_goal evd content = mark_in_evm ~goal:true evd content - let advance = advance + let advance = Evarutil.advance let mark_as_unresolvable p gl = { p with solution = mark_in_evm ~goal:false p.solution gl } -- cgit v1.2.3 From c28a2a3a1297098ee73ad5b26e714164b6167d2b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 21 Oct 2016 18:39:05 +0200 Subject: Adding a test for bug #3495. --- test-suite/bugs/closed/3495.v | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) create mode 100644 test-suite/bugs/closed/3495.v diff --git a/test-suite/bugs/closed/3495.v b/test-suite/bugs/closed/3495.v new file mode 100644 index 000000000..102a2aba0 --- /dev/null +++ b/test-suite/bugs/closed/3495.v @@ -0,0 +1,18 @@ +Require Import RelationClasses. + +Axiom R : Prop -> Prop -> Prop. +Declare Instance : Reflexive R. + +Class bar := { x : False }. +Record foo := { a : Prop ; b : bar }. + +Definition default_foo (a0 : Prop) `{b : bar} : foo := {| a := a0 ; b := b |}. + +Goal exists k, R k True. +Proof. +eexists. +evar (b : bar). +let e := match goal with |- R ?e _ => constr:(e) end in +unify e (a (default_foo True)). +subst b. +reflexivity. -- cgit v1.2.3 From 56744aadd413dd9417d245951083117b05170e14 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 22 Oct 2016 11:38:51 +0200 Subject: Fixing printing of generic arguments of tag "var". --- tactics/tacinterp.ml | 3 +++ test-suite/output/ltac.out | 1 + test-suite/output/ltac.v | 5 +++++ 3 files changed, 9 insertions(+) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 5ecc46d67..c3f7fa143 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -816,6 +816,9 @@ let rec message_of_value v = Ftactic.return (pr_closed_glob_env (pf_env gl) (Proofview.Goal.sigma gl) c) end + else if has_type v (topwit wit_var) then + let id = out_gen (topwit wit_var) v in + Ftactic.nf_enter begin fun gl -> Ftactic.return (pr_id id) end else match Value.to_list v with | Some l -> Ftactic.List.map message_of_value l >>= fun l -> diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out index d003c70df..266e4c724 100644 --- a/test-suite/output/ltac.out +++ b/test-suite/output/ltac.out @@ -1,2 +1,3 @@ The command has indeed failed with message: Error: Ltac variable y depends on pattern variable name z which is not bound in current context. +Hx diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v index 7e2610c7d..e5bcff8dd 100644 --- a/test-suite/output/ltac.v +++ b/test-suite/output/ltac.v @@ -15,3 +15,8 @@ lazymatch goal with | H1 : HT |- _ => idtac end. Abort. + +(* Check printing of the "var" argument "Hx" *) +Ltac m H := idtac H; exact H. +Goal True. +let a:=constr:(let Hx := 0 in ltac:(m Hx)) in idtac. -- cgit v1.2.3 From 9f8714f4cd3fb59ce38afee48caf081db1919c0c Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 5 Oct 2016 08:22:57 +0200 Subject: Fix incorrect token description for bullets. --- parsing/tok.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/parsing/tok.ml b/parsing/tok.ml index c96b53de4..25633c63d 100644 --- a/parsing/tok.ml +++ b/parsing/tok.ml @@ -55,7 +55,7 @@ let to_string = function | INT s -> Format.sprintf "INT %s" s | STRING s -> Format.sprintf "STRING %S" s | LEFTQMARK -> "LEFTQMARK" - | BULLET s -> Format.sprintf "STRING %S" s + | BULLET s -> Format.sprintf "BULLET %S" s | EOI -> "EOI" let match_keyword kwd = function -- cgit v1.2.3 From cc2778c3310a75585c00f0eb659ddde7aee2944a Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 28 Sep 2016 17:00:09 +0200 Subject: Do not stop propagation of signals when Coq is busy (bug #3941). When inserting a character in an already processed buffer, a message is sent to Coq so that the proof is backtracked and the character is inserted. If a second character is inserted while Coq is still busy with the first message, the action is canceled, but the signal is no longer dropped so that the second character is properly inserted. --- ide/session.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/ide/session.ml b/ide/session.ml index 168ddd4df..711111139 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -111,10 +111,10 @@ let set_buffer_handlers let id = ref 0 in fun () -> incr id; !id in let running_action = ref None in - let cancel_signal reason = + let cancel_signal ?(stop_emit=true) reason = Minilib.log ("user_action cancelled: "^reason); action_was_cancelled := true; - GtkSignal.stop_emit () in + if stop_emit then GtkSignal.stop_emit () in let del_mark () = try buffer#delete_mark (`NAME "target") with GText.No_such_mark _ -> () in @@ -127,7 +127,7 @@ let set_buffer_handlers fun () -> (* If Coq is busy due to the current action, we don't cancel *) match !running_action with | Some aid when aid = action -> () - | _ -> cancel_signal "Coq busy" in + | _ -> cancel_signal ~stop_emit:false "Coq busy" in Coq.try_grab coqtop action fallback in let get_start () = buffer#get_iter_at_mark (`NAME "start_of_input") in let get_stop () = buffer#get_iter_at_mark (`NAME "stop_of_input") in -- cgit v1.2.3 From 80d5779409bf33fbe5043275b96775a5f04a3b2c Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 28 Sep 2016 15:38:33 +0200 Subject: Remove incorrect assertion in cbn (bug #4822). This assertion checked that two arguments in the same position were equal, but in fact, since one might have already been reduced, they are only convertible (which is too costly to check in an assertion). --- pretyping/reductionops.ml | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 7c7b31395..9e654d29a 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -153,9 +153,6 @@ module Cst_stack = struct let empty = [] let is_empty = CList.is_empty - let sanity x y = - assert(Term.eq_constr x y) - let drop_useless = function | _ :: ((_,_,[])::_ as q) -> q | l -> l @@ -164,9 +161,9 @@ module Cst_stack = struct let append2cst = function | (c,params,[]) -> (c, h::params, []) | (c,params,((i,t)::q)) when i = pred (Array.length t) -> - let () = sanity h t.(i) in (c, params, q) + (c, params, q) | (c,params,(i,t)::q) -> - let () = sanity h t.(i) in (c, params, (succ i,t)::q) + (c, params, (succ i,t)::q) in drop_useless (List.map append2cst cst_l) -- cgit v1.2.3 From 1d769e02b3baba54246c942fe116abaf850892db Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 24 Oct 2016 11:44:24 +0200 Subject: Fix 6d5fe92e to #5150 (missing dependencies in test suite) was a bit too strong. New fix. A bit less consistent with the spirit of this Makefile as we list prerequisite files explicitly, but avoid to redo subsystems at each call to "make" as with previous fix. Other solutions from experts are welcome. --- test-suite/Makefile | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/test-suite/Makefile b/test-suite/Makefile index 8500ef1b3..491b16960 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -84,6 +84,9 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \ # All subsystems SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk +PREREQUISITELOG = prerequisite/admit.v.log \ + prerequisite/make_local.v.log prerequisite/make_notation.v.log + ####################################################################### # Phony targets ####################################################################### @@ -221,7 +224,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v fi; \ } > "$@" -$(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.v prerequisite +$(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ opts="$(if $(findstring modules/,$<),-R modules Mods -impredicative-set)"; \ @@ -253,7 +256,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v fi; \ } > "$@" -$(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v prerequisite +$(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ @@ -267,7 +270,7 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v prerequisite fi; \ } > "$@" -$(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out prerequisite +$(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ @@ -289,7 +292,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out prerequisite rm $$tmpoutput; \ } > "$@" -$(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v prerequisite +$(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ @@ -307,7 +310,7 @@ $(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v prerequisite # the .v file with exactly two digits after the dot. The reference for # time is a 6120 bogomips cpu. ifneq (,$(bogomips)) -$(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v prerequisite +$(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ @@ -338,7 +341,7 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v prerequisite endif # Ideal-features tests -$(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v prerequisite +$(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ -- cgit v1.2.3 From 81bdc22146d51f0131bffc12d4668f3902982f33 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 29 Sep 2016 14:34:41 -0400 Subject: Update .gitignore with new names for psatz caches --- .gitignore | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/.gitignore b/.gitignore index 4acd9930e..bea12162c 100644 --- a/.gitignore +++ b/.gitignore @@ -52,9 +52,9 @@ dev/ocamldebug-coq plugins/micromega/csdpcert kernel/byterun/dllcoqrun.so coqdoc.sty -csdp.cache -test-suite/lia.cache -test-suite/nra.cache +.csdp.cache +test-suite/.lia.cache +test-suite/.nra.cache test-suite/trace test-suite/misc/universes/all_stdlib.v test-suite/misc/universes/universes.txt @@ -68,7 +68,7 @@ doc/faq/axioms.eps_t doc/faq/axioms.pdf doc/faq/axioms.pdf_t doc/faq/axioms.png -doc/refman/csdp.cache +doc/refman/.csdp.cache doc/refman/trace doc/refman/Reference-Manual.pdf doc/refman/Reference-Manual.ps @@ -135,7 +135,7 @@ kernel/copcodes.ml tools/tolink.ml theories/Numbers/Natural/BigN/NMake_gen.v ide/index_urls.txt -lia.cache +.lia.cache checker/names.ml checker/names.mli checker/esubst.ml -- cgit v1.2.3 From 5f1dd4c401110d6b10350c847805c6923fa09de5 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 24 Oct 2016 17:04:41 +0200 Subject: Fixing #3479 (parsing of "{" and "}" when a keyword starts with "{" or "}"). --- parsing/lexer.ml4 | 6 ++++++ test-suite/success/Notations.v | 6 ++++++ 2 files changed, 12 insertions(+) diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 5d96873f3..db6816a70 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -535,6 +535,12 @@ let rec next_token = parser bp next_token s | [< t = process_chars bp c >] -> comment_stop bp; t >] -> t + | [< ' ('{' | '}' as c); s >] ep -> + let t,new_between_com = + if !between_com then (KEYWORD (String.make 1 c), (bp, ep)), true + else process_chars bp c s,false + in + comment_stop bp; between_com := new_between_com; t | [< s >] -> match lookup_utf8 s with | Utf8Token (Unicode.Letter, n) -> diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index 2f7c62972..511b60b4b 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -110,3 +110,9 @@ Goal True -> True. intros H. exact H. Qed. (* Check absence of collision on ".." in nested notations with ".." *) Notation "[ a , .. , b ]" := (a, (.. (b,tt) ..)). + +(* Check parsing of { and } is not affected by notations #3479 *) +Notation " |- {{ a }} b" := (a=b) (no associativity, at level 10). +Goal True. +{{ exact I. }} +Qed. -- cgit v1.2.3 From 0be88deef5e9ace1323cf8adc474bf2e4ada9153 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 24 Oct 2016 17:16:00 +0200 Subject: Fixing a location bug with "?" and "$". --- parsing/lexer.ml4 | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index db6816a70..cfea8793a 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -495,7 +495,7 @@ let rec next_token = parser bp | [< '' ' | '\t' | '\n' |'\r' as c; s >] -> comm_loc bp; push_char c; next_token s | [< ''$' as c; t = parse_after_special c bp >] ep -> - comment_stop bp; (t, (ep, bp)) + comment_stop bp; (t, (bp, ep)) | [< ''.' as c; t = parse_after_special c bp; s >] ep -> comment_stop bp; (* We enforce that "." should either be part of a larger keyword, @@ -514,7 +514,7 @@ let rec next_token = parser bp in comment_stop bp; between_com := new_between_com; t | [< ''?'; s >] ep -> - let t = parse_after_qmark bp s in comment_stop bp; (t, (ep, bp)) + let t = parse_after_qmark bp s in comment_stop bp; (t, (bp, ep)) | [< ' ('a'..'z' | 'A'..'Z' | '_' as c); len = ident_tail (store 0 c); s >] ep -> let id = get_buff len in -- cgit v1.2.3 From 71f69e26b595c2a403184cf805afaf9d46f8a0b3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 24 Oct 2016 15:01:43 +0200 Subject: ssrmatching: fix interpretation of rpattern --- plugins/ssrmatching/ssrmatching.ml4 | 78 ++++++++++++++++++------------------- 1 file changed, 39 insertions(+), 39 deletions(-) diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index a34fa4cae..41eb5826b 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -908,9 +908,47 @@ let glob_ssrterm gs = function fst x, Some c | ct -> ct +(* This piece of code asserts the following notations are reserved *) +(* Reserved Notation "( a 'in' b )" (at level 0). *) +(* Reserved Notation "( a 'as' b )" (at level 0). *) +(* Reserved Notation "( a 'in' b 'in' c )" (at level 0). *) +(* Reserved Notation "( a 'as' b 'in' c )" (at level 0). *) +let glob_cpattern gs p = + pp(lazy(str"globbing pattern: " ++ pr_term p)); + let glob x = snd (glob_ssrterm gs (mk_lterm x)) in + let encode k s l = + let name = Name (id_of_string ("_ssrpat_" ^ s)) in + k, (mkRCast mkRHole (mkRLambda name mkRHole (mkRApp mkRHole l)), None) in + let bind_in t1 t2 = + let d = dummy_loc in let n = Name (destCVar t1) in + fst (glob (mkCCast d (mkCHole d) (mkCLambda d n (mkCHole d) t2))) in + let check_var t2 = if not (isCVar t2) then + loc_error (constr_loc t2) "Only identifiers are allowed here" in + match p with + | _, (_, None) as x -> x + | k, (v, Some t) as orig -> + if k = 'x' then glob_ssrterm gs ('(', (v, Some t)) else + match t with + | CNotation(_, "( _ in _ )", ([t1; t2], [], [])) -> + (try match glob t1, glob t2 with + | (r1, None), (r2, None) -> encode k "In" [r1;r2] + | (r1, Some _), (r2, Some _) when isCVar t1 -> + encode k "In" [r1; r2; bind_in t1 t2] + | (r1, Some _), (r2, Some _) -> encode k "In" [r1; r2] + | _ -> CErrors.anomaly (str"where are we?") + with _ when isCVar t1 -> encode k "In" [bind_in t1 t2]) + | CNotation(_, "( _ in _ in _ )", ([t1; t2; t3], [], [])) -> + check_var t2; encode k "In" [fst (glob t1); bind_in t2 t3] + | CNotation(_, "( _ as _ )", ([t1; t2], [], [])) -> + encode k "As" [fst (glob t1); fst (glob t2)] + | CNotation(_, "( _ as _ in _ )", ([t1; t2; t3], [], [])) -> + check_var t2; encode k "As" [fst (glob t1); bind_in t2 t3] + | _ -> glob_ssrterm gs orig +;; + let glob_rpattern s p = match p with - | T t -> T (glob_ssrterm s t) + | T t -> T (glob_cpattern s t) | In_T t -> In_T (glob_ssrterm s t) | X_In_T(x,t) -> X_In_T (x,glob_ssrterm s t) | In_X_In_T(x,t) -> In_X_In_T (x,glob_ssrterm s t) @@ -995,44 +1033,6 @@ let input_ssrtermkind strm = match Compat.get_tok (stream_nth 0 strm) with | _ -> ' ' let ssrtermkind = Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind -(* This piece of code asserts the following notations are reserved *) -(* Reserved Notation "( a 'in' b )" (at level 0). *) -(* Reserved Notation "( a 'as' b )" (at level 0). *) -(* Reserved Notation "( a 'in' b 'in' c )" (at level 0). *) -(* Reserved Notation "( a 'as' b 'in' c )" (at level 0). *) -let glob_cpattern gs p = - pp(lazy(str"globbing pattern: " ++ pr_term p)); - let glob x = snd (glob_ssrterm gs (mk_lterm x)) in - let encode k s l = - let name = Name (id_of_string ("_ssrpat_" ^ s)) in - k, (mkRCast mkRHole (mkRLambda name mkRHole (mkRApp mkRHole l)), None) in - let bind_in t1 t2 = - let d = dummy_loc in let n = Name (destCVar t1) in - fst (glob (mkCCast d (mkCHole d) (mkCLambda d n (mkCHole d) t2))) in - let check_var t2 = if not (isCVar t2) then - loc_error (constr_loc t2) "Only identifiers are allowed here" in - match p with - | _, (_, None) as x -> x - | k, (v, Some t) as orig -> - if k = 'x' then glob_ssrterm gs ('(', (v, Some t)) else - match t with - | CNotation(_, "( _ in _ )", ([t1; t2], [], [])) -> - (try match glob t1, glob t2 with - | (r1, None), (r2, None) -> encode k "In" [r1;r2] - | (r1, Some _), (r2, Some _) when isCVar t1 -> - encode k "In" [r1; r2; bind_in t1 t2] - | (r1, Some _), (r2, Some _) -> encode k "In" [r1; r2] - | _ -> CErrors.anomaly (str"where are we?") - with _ when isCVar t1 -> encode k "In" [bind_in t1 t2]) - | CNotation(_, "( _ in _ in _ )", ([t1; t2; t3], [], [])) -> - check_var t2; encode k "In" [fst (glob t1); bind_in t2 t3] - | CNotation(_, "( _ as _ )", ([t1; t2], [], [])) -> - encode k "As" [fst (glob t1); fst (glob t2)] - | CNotation(_, "( _ as _ in _ )", ([t1; t2; t3], [], [])) -> - check_var t2; encode k "As" [fst (glob t1); bind_in t2 t3] - | _ -> glob_ssrterm gs orig -;; - let interp_ssrterm _ gl t = Tacmach.project gl, t ARGUMENT EXTEND cpattern -- cgit v1.2.3 From 166634c57bbad2e727364a97bf30bc3d67d2f2a8 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 24 Oct 2016 17:36:32 +0200 Subject: Merge branch 'v8.5' into v8.6 + a few improvements on 5f1dd4c40 (lexing of { and }). --- parsing/cLexer.ml4 | 12 ++++++++---- test-suite/Makefile | 15 +++++++++------ test-suite/success/Notations.v | 7 +++++++ 3 files changed, 24 insertions(+), 10 deletions(-) diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index 8a8e41956..79771f3f6 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -573,7 +573,7 @@ let rec next_token loc = parser bp comment_stop bp; between_commands := new_between_commands; t | [< ''?'; s >] ep -> let t = parse_after_qmark loc bp s in - comment_stop bp; (t, set_loc_pos loc ep bp) + comment_stop bp; (t, set_loc_pos loc bp ep) | [< ' ('a'..'z' | 'A'..'Z' | '_' as c); len = ident_tail loc (store 0 c); s >] ep -> let id = get_buff len in @@ -593,6 +593,12 @@ let rec next_token loc = parser bp let loc = comment loc bp s in next_token loc s | [< t = process_chars loc bp c >] -> comment_stop bp; t >] -> t + | [< ' ('{' | '}' as c); s >] ep -> + let t,new_between_commands = + if !between_commands then (KEYWORD (String.make 1 c), set_loc_pos loc bp ep), true + else process_chars loc bp c s, false + in + comment_stop bp; between_commands := new_between_commands; t | [< s >] -> match lookup_utf8 loc s with | Utf8Token (Unicode.Letter, n) -> @@ -603,9 +609,7 @@ let rec next_token loc = parser bp (try find_keyword loc id s with Not_found -> IDENT id), set_loc_pos loc bp ep | AsciiChar | Utf8Token ((Unicode.Symbol | Unicode.IdentPart | Unicode.Unknown), _) -> let t = process_chars loc bp (Stream.next s) s in - let new_between_commands = match t with - (KEYWORD ("{"|"}"),_) -> !between_commands | _ -> false in - comment_stop bp; between_commands := new_between_commands; t + comment_stop bp; t | EmptyStream -> comment_stop bp; (EOI, set_loc_pos loc bp (bp+1)) diff --git a/test-suite/Makefile b/test-suite/Makefile index 10eb2df39..6a18c45df 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -88,6 +88,9 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \ # All subsystems SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk +PREREQUISITELOG = prerequisite/admit.v.log \ + prerequisite/make_local.v.log prerequisite/make_notation.v.log + ####################################################################### # Phony targets ####################################################################### @@ -226,7 +229,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v fi; \ } > "$@" -$(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.v prerequisite +$(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ opts="$(if $(findstring modules/,$<),-R modules Mods -impredicative-set)"; \ @@ -257,7 +260,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v fi; \ } > "$@" -$(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v prerequisite +$(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ @@ -271,7 +274,7 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v prerequisite fi; \ } > "$@" -$(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out prerequisite +$(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ @@ -330,7 +333,7 @@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out rm $$tmpexpected; \ } > "$@" -$(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v prerequisite +$(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ @@ -348,7 +351,7 @@ $(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v prerequisite # the .v file with exactly two digits after the dot. The reference for # time is a 6120 bogomips cpu. ifneq (,$(bogomips)) -$(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v prerequisite +$(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ @@ -379,7 +382,7 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v prerequisite endif # Ideal-features tests -$(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v prerequisite +$(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index 30abd961b..666c91257 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -115,3 +115,10 @@ Notation "[ a , .. , b ]" := (a, (.. (b,tt) ..)). Require Import Coq.Vectors.VectorDef. Import VectorNotations. Goal True. idtac; []. (* important for test: no space here *) constructor. Qed. + +(* Check parsing of { and } is not affected by notations #3479 *) +Notation " |- {{ a }} b" := (a=b) (no associativity, at level 10). +Goal True. +{{ exact I. }} +Qed. +Check |- {{ 0 }} 0. -- cgit v1.2.3 From 7f69f6d94b751464aae3c852f0bc53d5854f30a4 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 24 Oct 2016 18:36:26 +0200 Subject: Rename lia.cache into .lia.cache in the test-suite Makefile. --- test-suite/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test-suite/Makefile b/test-suite/Makefile index 6a18c45df..c10cd4ed4 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -105,7 +105,7 @@ run: $(SUBSYSTEMS) bugs: $(BUGS) clean: - rm -f trace lia.cache + rm -f trace .lia.cache $(SHOW) "RM <**/*.stamp> <**/*.vo> <**/*.vio> <**/*.log>" $(HIDE)find . \( \ -name '*.stamp' -o -name '*.vo' -o -name '*.vio' -o -name '*.log' \ -- cgit v1.2.3 From 810077167cd6f5077abe7b79b12ae9b51eae1b62 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 24 Oct 2016 22:44:34 +0200 Subject: Adding a test for #4398 (interpretation scopes for "match goal"). --- test-suite/output/ltac.out | 4 ++++ test-suite/output/ltac.v | 9 +++++++++ 2 files changed, 13 insertions(+) diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out index a62f4312e..a7bde5ea3 100644 --- a/test-suite/output/ltac.out +++ b/test-suite/output/ltac.out @@ -27,3 +27,7 @@ In nested Ltac calls to "h" and "injection (destruction_arg)", last call failed. Error: No primitive equality found. Hx +nat +nat +0 +0 diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v index fb1dab799..76c37625a 100644 --- a/test-suite/output/ltac.v +++ b/test-suite/output/ltac.v @@ -48,3 +48,12 @@ Fail h H. Ltac m H := idtac H; exact H. Goal True. let a:=constr:(let Hx := 0 in ltac:(m Hx)) in idtac. + +(* Check consistency of interpretation scopes (#4398) *) + +Goal nat*(0*0=0) -> nat*(0*0=0). intro. +match goal with H: ?x*?y |- _ => idtac x end. +match goal with |- ?x*?y => idtac x end. +match goal with H: context [?x*?y] |- _ => idtac x end. +match goal with |- context [?x*?y] => idtac x end. +Abort. -- cgit v1.2.3