diff options
63 files changed, 1850 insertions, 423 deletions
diff --git a/.gitignore b/.gitignore index 1cbf56e3cb..56e1905981 100644 --- a/.gitignore +++ b/.gitignore @@ -127,6 +127,7 @@ parsing/cLexer.ml ltac/coretactics.ml ltac/extratactics.ml ltac/extraargs.ml +ltac/profile_ltac_tactics.ml ide/coqide_main.ml # other auto-generated files @@ -137,6 +138,10 @@ tools/tolink.ml theories/Numbers/Natural/BigN/NMake_gen.v ide/index_urls.txt lia.cache +checker/names.ml +checker/names.mli +checker/esubst.ml +checker/esubst.mli # mlis documentation @@ -36,8 +36,12 @@ Changes from V8.5pl1 to V8.5pl2 Bugfixes -- #4677: fix alpha-conversion in notations needing eta-expansion +- #4677: fix alpha-conversion in notations needing eta-expansion. - Fully preserve initial order of hypotheses in "Regular Subst Tactic" mode. +- #4644: a regression in unification. +- #4777: printing inefficiency with implicit arguments +- #4752: CoqIDE crash on files not ended by ".v". +- #4398: type_scope used consistently in "match goal". Changes from V8.5 to V8.5pl1 ============================ diff --git a/checker/esubst.ml b/checker/esubst.ml deleted file mode 120000 index b82bd24f1e..0000000000 --- a/checker/esubst.ml +++ /dev/null @@ -1 +0,0 @@ -../kernel/esubst.ml
\ No newline at end of file diff --git a/checker/esubst.mli b/checker/esubst.mli deleted file mode 120000 index e30eaae5d3..0000000000 --- a/checker/esubst.mli +++ /dev/null @@ -1 +0,0 @@ -../kernel/esubst.mli
\ No newline at end of file diff --git a/checker/names.ml b/checker/names.ml deleted file mode 120000 index f0bf2f83f6..0000000000 --- a/checker/names.ml +++ /dev/null @@ -1 +0,0 @@ -../kernel/names.ml
\ No newline at end of file diff --git a/checker/names.mli b/checker/names.mli deleted file mode 120000 index 10459f3b29..0000000000 --- a/checker/names.mli +++ /dev/null @@ -1 +0,0 @@ -../kernel/names.mli
\ No newline at end of file diff --git a/configure.ml b/configure.ml index f2f2390750..71502058fe 100644 --- a/configure.ml +++ b/configure.ml @@ -1061,6 +1061,16 @@ let write_configml f = let _ = write_configml "config/coq_config.ml" +(** * Symlinks or copies for the checker *) + +let _ = + let prog, args, prf = + if arch = "win32" then "cp", [], "" + else "ln", ["-s"], "../" in + List.iter (fun file -> + ignore(run "rm" ["-f"; "checker/"^file]); + ignore(run ~fatal:true prog (args @ [prf^"kernel/"^file;"checker/"^file]))) + [ "esubst.ml"; "esubst.mli"; "names.ml"; "names.mli" ] (** * Build the config/Makefile file *) diff --git a/doc/refman/AsyncProofs.tex b/doc/refman/AsyncProofs.tex index 7cf5004003..7ffe252253 100644 --- a/doc/refman/AsyncProofs.tex +++ b/doc/refman/AsyncProofs.tex @@ -46,6 +46,43 @@ proof does not begin with \texttt{Proof using}, the system records in an auxiliary file, produced along with the \texttt{.vo} file, the list of section variables used. +\section{Proof blocks and error resilience} + +Coq 8.6 introduces a mechanism for error resiliency: in interactive mode Coq +is able to completely check a document containing errors instead of bailing +out at the first failure. + +Two kind of errors are supported: errors occurring in vernacular commands and +errors occurring in proofs. + +To properly recover from a failing tactic, Coq needs to recognize the structure of +the proof in order to confine the error to a sub proof. Proof block detection +is performed by looking at the syntax of the proof script (i.e. also looking at indentation). +Coq comes with four kind of proof blocks, and an ML API to add new ones. + +\begin{description} +\item[curly] blocks are delimited by \texttt{\{} and \texttt{\}}, see \ref{Proof-handling} +\item[par] blocks are atomic, i.e. just one tactic introduced by the \texttt{par:} goal selector +\item[indent] blocks end with a tactic indented less than the previous one +\item[bullet] blocks are delimited by two equal bullet signs at the same indentation level +\end{description} + +\subsection{Caveats} + +When a vernacular command fails the subsequent error messages may be bogus, i.e. caused by +the first error. Error resiliency for vernacular commands can be switched off passing +\texttt{-async-proofs-command-error-resilience off} to CoqIDE. + +An incorrect proof block detection can result into an incorrect error recovery and +hence in bogus errors. Proof block detection cannot be precise for bullets or +any other non well parenthesized proof structure. Error resiliency can be +turned off or selectively activated for any set of block kind passing to +CoqIDE one of the following options: +\texttt{-async-proofs-tactic-error-resilience off}, +\texttt{-async-proofs-tactic-error-resilience all}, +\texttt{-async-proofs-tactic-error-resilience $blocktype_1$,..., $blocktype_n$}. +Valid proof block types are: ``curly'', ``par'', ``indent'', ``bullet''. + \subsubsection{Automatic suggestion of proof annotations} The command \texttt{Set Suggest Proof Using} makes Coq suggest, when a @@ -85,6 +122,9 @@ reduce the reactivity of the master process to user commands. To disable this feature, one can pass the \texttt{-async-proofs off} flag to CoqIDE. +Proofs that are known to take little time to process are not delegated to a +worker process. The threshold can be configure with \texttt{-async-proofs-delegation-threshold}. Default is 0.03 seconds. + \section{Batch mode} When Coq is used as a batch compiler by running \texttt{coqc} or diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 12dea9a306..ffcb371346 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -78,7 +78,7 @@ For instance {\tt try repeat \tac$_1$ || \tac$_2$;\tac$_3$;[\tac$_{31}$|\dots|\tac$_{3n}$];\tac$_4$.} \end{quote} -is understood as +is understood as \begin{quote} {\tt (try (repeat (\tac$_1$ || \tac$_2$)));} \\ {\tt ((\tac$_3$;[\tac$_{31}$|\dots|\tac$_{3n}$]);\tac$_4$).} @@ -174,7 +174,7 @@ is understood as \\ {\messagetoken}\!\!\!\!\!\! & ::= & {\qstring} ~|~ {\ident} ~|~ {\integer} \\ \\ -\tacarg & ::= & +\tacarg & ::= & {\qualid}\\ & $|$ & {\tt ()} \\ & $|$ & {\tt ltac :} {\atom}\\ @@ -344,7 +344,7 @@ for $=1,...,n$. It fails if the number of focused goals is not exactly $n$. expects multiple goals, such as {\tt swap}, would act as if a single goal is focused. - \item {\tacexpr} {\tt ; [ } {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]} + \item {\tacexpr} {\tt ; [ } {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]} This variant of local tactic application is paired with a sequence. In this variant, $n$ must be the number of goals @@ -782,7 +782,7 @@ setting option {\tt Printing All}, see Section~\ref{SetPrintingAll}). \begin{coq_example} Ltac f x := match x with - context f [S ?X] => + context f [S ?X] => idtac X; (* To display the evaluation order *) assert (p := eq_refl 1 : X=1); (* To filter the case X=1 *) let x:= context f[O] in assert (x=O) (* To observe the context *) @@ -1026,7 +1026,7 @@ Reset Initial. \index{Tacticals!abstract@{\tt abstract}}} From the outside ``\texttt{abstract \tacexpr}'' is the same as -{\tt solve \tacexpr}. Internally it saves an auxiliary lemma called +{\tt solve \tacexpr}. Internally it saves an auxiliary lemma called {\ident}\texttt{\_subproof}\textit{n} where {\ident} is the name of the current goal and \textit{n} is chosen so that this is a fresh name. Such auxiliary lemma is inlined in the final proof term @@ -1196,6 +1196,86 @@ s: & continue current evaluation without stopping\\ r $n$: & advance $n$ steps further\\ r {\qstring}: & advance up to the next call to ``{\tt idtac} {\qstring}''\\ \end{tabular} + +\subsection[Profiling {\ltac} tactics]{Profiling {\ltac} tactics\optindex{Ltac Profiling}\comindex{Show Ltac Profile}\comindex{Reset Ltac Profile}} + +It is possible to measure the time spent in invocations of primitive tactics as well as tactics defined in {\ltac} and their inner invocations. The primary use is the development of complex tactics, which can sometimes be so slow as to impede interactive usage. The reasons for the performence degradation can be intricate, like a slowly performing {\ltac} match or a sub-tactic whose performance only degrades in certain situations. The profiler generates a call tree and indicates the time spent in a tactic depending its calling context. Thus it allows to locate the part of a tactic definition that contains the performance bug. + +\begin{quote} +{\tt Set Ltac Profiling}. +\end{quote} +Enables the profiler + +\begin{quote} +{\tt Unset Ltac Profiling}. +\end{quote} +Disables the profiler + +\begin{quote} +{\tt Show Ltac Profile}. +\end{quote} +Prints the profile + +\begin{quote} +{\tt Show Ltac Profile} {\qstring}. +\end{quote} +Prints a profile for all tactics that start with {\qstring}. Append a period (.) to the string if you only want exactly that name. + +\begin{quote} +{\tt Reset Profile}. +\end{quote} +Resets the profile, that is, deletes all accumulated information + +\begin{coq_eval} +Reset Initial. +\end{coq_eval} +\begin{coq_example*} +Require Import Coq.omega.Omega. + +Ltac mytauto := tauto. +Ltac tac := intros; repeat split; omega || mytauto. + +Notation max x y := (x + (y - x)) (only parsing). +\end{coq_example*} +\begin{coq_example*} +Goal forall x y z A B C D E F G H I J K L M N O P Q R S T U V W X Y Z, + max x (max y z) = max (max x y) z /\ max x (max y z) = max (max x y) z + /\ (A /\ B /\ C /\ D /\ E /\ F /\ G /\ H /\ I /\ J /\ K /\ L /\ M /\ N /\ O /\ P /\ Q /\ R /\ S /\ T /\ U /\ V /\ W /\ X /\ Y /\ Z + -> Z /\ Y /\ X /\ W /\ V /\ U /\ T /\ S /\ R /\ Q /\ P /\ O /\ N /\ M /\ L /\ K /\ J /\ I /\ H /\ G /\ F /\ E /\ D /\ C /\ B /\ A). +Proof. +\end{coq_example*} +\begin{coq_example} + Set Ltac Profiling. + tac. +\end{coq_example} +{\let\textit\texttt% use tt mode for the output of ltacprof +\begin{coq_example} + Show Ltac Profile. +\end{coq_example} +\begin{coq_example} + Show Ltac Profile "omega". +\end{coq_example} +} +\begin{coq_example*} +Abort. +Unset Ltac Profiling. +\end{coq_example*} + +\tacindex{start ltac profiling}\tacindex{stop ltac profiling} +The following two tactics behave like {\tt idtac} but enable and disable the profiling. They allow you to exclude parts of a proof script from profiling. + +\begin{quote} +{\tt start ltac profiling}. +\end{quote} + +\begin{quote} +{\tt stop ltac profiling}. +\end{quote} + +You can also pass the {\tt -profile-ltac} command line option to {\tt coqc}, which performs a {\tt Set Ltac Profiling} at the beginning of each document, and a {\tt Show Ltac Profile} at the end. + +Note that the profiler currently does not handle backtracking into multi-success tactics, and issues a warning to this effect in many cases when such backtracking occurs. + \endinput \subsection{Permutation on closed lists} @@ -1229,7 +1309,7 @@ Another more complex example is the problem of permutation on closed lists. The aim is to show that a closed list is a permutation of another one. First, we define the permutation predicate as shown on Figure~\ref{permutpred}. - + \begin{figure}[p] \begin{center} \fbox{\begin{minipage}{0.95\textwidth} @@ -1555,7 +1635,7 @@ Figure~\ref{isoslem} gives examples of what can be solved by {\tt IsoProve}. \begin{center} \fbox{\begin{minipage}{0.95\textwidth} \begin{coq_example*} -Lemma isos_ex1 : +Lemma isos_ex1 : forall A B:Set, A * unit * B = B * (unit * A). Proof. intros; IsoProve. @@ -1575,7 +1655,7 @@ Qed. \label{isoslem} \end{figure} -%%% Local Variables: +%%% Local Variables: %%% mode: latex %%% TeX-master: "Reference-Manual" -%%% End: +%%% End: diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex index a08cd1475a..36518e6fae 100644 --- a/doc/refman/Universes.tex +++ b/doc/refman/Universes.tex @@ -201,7 +201,8 @@ universes and explicitly instantiate polymorphic definitions. In the monorphic case, this command declares a new global universe named {\ident}. It supports the polymorphic flag only in sections, meaning the universe quantification will be discharged on each section definition -independently. +independently. One cannot mix polymorphic and monomorphic declarations +in the same section. \subsection{\tt Constraint {\ident} {\textit{ord}} {\ident}. \comindex{Constraint} @@ -212,6 +213,7 @@ The order relation can be one of $<$, $\le$ or $=$. If consistent, the constraint is then enforced in the global environment. Like \texttt{Universe}, it can be used with the \texttt{Polymorphic} prefix in sections only to declare constraints discharged at section closing time. +One cannot declare a global constraint on polymorphic universes. \begin{ErrMsgs} \item \errindex{Undeclared universe {\ident}}. diff --git a/engine/proofview.mli b/engine/proofview.mli index 7996b7969c..93ba55c61f 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -303,6 +303,9 @@ val guard_no_unifiable : Names.Name.t list option tactic goals of p *) val unshelve : Goal.goal list -> proofview -> proofview +(** [depends_on g1 g2 sigma] checks if g1 occurs in the type/ctx of g2 *) +val depends_on : Evd.evar_map -> Goal.goal -> Goal.goal -> bool + (** [with_shelf tac] executes [tac] and returns its result together with the set of goals shelved by [tac]. The current shelf is unchanged. *) val with_shelf : 'a tactic -> (Goal.goal list * 'a) tactic diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 9301359957..6ffe771da3 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -741,7 +741,7 @@ object(self) self#cleanup (Doc.cut_at document to_id); conclusion () | Fail (safe_id, loc, msg) -> - if loc <> None then messages#push Feedback.Error (Richpp.richpp_of_string "Fixme LOC"); +(* if loc <> None then messages#push Feedback.Error (Richpp.richpp_of_string "Fixme LOC"); *) messages#push Feedback.Error msg; if Stateid.equal safe_id Stateid.dummy then self#show_goals else undo safe_id diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index ae9328fcc0..6ce15a7c5a 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -454,7 +454,7 @@ type vernac_type = | VtStartProof of vernac_start | VtSideff of vernac_sideff_type | VtQed of vernac_qed_type - | VtProofStep of bool (* parallelize *) + | VtProofStep of proof_step | VtProofMode of string | VtQuery of vernac_part_of_script * report_with | VtStm of vernac_control * vernac_part_of_script @@ -476,6 +476,11 @@ and vernac_control = and opacity_guarantee = | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*) +and proof_step = { (* TODO: inline with OCaml 4.03 *) + parallel : bool; + proof_block_detection : proof_block_name option +} +and proof_block_name = string (* open type of delimiters *) type vernac_when = | VtNow | VtLater diff --git a/kernel/closure.ml b/kernel/closure.ml index 65123108fd..960bdb649a 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -363,6 +363,7 @@ let set_norm v = v.norm <- Norm let is_val v = match v.norm with Norm -> true | _ -> false let mk_atom c = {norm=Norm;term=FAtom c} +let mk_red f = {norm=Red;term=f} (* Could issue a warning if no is still Red, pointing out that we loose sharing. *) diff --git a/kernel/closure.mli b/kernel/closure.mli index 07176cb7de..8e172290fb 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -164,6 +164,9 @@ val inject : constr -> fconstr (** mk_atom: prevents a term from being evaluated *) val mk_atom : constr -> fconstr +(** mk_red: makes a reducible term (used in newring) *) +val mk_red : fterm -> fconstr + val fterm_of : fconstr -> fterm val term_of_fconstr : fconstr -> constr val destFLambda : diff --git a/lib/flags.ml b/lib/flags.ml index c1ec9738ca..f07877e20d 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -68,11 +68,15 @@ let priority_of_string = function | "low" -> Low | "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_cmd_error_resilience = ref true let async_proofs_is_worker () = !async_proofs_worker_id <> "master" let async_proofs_is_master () = !async_proofs_mode = APon && !async_proofs_worker_id = "master" +let async_proofs_delegation_threshold = ref 0.03 let debug = ref false let in_debugger = ref false @@ -220,6 +224,7 @@ let native_compiler = ref false let print_mod_uid = ref false let tactic_context_compat = ref false +let profile_ltac = ref false let dump_bytecode = ref false let set_dump_bytecode = (:=) dump_bytecode diff --git a/lib/flags.mli b/lib/flags.mli index 24780f0dcc..729c21fcf9 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -34,6 +34,10 @@ type priority = Low | High val async_proofs_worker_priority : priority ref val string_of_priority : priority -> string val priority_of_string : string -> priority +type tac_error_filter = [ `None | `Only of string list | `All ] +val async_proofs_tac_error_resilience : tac_error_filter ref +val async_proofs_cmd_error_resilience : bool ref +val async_proofs_delegation_threshold : float ref val debug : bool ref val in_debugger : bool ref @@ -143,6 +147,8 @@ val tactic_context_compat : bool ref (** Set to [true] to trigger the compatibility bugged context matching (old context vs. appcontext) is set. *) +val profile_ltac : bool ref + (** Dump the bytecode after compilation (for debugging purposes) *) val dump_bytecode : bool ref val set_dump_bytecode : bool -> unit diff --git a/lib/stateid.ml b/lib/stateid.ml index c17df2b321..500581a39e 100644 --- a/lib/stateid.ml +++ b/lib/stateid.ml @@ -29,7 +29,13 @@ let get exn = Exninfo.get exn state_id_info let equal = Int.equal let compare = Int.compare -module Set = Set.Make(struct type t = int let compare = compare end) +module Self = struct + type t = int + let compare = compare + let equal = equal +end + +module Set = Set.Make(Self) type ('a,'b) request = { exn_info : t * t; diff --git a/lib/stateid.mli b/lib/stateid.mli index 516ad891ff..cd8fddf0ce 100644 --- a/lib/stateid.mli +++ b/lib/stateid.mli @@ -11,7 +11,8 @@ type t val equal : t -> t -> bool val compare : t -> t -> int -module Set : Set.S with type elt = t +module Self : Map.OrderedType with type t = t +module Set : Set.S with type elt = t and type t = Set.Make(Self).t val initial : t val dummy : t diff --git a/lib/unicode.ml b/lib/unicode.ml index 7aa8d9d513..dc852d9819 100644 --- a/lib/unicode.ml +++ b/lib/unicode.ml @@ -261,3 +261,73 @@ let ascii_of_ident s = (Buffer.add_char out s.[!i]; incr i) done; Buffer.contents out + +(* Compute length of an UTF-8 encoded string + Rem 1 : utf8_length <= String.length (equal if pure ascii) + Rem 2 : if used for an iso8859_1 encoded string, the result is + wrong in very rare cases. Such a wrong case corresponds to any + sequence of a character in range 192..253 immediately followed by a + character in range 128..191 (typical case in french is "déçu" which + is counted 3 instead of 4); then no real harm to use always + utf8_length even if using an iso8859_1 encoding *) + +(** FIXME: duplicate code with Pp *) + +let utf8_length s = + let len = String.length s + and cnt = ref 0 + and nc = ref 0 + and p = ref 0 in + while !p < len do + begin + match s.[!p] with + | '\000'..'\127' -> nc := 0 (* ascii char *) + | '\128'..'\191' -> nc := 0 (* cannot start with a continuation byte *) + | '\192'..'\223' -> nc := 1 (* expect 1 continuation byte *) + | '\224'..'\239' -> nc := 2 (* expect 2 continuation bytes *) + | '\240'..'\247' -> nc := 3 (* expect 3 continuation bytes *) + | '\248'..'\251' -> nc := 4 (* expect 4 continuation bytes *) + | '\252'..'\253' -> nc := 5 (* expect 5 continuation bytes *) + | '\254'..'\255' -> nc := 0 (* invalid byte *) + end ; + incr p ; + while !p < len && !nc > 0 do + match s.[!p] with + | '\128'..'\191' (* next continuation byte *) -> incr p ; decr nc + | _ (* not a continuation byte *) -> nc := 0 + done ; + incr cnt + done ; + !cnt + +(* Variant of String.sub for UTF8 character positions *) +let utf8_sub s start_u len_u = + let len_b = String.length s + and end_u = start_u + len_u + and cnt = ref 0 + and nc = ref 0 + and p = ref 0 in + let start_b = ref len_b in + while !p < len_b && !cnt < end_u do + if !cnt <= start_u then start_b := !p ; + begin + match s.[!p] with + | '\000'..'\127' -> nc := 0 (* ascii char *) + | '\128'..'\191' -> nc := 0 (* cannot start with a continuation byte *) + | '\192'..'\223' -> nc := 1 (* expect 1 continuation byte *) + | '\224'..'\239' -> nc := 2 (* expect 2 continuation bytes *) + | '\240'..'\247' -> nc := 3 (* expect 3 continuation bytes *) + | '\248'..'\251' -> nc := 4 (* expect 4 continuation bytes *) + | '\252'..'\253' -> nc := 5 (* expect 5 continuation bytes *) + | '\254'..'\255' -> nc := 0 (* invalid byte *) + end ; + incr p ; + while !p < len_b && !nc > 0 do + match s.[!p] with + | '\128'..'\191' (* next continuation byte *) -> incr p ; decr nc + | _ (* not a continuation byte *) -> nc := 0 + done ; + incr cnt + done ; + let end_b = !p in + String.sub s !start_b (end_b - !start_b) diff --git a/lib/unicode.mli b/lib/unicode.mli index aaf455dec5..1f8bd44eee 100644 --- a/lib/unicode.mli +++ b/lib/unicode.mli @@ -40,3 +40,9 @@ val ascii_of_ident : string -> string (** Validate an UTF-8 string *) val is_utf8 : string -> bool + +(** Return the length of a valid UTF-8 string. *) +val utf8_length : string -> int + +(** Variant of {!String.sub} for UTF-8 strings. *) +val utf8_sub : string -> int -> int -> string diff --git a/library/declare.ml b/library/declare.ml index b0df32b8de..84284fd182 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -440,8 +440,9 @@ let cache_universes (p, l) = let glob = Universes.global_universe_names () in let glob', ctx = List.fold_left (fun ((idl,lid),ctx) (id, lev) -> - ((Idmap.add id lev idl, Univ.LMap.add lev id lid), - Univ.ContextSet.add_universe lev ctx)) + ((Idmap.add id (p, lev) idl, + Univ.LMap.add lev id lid), + Univ.ContextSet.add_universe lev ctx)) (glob, Univ.ContextSet.empty) l in Global.push_context_set p ctx; @@ -457,6 +458,12 @@ let input_universes : universe_decl -> Libobject.obj = classify_function = (fun a -> Keep a) } let do_universe poly l = + let in_section = Lib.sections_are_opened () in + let () = + if poly && not in_section then + user_err_loc (Loc.ghost, "Constraint", + str"Cannot declare polymorphic universes outside sections") + in let l = List.map (fun (l, id) -> let lev = Universes.new_univ_level (Global.current_dirpath ()) in @@ -485,14 +492,30 @@ let input_constraints : constraint_decl -> Libobject.obj = let do_constraint poly l = let u_of_id = let names, _ = Universes.global_universe_names () in - fun (loc, id) -> - try Idmap.find id names - with Not_found -> - user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id) + fun (loc, id) -> + try Idmap.find id names + with Not_found -> + user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id) + in + let in_section = Lib.sections_are_opened () in + let () = + if poly && not in_section then + user_err_loc (Loc.ghost, "Constraint", + str"Cannot declare polymorphic constraints outside sections") + in + let check_poly loc p loc' p' = + if poly then () + else if p || p' then + let loc = if p then loc else loc' in + user_err_loc (loc, "Constraint", + str "Cannot declare a global constraint on " ++ + str "a polymorphic universe, use " + ++ str "Polymorphic Constraint instead") in let constraints = List.fold_left (fun acc (l, d, r) -> - let lu = u_of_id l and ru = u_of_id r in - Univ.Constraint.add (lu, d, ru) acc) + let p, lu = u_of_id l and p', ru = u_of_id r in + check_poly (fst l) p (fst r) p'; + Univ.Constraint.add (lu, d, ru) acc) Univ.Constraint.empty l in Lib.add_anonymous_leaf (input_constraints (poly, constraints)) diff --git a/library/declaremods.ml b/library/declaremods.ml index f3f734aa09..dcd63c7691 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -897,7 +897,13 @@ let start_library dir = Lib.start_compilation dir mp; Lib.add_frozen_state () +let end_library_hook = ref ignore +let append_end_library_hook f = + let old_f = !end_library_hook in + end_library_hook := fun () -> old_f(); f () + let end_library ?except dir = + !end_library_hook(); let oname = Lib.end_compilation_checks dir in let mp,cenv,ast = Global.export ?except dir in let prefix, lib_stack = Lib.end_compilation oname in diff --git a/library/declaremods.mli b/library/declaremods.mli index 2b440c087a..3917fe8d64 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -90,6 +90,9 @@ val end_library : ?except:Future.UUIDSet.t -> library_name -> Safe_typing.compiled_library * library_objects * Safe_typing.native_library +(** append a function to be executed at end_library *) +val append_end_library_hook : (unit -> unit) -> unit + (** [really_import_module mp] opens the module [mp] (in a Caml sense). It modifies Nametab and performs the [open_object] function for every object of the module. Raises [Not_found] when [mp] is unknown diff --git a/library/universes.ml b/library/universes.ml index c4eb2afcbb..75cbd5604b 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -13,10 +13,11 @@ open Term open Environ open Univ open Globnames +open Decl_kinds (** Global universe names *) type universe_names = - Univ.universe_level Idmap.t * Id.t Univ.LMap.t + (polymorphic * Univ.universe_level) Idmap.t * Id.t Univ.LMap.t let global_universes = Summary.ref ~name:"Global universe names" diff --git a/library/universes.mli b/library/universes.mli index 53cf5f3844..a5740ec49f 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -19,7 +19,7 @@ val is_set_minimization : unit -> bool (** Global universe name <-> level mapping *) type universe_names = - Univ.universe_level Idmap.t * Id.t Univ.LMap.t + (Decl_kinds.polymorphic * Univ.universe_level) Idmap.t * Id.t Univ.LMap.t val global_universe_names : unit -> universe_names val set_global_universe_names : universe_names -> unit diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index 5d3c149ab9..57fad85113 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -872,7 +872,7 @@ END;; mode. *) VERNAC COMMAND EXTEND GrabEvars [ "Grab" "Existential" "Variables" ] - => [ Vernacexpr.VtProofStep false, Vernacexpr.VtLater ] + => [ Vernac_classifier.classify_as_proofstep ] -> [ Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.grab_evars p) ] END @@ -903,7 +903,7 @@ END (* Command to add every unshelved variables to the focus *) VERNAC COMMAND EXTEND Unshelve [ "Unshelve" ] - => [ Vernacexpr.VtProofStep false, Vernacexpr.VtLater ] + => [ Vernac_classifier.classify_as_proofstep ] -> [ Proof_global.simple_with_current_proof (fun _ p -> Proof.unshelve p) ] END diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4 index 3579fc10f6..7c161e5cdc 100644 --- a/ltac/g_ltac.ml4 +++ b/ltac/g_ltac.ml4 @@ -366,7 +366,8 @@ VERNAC tactic_mode EXTEND VernacSolve vernac_solve g n t def ] | [ - "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => - [ VtProofStep true, VtLater ] -> [ + [ VtProofStep{ parallel = true; proof_block_detection = Some "par" }, + VtLater ] -> [ vernac_solve SelectAll n t def ] END diff --git a/ltac/ltac.mllib b/ltac/ltac.mllib index e0c6f3ac0a..65ed114cff 100644 --- a/ltac/ltac.mllib +++ b/ltac/ltac.mllib @@ -3,6 +3,7 @@ Tacenv Tactic_debug Tacintern Tacentries +Profile_ltac Tacinterp Evar_tactics Tactic_option @@ -10,6 +11,7 @@ Extraargs G_obligations Coretactics Extratactics +Profile_ltac_tactics G_auto G_class Rewrite diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml new file mode 100644 index 0000000000..7a8ef32c3f --- /dev/null +++ b/ltac/profile_ltac.ml @@ -0,0 +1,323 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Unicode +open Pp +open Printer +open Util + +(** [is_profiling] and the profiling info ([stack]) should be synchronized with + the document; the rest of the ref cells are either local to individual + tactic invocations, or global flags, and need not be synchronized, since no + document-level backtracking happens within tactics. We synchronize + is_profiling via an option. *) +let is_profiling = Flags.profile_ltac + +let set_profiling b = is_profiling := b +let get_profiling () = !is_profiling + +let new_call = ref false +let entered_call () = new_call := true +let is_new_call () = let b = !new_call in new_call := false; b + +(** LtacProf cannot yet handle backtracking into multi-success tactics. + To properly support this, we'd have to somehow recreate our location in the + call-stack, and stop/restart the intervening timers. This is tricky and + possibly expensive, so instead we currently just emit a warning that + profiling results will be off. *) +let encountered_multi_success_backtracking = ref false + +let warn_encountered_multi_success_backtracking () = + if !encountered_multi_success_backtracking then + Feedback.msg_warning (str "Ltac Profiler cannot yet handle backtracking \ + into multi-success tactics; profiling results may be wildly inaccurate.") + +let encounter_multi_success_backtracking () = + if not !encountered_multi_success_backtracking + then begin + encountered_multi_success_backtracking := true; + warn_encountered_multi_success_backtracking () + end + +type entry = { + mutable total : float; + mutable local : float; + mutable ncalls : int; + mutable max_total : float +} + +let empty_entry () = { total = 0.; local = 0.; ncalls = 0; max_total = 0. } + +let add_entry e add_total { total; local; ncalls; max_total } = + if add_total then e.total <- e.total +. total; + e.local <- e.local +. local; + e.ncalls <- e.ncalls + ncalls; + if add_total then e.max_total <- max e.max_total max_total + +type treenode = { + entry : entry; + children : (string, treenode) Hashtbl.t +} + +let empty_treenode n = { entry = empty_entry (); children = Hashtbl.create n } + +(** Tobias Tebbi wrote some tricky code involving mutation. Rather than + rewriting it in a functional style, we simply freeze the state when we need + to by issuing a deep copy of the profiling data. *) +(** TODO: rewrite me in purely functional style *) +let deepcopy_entry { total; local; ncalls; max_total } = + { total; local; ncalls; max_total } + +let rec deepcopy_treenode { entry; children } = + let children' = Hashtbl.create (Hashtbl.length children) in + let iter key subtree = Hashtbl.add children' key (deepcopy_treenode subtree) in + let () = Hashtbl.iter iter children in + { entry = deepcopy_entry entry; children = children' } + +let stack = + let freeze _ = List.map deepcopy_treenode in + Summary.ref ~freeze [empty_treenode 20] ~name:"LtacProf-stack" + +let on_stack = Hashtbl.create 5 + +let get_node c table = + try Hashtbl.find table c + with Not_found -> + let new_node = empty_treenode 5 in + Hashtbl.add table c new_node; + new_node + +let rec add_node node node' = + add_entry node.entry true node'.entry; + Hashtbl.iter + (fun s node' -> add_node (get_node s node.children) node') + node'.children + +let time () = + let times = Unix.times () in + times.Unix.tms_utime +. times.Unix.tms_stime + +(* +let msgnl_with fmt strm = msg_with fmt (strm ++ fnl ()) +let msgnl strm = msgnl_with !Pp_control.std_ft strm + +let rec print_treenode indent (tn : treenode) = + msgnl (str (indent^"{ entry = {")); + Feedback.msg_notice (str (indent^"total = ")); + msgnl (str (indent^(string_of_float (tn.entry.total)))); + Feedback.msg_notice (str (indent^"local = ")); + msgnl (str (indent^(string_of_float tn.entry.local))); + Feedback.msg_notice (str (indent^"ncalls = ")); + msgnl (str (indent^(string_of_int tn.entry.ncalls))); + Feedback.msg_notice (str (indent^"max_total = ")); + msgnl (str (indent^(string_of_float tn.entry.max_total))); + msgnl (str (indent^"}")); + msgnl (str (indent^"children = {")); + Hashtbl.iter + (fun s node -> + msgnl (str (indent^" "^s^" |-> ")); + print_treenode (indent^" ") node + ) + tn.children; + msgnl (str (indent^"} }")) + +let rec print_stack (st : treenode list) = match st with +| [] -> msgnl (str "[]") +| x :: xs -> print_treenode "" x; msgnl (str ("::")); print_stack xs +*) + +let string_of_call ck = + let s = + string_of_ppcmds + (match ck with + | Tacexpr.LtacNotationCall s -> Names.KerName.print s + | Tacexpr.LtacNameCall cst -> Pptactic.pr_ltac_constant cst + | Tacexpr.LtacVarCall (id, t) -> Nameops.pr_id id + | Tacexpr.LtacAtomCall te -> + (Pptactic.pr_glob_tactic (Global.env ()) + (Tacexpr.TacAtom (Loc.ghost, te))) + | Tacexpr.LtacConstrInterp (c, _) -> + pr_glob_constr_env (Global.env ()) c + | Tacexpr.LtacMLCall te -> + (Pptactic.pr_glob_tactic (Global.env ()) + te) + ) in + for i = 0 to String.length s - 1 do if s.[i] = '\n' then s.[i] <- ' ' done; + let s = try String.sub s 0 (CString.string_index_from s 0 "(*") with Not_found -> s in + CString.strip s + +let exit_tactic start_time add_total c = match !stack with +| [] | [_] -> + (* oops, our stack is invalid *) + encounter_multi_success_backtracking () +| node :: (parent :: _ as stack') -> + stack := stack'; + if add_total then Hashtbl.remove on_stack (string_of_call c); + let diff = time () -. start_time in + parent.entry.local <- parent.entry.local -. diff; + let node' = { total = diff; local = diff; ncalls = 1; max_total = diff } in + add_entry node.entry add_total node' + +let tclFINALLY tac (finally : unit Proofview.tactic) = + let open Proofview.Notations in + Proofview.tclIFCATCH + tac + (fun v -> finally <*> Proofview.tclUNIT v) + (fun (exn, info) -> finally <*> Proofview.tclZERO ~info exn) + +let do_profile s call_trace tac = + let open Proofview.Notations in + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> + if !is_profiling && is_new_call () then + match call_trace with + | (_, c) :: _ -> + let s = string_of_call c in + let parent = List.hd !stack in + let node, add_total = try Hashtbl.find on_stack s, false + with Not_found -> + let node = get_node s parent.children in + Hashtbl.add on_stack s node; + node, true + in + if not add_total && node = List.hd !stack then None else ( + stack := node :: !stack; + let start_time = time () in + Some (start_time, add_total) + ) + | [] -> None + else None)) >>= function + | Some (start_time, add_total) -> + tclFINALLY + tac + (Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> + (match call_trace with + | (_, c) :: _ -> + exit_tactic start_time add_total c + | [] -> ())))) + | None -> tac + + + +let format_sec x = (Printf.sprintf "%.3fs" x) +let format_ratio x = (Printf.sprintf "%.1f%%" (100. *. x)) +let padl n s = ws (max 0 (n - utf8_length s)) ++ str s +let padr n s = str s ++ ws (max 0 (n - utf8_length s)) +let padr_with c n s = + let ulength = utf8_length s in + str (utf8_sub s 0 n) ++ str (String.make (max 0 (n - ulength)) c) + +let rec list_iter_is_last f = function + | [] -> [] + | [x] -> [f true x] + | x :: xs -> f false x :: list_iter_is_last f xs + +let header = + str " tactic self total calls max" ++ + fnl () ++ + str "────────────────────────────────────────┴──────┴──────┴───────┴─────────┘" + +let rec print_node all_total indent prefix (s, n) = + let e = n.entry in + h 0 ( + padr_with '-' 40 (prefix ^ s ^ " ") + ++ padl 7 (format_ratio (e.local /. all_total)) + ++ padl 7 (format_ratio (e.total /. all_total)) + ++ padl 8 (string_of_int e.ncalls) + ++ padl 10 (format_sec (e.max_total)) + ) ++ + print_table all_total indent false n.children + +and print_table all_total indent first_level table = + let fold s n l = if n.entry.total /. all_total < 0.02 then l else (s, n) :: l in + let ls = Hashtbl.fold fold table [] in + match ls with + | [s, n] when not first_level -> + print_node all_total indent (indent ^ "└") (s, n) + | _ -> + let ls = List.sort (fun (_, n1) (_, n2) -> compare n2.entry.total n1.entry.total) ls in + let iter is_last = + let sep0 = if first_level then "" else if is_last then " " else " │" in + let sep1 = if first_level then "─" else if is_last then " └─" else " ├─" in + print_node all_total (indent ^ sep0) (indent ^ sep1) + in + prlist_with_sep fnl (fun pr -> pr) (list_iter_is_last iter ls) + +let print_results () = + let tree = (List.hd !stack).children in + let all_total = -. (List.hd !stack).entry.local in + let global = Hashtbl.create 20 in + let rec cumulate table = + let iter s node = + let node' = get_node s global in + add_entry node'.entry true node.entry; + cumulate node.children + in + Hashtbl.iter iter table + in + cumulate tree; + warn_encountered_multi_success_backtracking (); + let msg = + h 0 (str "total time: " ++ padl 11 (format_sec (all_total))) ++ + fnl () ++ + header ++ + print_table all_total "" true global ++ + fnl () ++ + header ++ + print_table all_total "" true tree + in + Feedback.msg_notice msg + (* FOR DEBUGGING *) + (* ; + msgnl (str""); + print_stack (!stack) + *) + +let print_results_tactic tactic = + let tree = (List.hd !stack).children in + let table_tactic = Hashtbl.create 20 in + let rec cumulate table = + let iter s node = + if String.sub (s ^ ".") 0 (min (1 + String.length s) (String.length tactic)) = tactic + then add_node (get_node s table_tactic) node + else cumulate node.children + in + Hashtbl.iter iter table + in + cumulate tree; + let all_total = -. (List.hd !stack).entry.local in + let tactic_total = + Hashtbl.fold + (fun _ node all_total -> node.entry.total +. all_total) + table_tactic 0. in + warn_encountered_multi_success_backtracking (); + let msg = + h 0 (str"total time: " ++ padl 11 (format_sec (all_total))) ++ + h 0 (str"time spent in tactic: " ++ padl 11 (format_sec (tactic_total))) ++ + fnl () ++ + header ++ + print_table tactic_total "" true table_tactic + in + Feedback.msg_notice msg + +let reset_profile () = + stack := [empty_treenode 20]; + encountered_multi_success_backtracking := false + +let do_print_results_at_close () = if get_profiling () then print_results () + +let _ = Declaremods.append_end_library_hook do_print_results_at_close + +let _ = + let open Goptions in + declare_bool_option + { optsync = true; + optdepr = false; + optname = "Ltac Profiling"; + optkey = ["Ltac"; "Profiling"]; + optread = get_profiling; + optwrite = set_profiling } diff --git a/ltac/profile_ltac.mli b/ltac/profile_ltac.mli new file mode 100644 index 0000000000..7bbdca9425 --- /dev/null +++ b/ltac/profile_ltac.mli @@ -0,0 +1,25 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Ltac profiling primitives *) + +val do_profile : string -> ('a * Tacexpr.ltac_call_kind) list -> 'b Proofview.tactic -> 'b Proofview.tactic + +val set_profiling : bool -> unit + +val get_profiling : unit -> bool + +val entered_call : unit -> unit + +val print_results : unit -> unit + +val print_results_tactic : string -> unit + +val reset_profile : unit -> unit + +val do_print_results_at_close : unit -> unit diff --git a/ltac/profile_ltac_tactics.ml4 b/ltac/profile_ltac_tactics.ml4 new file mode 100644 index 0000000000..c092a0cb61 --- /dev/null +++ b/ltac/profile_ltac_tactics.ml4 @@ -0,0 +1,39 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i camlp4deps: "grammar/grammar.cma" i*) + +(** Ltac profiling entrypoints *) + +open Profile_ltac +open Stdarg + +DECLARE PLUGIN "profile_ltac_plugin" + +let tclSET_PROFILING b = + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> set_profiling b)) + +TACTIC EXTEND start_ltac_profiling +| [ "start" "ltac" "profiling" ] -> [ tclSET_PROFILING true ] +END + +TACTIC EXTEND stop_profiling +| [ "stop" "ltac" "profiling" ] -> [ tclSET_PROFILING false ] +END + +VERNAC COMMAND EXTEND ResetLtacProfiling CLASSIFIED AS SIDEFF + [ "Reset" "Ltac" "Profile" ] -> [ reset_profile() ] +END + +VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY + [ "Show" "Ltac" "Profile" ] -> [ print_results() ] +END + +VERNAC COMMAND EXTEND ShowLtacProfileTactic CLASSIFIED AS QUERY + [ "Show" "Ltac" "Profile" string(s) ] -> [ print_results_tactic s ] +END diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 5ee9b0fc4d..ab61c8abba 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -286,9 +286,10 @@ let constr_of_id env id = (** Generic arguments : table of interpretation functions *) +(* Some of the code further down depends on the fact that push_trace does not modify sigma (the evar map) *) let push_trace call ist = match TacStore.get ist.extra f_trace with -| None -> [call] -| Some trace -> call :: trace +| None -> Proofview.tclUNIT [call] +| Some trace -> Proofview.tclLIFT (Proofview.NonLogical.make Profile_ltac.entered_call) <*> Proofview.tclUNIT (call :: trace) let propagate_trace ist loc id v = let v = Value.normalize v in @@ -297,10 +298,11 @@ let propagate_trace ist loc id v = match tacv with | VFun (appl,_,lfun,it,b) -> let t = if List.is_empty it then b else TacFun (it,b) in - let ans = VFun (appl,push_trace(loc,LtacVarCall (id,t)) ist,lfun,it,b) in - of_tacvalue ans - | _ -> v - else v + push_trace(loc,LtacVarCall (id,t)) ist >>= fun trace -> + let ans = VFun (appl,trace,lfun,it,b) in + Proofview.tclUNIT (of_tacvalue ans) + | _ -> Proofview.tclUNIT v + else Proofview.tclUNIT v let append_trace trace v = let v = Value.normalize v in @@ -622,8 +624,13 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) = match kind with OfType _ -> WithoutTypeConstraint | _ -> kind in intern_gen kind_for_intern ~allow_patvar ~ltacvars env c in - let trace = - push_trace (loc_of_glob_constr c,LtacConstrInterp (c,vars)) ist in + (* Jason Gross: To avoid unnecessary modifications to tacinterp, as + suggested by Arnaud Spiwack, we run push_trace immediately. We do + this with the kludge of an empty proofview, and rely on the + invariant that running the tactic returned by push_trace does + not modify sigma. *) + let (_, dummy_proofview) = Proofview.init sigma [] in + let (trace,_,_,_) = Proofview.apply env (push_trace (loc_of_glob_constr c,LtacConstrInterp (c,vars)) ist) dummy_proofview in let (evd,c) = catch_error trace (understand_ltac flags env sigma vars kind) c in @@ -1169,7 +1176,9 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti and eval_tactic ist tac : unit Proofview.tactic = match tac with | TacAtom (loc,t) -> let call = LtacAtomCall t in - catch_error_tac (push_trace(loc,call) ist) (interp_atomic ist t) + push_trace(loc,call) ist >>= fun trace -> + Profile_ltac.do_profile "eval_tactic:2" trace + (catch_error_tac trace (interp_atomic ist t)) | TacFun _ | TacLetIn _ -> assert false | TacMatchGoal _ | TacMatch _ -> assert false | TacId [] -> Proofview.tclLIFT (db_breakpoint (curr_debug ist) []) @@ -1251,7 +1260,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with let tac l = let addvar x v accu = Id.Map.add x v accu in let lfun = List.fold_right2 addvar ids l ist.lfun in - let trace = push_trace (loc,LtacNotationCall s) ist in + Ftactic.lift (push_trace (loc,LtacNotationCall s) ist) >>= fun trace -> let ist = { lfun = lfun; extra = TacStore.set ist.extra f_trace trace; } in @@ -1276,7 +1285,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with Ftactic.run tac (fun () -> Proofview.tclUNIT ()) | TacML (loc,opn,l) -> - let trace = push_trace (loc,LtacMLCall tac) ist in + push_trace (loc,LtacMLCall tac) ist >>= fun trace -> let ist = { ist with extra = TacStore.set ist.extra f_trace trace; } in let tac = Tacenv.interp_ml_tactic opn in let args = Ftactic.List.map_right (fun a -> interp_tacarg ist a) l in @@ -1302,15 +1311,17 @@ and interp_ltac_reference loc' mustbetac ist r : Val.t Ftactic.t = try Id.Map.find id ist.lfun with Not_found -> in_gen (topwit wit_var) id in - Ftactic.bind (force_vrec ist v) begin fun v -> - let v = propagate_trace ist loc id v in + let open Ftactic in + force_vrec ist v >>= begin fun v -> + Ftactic.lift (propagate_trace ist loc id v) >>= fun v -> if mustbetac then Ftactic.return (coerce_to_tactic loc id v) else Ftactic.return v end | ArgArg (loc,r) -> let ids = extract_ids [] ist.lfun in let loc_info = ((if Loc.is_ghost loc' then loc else loc'),LtacNameCall r) in - let extra = TacStore.set ist.extra f_avoid_ids ids in - let extra = TacStore.set extra f_trace (push_trace loc_info ist) in + let extra = TacStore.set ist.extra f_avoid_ids ids in + push_trace loc_info ist >>= fun trace -> + let extra = TacStore.set extra f_trace trace in let ist = { lfun = Id.Map.empty; extra = extra; } in let appl = GlbAppl[r,[]] in val_interp ~appl ist (Tacenv.interp_ltac r) @@ -1408,7 +1419,7 @@ and tactic_of_value ist vle = lfun = lfun; extra = TacStore.set ist.extra f_trace []; } in let tac = name_if_glob appl (eval_tactic ist t) in - catch_error_tac trace tac + Profile_ltac.do_profile "tactic_of_value" trace (catch_error_tac trace tac) | (VFun _|VRec _) -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.") else if has_type vle (topwit wit_tactic) then let tac = out_gen (topwit wit_tactic) vle in diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 0feba6365c..73d3d1bab8 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -100,7 +100,7 @@ let _ = Pptactic.declare_extra_genarg_pprule wit_proof_instr let classify_proof_instr = function | { instr = Pescape |Pend B_proof } -> VtProofMode "Classic", VtNow - | _ -> VtProofStep false, VtLater + | _ -> Vernac_classifier.classify_as_proofstep (* We use the VERNAC EXTEND facility with a custom non-terminal to populate [proof_mode] with a new toplevel interpreter. diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 7af72b07cf..57ef920325 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -34,15 +34,6 @@ open Proofview.Notations (****************************************************************************) (* controlled reduction *) -(** ppedrot: something dubious here, we're obviously using evars the wrong - way. FIXME! *) - -let mark_arg i c = mkEvar(Evar.unsafe_of_int i,[|c|]) -let unmark_arg f c = - match destEvar c with - | (i,[|c|]) -> f (Evar.repr i) c - | _ -> assert false - type protect_flag = Eval|Prot|Rec let tag_arg tag_rec map subs i c = @@ -75,12 +66,10 @@ and mk_clos_app_but f_map subs f args n = let fargs, args' = Array.chop n args in let f' = mkApp(f,fargs) in match f_map (global_of_constr_nofail f') with - Some map -> - mk_clos_deep - (fun s' -> unmark_arg (tag_arg (mk_clos_but f_map s') map s')) - subs - (mkApp (mark_arg (-1) f', Array.mapi mark_arg args')) - | None -> mk_clos_app_but f_map subs f args (n+1) + | Some map -> + let f i t = tag_arg (mk_clos_but f_map subs) map subs i t in + mk_red (FApp (f (-1) f', Array.mapi f args')) + | None -> mk_atom (mkApp (f, args)) let interp_map l t = try Some(List.assoc_f eq_gr t l) with Not_found -> None diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 7ec7d21c0c..e5fc5a188d 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -103,8 +103,7 @@ let position_problem l2r = function | CUMUL -> Some l2r let occur_rigidly ev evd t = - let (l, app) = decompose_app_vect t in - let rec aux t = + let rec aux t = match kind_of_term (whd_evar evd t) with | App (f, c) -> if aux f then Array.exists aux c else false | Construct _ | Ind _ | Sort _ | Meta _ | Fix _ | CoFix _ -> true @@ -116,7 +115,7 @@ let occur_rigidly ev evd t = | Prod (_, b, t) -> ignore(aux b || aux t); true | Rel _ | Var _ -> false | Case _ -> false - in Array.exists (fun t -> try ignore(aux t); false with Occur -> true) app + in try ignore(aux t); false with Occur -> true (* [check_conv_record env sigma (t1,stack1) (t2,stack2)] tries to decompose the problem (t1 stack1) = (t2 stack2) into a problem @@ -368,8 +367,6 @@ let rec evar_conv_x ts env evd pbty term1 term2 = and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ((term1,sk1 as appr1),csts1) ((term2,sk2 as appr2),csts2) = - let default_fail i = (* costly *) - UnifFailure (i,ConversionFailed (env, Stack.zip appr1, Stack.zip appr2)) in let quick_fail i = (* not costly, loses info *) UnifFailure (i, NotSameHead) in @@ -421,7 +418,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let not_only_app = Stack.not_purely_applicative skM in let f1 i = match Stack.list_of_app_stack skF with - | None -> default_fail evd + | None -> quick_fail evd | Some lF -> let tM = Stack.zip apprM in miller_pfenning on_left @@ -468,10 +465,11 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let flex_rigid on_left ev (termF, skF as apprF) (termR, skR as apprR) = let switch f a b = if on_left then f a b else f b a in let eta evd = - match kind_of_term termR with - | Lambda _ -> eta env evd false skR termR skF termF - | Construct u -> eta_constructor ts env evd skR u skF termF - | _ -> UnifFailure (evd,NotSameHead) + match kind_of_term termR with + | Lambda _ when (* if ever problem is ill-typed: *) List.is_empty skR -> + eta env evd false skR termR skF termF + | Construct u -> eta_constructor ts env evd skR u skF termF + | _ -> UnifFailure (evd,NotSameHead) in match Stack.list_of_app_stack skF with | None -> @@ -747,10 +745,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ise_try evd [f3; f4] (* Eta-expansion *) - | Rigid, _ when isLambda term1 -> + | Rigid, _ when isLambda term1 && (* if ever ill-typed: *) List.is_empty sk1 -> eta env evd true sk1 term1 sk2 term2 - | _, Rigid when isLambda term2 -> + | _, Rigid when isLambda term2 && (* if ever ill-typed: *) List.is_empty sk2 -> eta env evd false sk2 term2 sk1 term1 | Rigid, Rigid -> begin @@ -1106,7 +1104,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = abstract_free_holes evd subst, true with TypingFailed evd -> evd, false -let second_order_matching_with_args ts env evd ev l t = +let second_order_matching_with_args ts env evd pbty ev l t = (* let evd,ev = evar_absorb_arguments env evd ev l in let argoccs = Array.map_to_list (fun _ -> None) (snd ev) in @@ -1114,8 +1112,9 @@ let second_order_matching_with_args ts env evd ev l t = if b then Success evd else UnifFailure (evd, ConversionFailed (env,mkApp(mkEvar ev,l),t)) if b then Success evd else -*) - UnifFailure (evd, ConversionFailed (env,mkApp(mkEvar ev,l),t)) + *) + let pb = (pbty,env,mkApp(mkEvar ev,l),t) in + UnifFailure (evd, CannotSolveConstraint (pb,ProblemBeyondCapabilities)) let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = let t1 = apprec_nohdbeta ts env evd (whd_head_evar evd t1) in @@ -1131,7 +1130,9 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = type inference *) (match choose_less_dependent_instance evk1 evd term2 args1 with | Some evd -> Success evd - | None -> UnifFailure (evd, ConversionFailed (env,term1,term2))) + | None -> + let reason = ProblemBeyondCapabilities in + UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason))) | (Rel _|Var _), Evar (evk2,args2) when app_empty && List.for_all (fun a -> Term.eq_constr a term1 || isEvar a) (remove_instance_local_defs evd evk2 args2) -> @@ -1139,7 +1140,9 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = type inference *) (match choose_less_dependent_instance evk2 evd term1 args2 with | Some evd -> Success evd - | None -> UnifFailure (evd, ConversionFailed (env,term1,term2))) + | None -> + let reason = ProblemBeyondCapabilities in + UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason))) | Evar (evk1,args1), Evar (evk2,args2) when Evar.equal evk1 evk2 -> let f env evd pbty x y = is_fconv ~reds:ts pbty env evd x y in Success (solve_refl ~can_drop:true f env evd @@ -1154,20 +1157,20 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = ise_try evd [(fun evd -> first_order_unification ts env evd (ev1,l1) appr2); (fun evd -> - second_order_matching_with_args ts env evd ev1 l1 t2)] + second_order_matching_with_args ts env evd pbty ev1 l1 t2)] | _,Evar ev2 when Array.length l2 <= Array.length l1 -> (* On "u u1 .. u(n+p) = ?n t1 .. tn", try first-order unification *) (* and otherwise second-order matching *) ise_try evd [(fun evd -> first_order_unification ts env evd (ev2,l2) appr1); (fun evd -> - second_order_matching_with_args ts env evd ev2 l2 t1)] + second_order_matching_with_args ts env evd pbty ev2 l2 t1)] | Evar ev1,_ -> (* Try second-order pattern-matching *) - second_order_matching_with_args ts env evd ev1 l1 t2 + second_order_matching_with_args ts env evd pbty ev1 l1 t2 | _,Evar ev2 -> (* Try second-order pattern-matching *) - second_order_matching_with_args ts env evd ev2 l2 t1 + second_order_matching_with_args ts env evd pbty ev2 l2 t1 | _ -> (* Some head evar have been instantiated, or unknown kind of problem *) evar_conv_x ts env evd pbty t1 t2 diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index cf5b08c58f..b0715af734 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -14,15 +14,16 @@ open Type_errors type unification_error = | OccurCheck of existential_key * constr - | NotClean of existential * env * constr + | NotClean of existential * env * constr (* Constr is a variable not in scope *) | NotSameArgSize | NotSameHead | NoCanonicalStructure - | ConversionFailed of env * constr * constr + | ConversionFailed of env * constr * constr (* Non convertible closed terms *) | MetaOccurInBody of existential_key | InstanceNotSameType of existential_key * env * types * types | UnifUnivInconsistency of Univ.univ_inconsistency | CannotSolveConstraint of Evd.evar_constraint * unification_error + | ProblemBeyondCapabilities type position = (Id.t * Locus.hyp_location_flag) option diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index f617df9ee7..880f48e5f9 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -24,6 +24,7 @@ type unification_error = | InstanceNotSameType of existential_key * env * types * types | UnifUnivInconsistency of Univ.univ_inconsistency | CannotSolveConstraint of Evd.evar_constraint * unification_error + | ProblemBeyondCapabilities type position = (Id.t * Locus.hyp_location_flag) option diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index efc42aab76..378294c984 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -143,7 +143,7 @@ let interp_universe_level_name evd (loc,s) = with Not_found -> try let id = try Id.of_string s with _ -> raise Not_found in - evd, Idmap.find id names + evd, snd (Idmap.find id names) with Not_found -> if not (is_strict_universe_declarations ()) then new_univ_level_variable ~loc ~name:s univ_rigid evd diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 1ef0b087ba..78dce0d64c 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -491,7 +491,8 @@ let clenv_unify_binding_type clenv c t u = let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in TypeProcessed, { clenv with evd = evd }, c with - | PretypeError (_,_,ActualTypeNotCoercible (_,_,NotClean _)) as e -> + | PretypeError (_,_,ActualTypeNotCoercible (_,_, + (NotClean _ | ConversionFailed _))) as e -> raise e | e when precatchable_exception e -> TypeNotProcessed, clenv, c diff --git a/stm/dag.ml b/stm/dag.ml index 0c7f9f34bd..99e7c92648 100644 --- a/stm/dag.ml +++ b/stm/dag.ml @@ -8,15 +8,6 @@ module type S = sig - module Cluster : - sig - type 'd t - val equal : 'd t -> 'd t -> bool - val compare : 'd t -> 'd t -> int - val to_string : 'd t -> string - val data : 'd t -> 'd - end - type node module NodeSet : Set.S with type elt = node @@ -31,45 +22,57 @@ module type S = sig val del_nodes : ('e,'i,'d) t -> NodeSet.t -> ('e,'i,'d) t val all_nodes : ('e,'i,'d) t -> NodeSet.t - val iter : ('e,'i,'d) t -> - (node -> 'd Cluster.t option -> 'i option -> - (node * 'e) list -> unit) -> unit - - val create_cluster : ('e,'i,'d) t -> node list -> 'd -> ('e,'i,'d) t - val cluster_of : ('e,'i,'d) t -> node -> 'd Cluster.t option - val del_cluster : ('e,'i,'d) t -> 'd Cluster.t -> ('e,'i,'d) t - val get_info : ('e,'i,'d) t -> node -> 'i option val set_info : ('e,'i,'d) t -> node -> 'i -> ('e,'i,'d) t val clear_info : ('e,'i,'d) t -> node -> ('e,'i,'d) t + module Property : + sig + type 'd t + val equal : 'd t -> 'd t -> bool + val compare : 'd t -> 'd t -> int + val to_string : 'd t -> string + val data : 'd t -> 'd + val having_it : 'd t -> NodeSet.t + end + + val create_property : ('e,'i,'d) t -> node list -> 'd -> ('e,'i,'d) t + val property_of : ('e,'i,'d) t -> node -> 'd Property.t list + val del_property : ('e,'i,'d) t -> 'd Property.t -> ('e,'i,'d) t + + val iter : ('e,'i,'d) t -> + (node -> 'd Property.t list -> 'i option -> + (node * 'e) list -> unit) -> unit + end module Make(OT : Map.OrderedType) = struct -module Cluster = +module NodeSet = Set.Make(OT) + +module Property = struct - type 'd t = 'd * int - let equal (_,i1) (_,i2) = Int.equal i1 i2 - let compare (_,i1) (_,i2) = Int.compare i1 i2 - let to_string (_,i) = string_of_int i - let data (d,_) = d + type 'd t = { data : 'd; uid : int; having_it : NodeSet.t } + let equal { uid = i1 } { uid = i2 } = Int.equal i1 i2 + let compare { uid = i1 } { uid = i2 } = Int.compare i1 i2 + let to_string { uid = i } = string_of_int i + let data { data = d } = d + let having_it { having_it } = having_it end type node = OT.t module NodeMap = CMap.Make(OT) -module NodeSet = Set.Make(OT) type ('edge,'info,'data) t = { graph : (node * 'edge) list NodeMap.t; - clusters : 'data Cluster.t NodeMap.t; + properties : 'data Property.t list NodeMap.t; infos : 'info NodeMap.t; } let empty = { graph = NodeMap.empty; - clusters = NodeMap.empty; + properties = NodeMap.empty; infos = NodeMap.empty; } @@ -94,7 +97,7 @@ let del_edge dag id tgt = { dag with let del_nodes dag s = { infos = NodeMap.filter (fun n _ -> not(NodeSet.mem n s)) dag.infos; - clusters = NodeMap.filter (fun n _ -> not(NodeSet.mem n s)) dag.clusters; + properties = NodeMap.filter (fun n _ -> not(NodeSet.mem n s)) dag.properties; graph = NodeMap.filter (fun n l -> let drop = NodeSet.mem n s in if not drop then @@ -102,20 +105,31 @@ let del_nodes dag s = { not drop) dag.graph } +let map_add_list k v m = + try + let l = NodeMap.find k m in + NodeMap.add k (v::l) m + with Not_found -> NodeMap.add k [v] m + let clid = ref 1 -let create_cluster dag l data = +let create_property dag l data = incr clid; - { dag with clusters = - List.fold_right (fun x clusters -> - NodeMap.add x (data, !clid) clusters) l dag.clusters } - -let cluster_of dag id = - try Some (NodeMap.find id dag.clusters) - with Not_found -> None - -let del_cluster dag c = - { dag with clusters = - NodeMap.filter (fun _ c' -> not (Cluster.equal c' c)) dag.clusters } + let having_it = List.fold_right NodeSet.add l NodeSet.empty in + let property = { Property.data; uid = !clid; having_it } in + { dag with properties = + List.fold_right (fun x ps -> map_add_list x property ps) l dag.properties } + +let property_of dag id = + try NodeMap.find id dag.properties + with Not_found -> [] + +let del_property dag c = + { dag with properties = + NodeMap.filter (fun _ cl -> cl <> []) + (NodeMap.map (fun cl -> + List.filter (fun c' -> + not (Property.equal c' c)) cl) + dag.properties) } let get_info dag id = try Some (NodeMap.find id dag.infos) @@ -126,7 +140,7 @@ let set_info dag id info = { dag with infos = NodeMap.add id info dag.infos } let clear_info dag id = { dag with infos = NodeMap.remove id dag.infos } let iter dag f = - NodeMap.iter (fun k v -> f k (cluster_of dag k) (get_info dag k) v) dag.graph + NodeMap.iter (fun k v -> f k (property_of dag k) (get_info dag k) v) dag.graph let all_nodes dag = NodeMap.domain dag.graph diff --git a/stm/dag.mli b/stm/dag.mli index 6b4442df00..e783cd8ee1 100644 --- a/stm/dag.mli +++ b/stm/dag.mli @@ -7,19 +7,7 @@ (************************************************************************) module type S = sig - - (* A cluster is just a set of nodes. This set holds some data. - Stm uses this to group nodes contribution to the same proofs and - that can be evaluated asynchronously *) - module Cluster : - sig - type 'd t - val equal : 'd t -> 'd t -> bool - val compare : 'd t -> 'd t -> int - val to_string : 'd t -> string - val data : 'd t -> 'd - end - + type node module NodeSet : Set.S with type elt = node @@ -34,19 +22,35 @@ module type S = sig val del_nodes : ('e,'i,'d) t -> NodeSet.t -> ('e,'i,'d) t val all_nodes : ('e,'i,'d) t -> NodeSet.t - val iter : ('e,'i,'d) t -> - (node -> 'd Cluster.t option -> 'i option -> - (node * 'e) list -> unit) -> unit - - val create_cluster : ('e,'i,'d) t -> node list -> 'd -> ('e,'i,'d) t - val cluster_of : ('e,'i,'d) t -> node -> 'd Cluster.t option - val del_cluster : ('e,'i,'d) t -> 'd Cluster.t -> ('e,'i,'d) t - val get_info : ('e,'i,'d) t -> node -> 'i option val set_info : ('e,'i,'d) t -> node -> 'i -> ('e,'i,'d) t val clear_info : ('e,'i,'d) t -> node -> ('e,'i,'d) t -end + (* A property applies to a set of nodes and holds some data. + Stm uses this feature to group nodes contributing to the same proofs and + to structure proofs in boxes limiting the scope of errors *) + module Property : + sig + type 'd t + val equal : 'd t -> 'd t -> bool + val compare : 'd t -> 'd t -> int + val to_string : 'd t -> string + val data : 'd t -> 'd + val having_it : 'd t -> NodeSet.t + end + + val create_property : ('e,'i,'d) t -> node list -> 'd -> ('e,'i,'d) t + val property_of : ('e,'i,'d) t -> node -> 'd Property.t list + val del_property : ('e,'i,'d) t -> 'd Property.t -> ('e,'i,'d) t + + val iter : ('e,'i,'d) t -> + (node -> 'd Property.t list -> 'i option -> + (node * 'e) list -> unit) -> unit + + end -module Make(OT : Map.OrderedType) : S with type node = OT.t +module Make(OT : Map.OrderedType) : S +with type node = OT.t +and type NodeSet.t = Set.Make(OT).t +and type NodeSet.elt = OT.t diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml new file mode 100644 index 0000000000..ce12185cba --- /dev/null +++ b/stm/proofBlockDelimiter.ml @@ -0,0 +1,184 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Stm + +module Util : sig + +val simple_goal : Evd.evar_map -> Goal.goal -> Goal.goal list -> bool +val is_focused_goal_simple : Stateid.t -> [ `Simple of Goal.goal list | `Not ] + +type 'a until = [ `Stop | `Found of static_block_declaration | `Cont of 'a ] + +val crawl : + document_view -> ?init:document_node option -> + ('a -> document_node -> 'a until) -> 'a -> + static_block_declaration option + +val unit_val : Stm.DynBlockData.t +val of_bullet_val : Vernacexpr.bullet -> Stm.DynBlockData.t +val to_bullet_val : Stm.DynBlockData.t -> Vernacexpr.bullet +val of_vernac_expr_val : Vernacexpr.vernac_expr -> Stm.DynBlockData.t +val to_vernac_expr_val : Stm.DynBlockData.t -> Vernacexpr.vernac_expr + +end = struct + +let unit_tag = DynBlockData.create "unit" +let unit_val = DynBlockData.Easy.inj () unit_tag + +let of_bullet_val, to_bullet_val = DynBlockData.Easy.make_dyn "bullet" +let of_vernac_expr_val, to_vernac_expr_val = DynBlockData.Easy.make_dyn "vernac_expr" + +let simple_goal sigma g gs = + let open Evar in + let open Evd in + let open Evarutil in + let evi = Evd.find sigma g in + Set.is_empty (evars_of_term evi.evar_concl) && + Set.is_empty (evars_of_filtered_evar_info (nf_evar_info sigma evi)) && + not (List.exists (Proofview.depends_on sigma g) gs) + +let is_focused_goal_simple id = + match state_of_id id with + | `Expired | `Error _ | `Valid None -> `Not + | `Valid (Some { proof }) -> + let proof = Proof_global.proof_of_state proof in + let focused, r1, r2, r3, sigma = Proof.proof proof in + let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in + if List.for_all (fun x -> simple_goal sigma x rest) focused + then `Simple focused + else `Not + +type 'a until = [ `Stop | `Found of static_block_declaration | `Cont of 'a ] + +let crawl { entry_point; prev_node } ?(init=Some entry_point) f acc = + let rec crawl node acc = + match node with + | None -> None + | Some node -> + match f acc node with + | `Stop -> None + | `Found x -> Some x + | `Cont acc -> crawl (prev_node node) acc in + crawl init acc + +end + +include Util + +(* ****************** - foo - bar - baz *********************************** *) + +let static_bullet ({ entry_point; prev_node } as view) = + match entry_point.ast with + | Vernacexpr.VernacBullet b -> + let base = entry_point.indentation in + let last_tac = prev_node entry_point in + crawl view ~init:last_tac (fun prev node -> + if node.indentation < base then `Stop else + 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; + dynamic_switch = node.id; carry_on_data = of_bullet_val b } + | _ -> `Stop) entry_point + | _ -> assert false + +let dynamic_bullet { dynamic_switch = id; carry_on_data = b } = + match is_focused_goal_simple id with + | `Simple focused -> + `ValidBlock { + base_state = id; + goals_to_admit = focused; + recovery_command = Some (Vernacexpr.VernacBullet (to_bullet_val b)) + } + | `Not -> `Leaks + +let () = register_proof_block_delimiter + "bullet" static_bullet dynamic_bullet + +(* ******************** { block } ***************************************** *) + +let static_curly_brace ({ entry_point; prev_node } as view) = + assert(entry_point.ast = Vernacexpr.VernacEndSubproof); + crawl view (fun (nesting,prev) node -> + match node.ast with + | Vernacexpr.VernacSubproof _ when nesting = 0 -> + `Found { stop = entry_point.id; start = prev.id; + dynamic_switch = node.id; carry_on_data = unit_val } + | Vernacexpr.VernacSubproof _ -> + `Cont (nesting - 1,node) + | Vernacexpr.VernacEndSubproof -> + `Cont (nesting + 1,node) + | _ -> `Cont (nesting,node)) (-1, entry_point) + +let dynamic_curly_brace { dynamic_switch = id } = + match is_focused_goal_simple id with + | `Simple focused -> + `ValidBlock { + base_state = id; + goals_to_admit = focused; + recovery_command = Some Vernacexpr.VernacEndSubproof + } + | `Not -> `Leaks + +let () = register_proof_block_delimiter + "curly" static_curly_brace dynamic_curly_brace + +(* ***************** par: ************************************************* *) + +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; + dynamic_switch = pid; carry_on_data = unit_val } + +let dynamic_par { dynamic_switch = id } = + match is_focused_goal_simple id with + | `Simple focused -> + `ValidBlock { + base_state = id; + goals_to_admit = focused; + recovery_command = None; + } + | `Not -> `Leaks + +let () = register_proof_block_delimiter "par" static_par dynamic_par + +(* ***************** simple indentation *********************************** *) + +let static_indent ({ entry_point; prev_node } as view) = + Printf.eprintf "@%d\n" (Stateid.to_int entry_point.id); + match prev_node entry_point with + | None -> None + | Some last_tac -> + if last_tac.indentation <= entry_point.indentation then None + else + 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; + dynamic_switch = node.id; + carry_on_data = of_vernac_expr_val entry_point.ast } + ) last_tac + +let dynamic_indent { dynamic_switch = id; carry_on_data = e } = + Printf.eprintf "%s\n" (Stateid.to_string id); + match is_focused_goal_simple id with + | `Simple [] -> `Leaks + | `Simple focused -> + let but_last = List.tl (List.rev focused) in + `ValidBlock { + base_state = id; + goals_to_admit = but_last; + recovery_command = Some (to_vernac_expr_val e); + } + | `Not -> `Leaks + +let () = register_proof_block_delimiter "indent" static_indent dynamic_indent + diff --git a/stm/proofBlockDelimiter.mli b/stm/proofBlockDelimiter.mli new file mode 100644 index 0000000000..a55032a470 --- /dev/null +++ b/stm/proofBlockDelimiter.mli @@ -0,0 +1,41 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* This file implements proof block detection for: + - blocks delimited by { and } + - bullets with indentation + - par: terminator + + It exports utility functions to ease the development of other proof block + detection code. +*) + +(** A goal is simple if it nor depends on nor impacts on any other goal. + This function is used to detect, dynamically, if a proof block leaks, + i.e. if skipping it could impact other goals (like not instantiating their + type). `Simple carries the list of focused goals. +*) +val simple_goal : Evd.evar_map -> Goal.goal -> Goal.goal list -> bool +val is_focused_goal_simple : Stateid.t -> [ `Simple of Goal.goal list | `Not ] + +type 'a until = [ `Stop | `Found of Stm.static_block_declaration | `Cont of 'a ] + +(* Simpler function to crawl the document backward to detect the block. + * ?init is the entry point of the document view if not given *) +val crawl : + Stm.document_view -> ?init:Stm.document_node option -> + ('a -> Stm.document_node -> 'a until) -> 'a -> + Stm.static_block_declaration option + +(* Dummy value for static_block_declaration when no real value is needed *) +val unit_val : Stm.DynBlockData.t + +(* Bullets *) +val of_bullet_val : Vernacexpr.bullet -> Stm.DynBlockData.t +val to_bullet_val : Stm.DynBlockData.t -> Vernacexpr.bullet + diff --git a/stm/stm.ml b/stm/stm.ml index 3fe439cb20..f312e8539e 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -76,8 +76,14 @@ let interactive () = let async_proofs_workers_extra_env = ref [||] -type ast = { verbose : bool; loc : Loc.t; mutable expr : vernac_expr } -let pr_ast { expr } = pr_vernac expr +type aast = { + verbose : bool; + loc : Loc.t; + indentation : int; + strlen : int; + mutable expr : vernac_expr; (* mutable: Proof using hinted by aux file *) +} +let pr_ast { expr; indentation } = int indentation ++ str " " ++ pr_vernac expr let default_proof_mode () = Proof_global.get_default_proof_mode_name () @@ -114,17 +120,31 @@ let vernac_interp ?proof id ?route { verbose; loc; expr } = end (* Wrapper for Vernac.parse_sentence to set the feedback id *) -let vernac_parse ?newtip ?route eid s = +let indentation_of_string s = + let len = String.length s in + let rec aux n i precise = + if i >= len then 0, precise, len + else + match s.[i] with + | ' ' | '\t' -> aux (succ n) (succ i) precise + | '\n' | '\r' -> aux 0 (succ i) true + | _ -> n, precise, len in + aux 0 0 false + +let vernac_parse ?(indlen_prev=fun() -> 0) ?newtip ?route eid s = let feedback_id = if Option.is_empty newtip then Edit eid else State (Option.get newtip) in + let indentation, precise, strlen = indentation_of_string s in + let indentation = + if precise then indentation else indlen_prev () + indentation in set_id_for_feedback ?route feedback_id; let pa = Pcoq.Gram.parsable (Stream.of_string s) in Flags.with_option Flags.we_are_parsing (fun () -> try match Pcoq.Gram.entry_parse Pcoq.main_entry pa with | None -> raise (Invalid_argument "vernac_parse") - | Some ast -> ast + | Some (loc, ast) -> indentation, strlen, loc, ast with e when Errors.noncritical e -> let (e, info) = Errors.push e in let loc = Option.default Loc.ghost (Loc.get_loc info) in @@ -140,7 +160,7 @@ let update_global_env () = if Proof_global.there_are_pending_proofs () then Proof_global.update_global_env () -module Vcs_ = Vcs.Make(Stateid) +module Vcs_ = Vcs.Make(Stateid.Self) type future_proof = Proof_global.closed_proof_output Future.computation type proof_mode = string type depth = int @@ -150,22 +170,27 @@ type branch_type = | `Proof of proof_mode * depth | `Edit of proof_mode * Stateid.t * Stateid.t * vernac_qed_type * Vcs_.Branch.t ] +(* TODO 8.7 : split commands and tactics, since this type is too messy now *) type cmd_t = { - ctac : bool; (* is a tactic, needed by the 8.4 semantics of Undo *) + ctac : bool; (* is a tactic *) ceff : bool; (* is a side-effecting command in the middle of a proof *) - cast : ast; + cast : aast; cids : Id.t list; - cqueue : [ `MainQueue | `TacQueue of cancel_switch | `QueryQueue of cancel_switch | `SkipQueue ] } -type fork_t = ast * Vcs_.Branch.t * Vernacexpr.opacity_guarantee * Id.t list + cblock : proof_block_name option; + cqueue : [ `MainQueue + | `TacQueue of cancel_switch + | `QueryQueue of cancel_switch + | `SkipQueue ] } +type fork_t = aast * Vcs_.Branch.t * Vernacexpr.opacity_guarantee * Id.t list type qed_t = { - qast : ast; + qast : aast; keep : vernac_qed_type; mutable fproof : (future_proof * cancel_switch) option; brname : Vcs_.Branch.t; brinfo : branch_type Vcs_.branch_info } -type seff_t = ast option -type alias_t = Stateid.t * ast +type seff_t = aast option +type alias_t = Stateid.t * aast type transaction = | Cmd of cmd_t | Fork of fork_t @@ -177,40 +202,69 @@ type step = [ `Cmd of cmd_t | `Fork of fork_t * Stateid.t option | `Qed of qed_t * Stateid.t - | `Sideff of [ `Ast of ast * Stateid.t | `Id of Stateid.t ] + | `Sideff of [ `Ast of aast * Stateid.t | `Id of Stateid.t ] | `Alias of alias_t ] type visit = { step : step; next : Stateid.t } +let mkTransTac cast cblock cqueue = + Cmd { ctac = true; cast; cblock; cqueue; cids = []; ceff = false } +let mkTransCmd cast cids ceff cqueue = + Cmd { ctac = false; cast; cblock = None; cqueue; cids; ceff } (* Parts of the system state that are morally part of the proof state *) let summary_pstate = [ Evarutil.meta_counter_summary_name; Evd.evar_counter_summary_name; "program-tcc-table" ] -type state = { - system : States.state; - proof : Proof_global.state; - shallow : bool +type cached_state = + | Empty + | Error of Exninfo.iexn + | Valid of state +and state = { (* TODO: inline records in OCaml 4.03 *) + system : States.state; (* summary + libstack *) + proof : Proof_global.state; (* proof state *) + shallow : bool (* is the state trimmed down (libstack) *) } type branch = Vcs_.Branch.t * branch_type Vcs_.branch_info type backup = { mine : branch; others : branch list } -type 'vcs state_info = { (* Make private *) - mutable n_reached : int; - mutable n_goals : int; - mutable state : state option; +type 'vcs state_info = { (* TODO: Make this record private to VCS *) + mutable n_reached : int; (* debug cache: how many times was computed *) + mutable n_goals : int; (* open goals: indentation *) + mutable state : cached_state; (* state value *) mutable vcs_backup : 'vcs option * backup option; } let default_info () = - { n_reached = 0; n_goals = 0; state = None; vcs_backup = None,None } + { n_reached = 0; n_goals = 0; state = Empty; vcs_backup = None,None } + +module DynBlockData : Dyn.S = Dyn.Make(struct end) + +(* Clusters of nodes implemented as Dag properties. While Dag and Vcs impose + * no constraint on properties, here we impose boxes to be non overlapping. + * Such invariant makes sense for the current kinds of boxes (proof blocks and + * entire proofs) but may make no sense and dropped/refined in the future. + * Such invariant is useful to detect broken proof block detection code *) +type box = + | ProofTask of pt + | ProofBlock of static_block_declaration * proof_block_name +and pt = { (* TODO: inline records in OCaml 4.03 *) + lemma : Stateid.t; + qed : Stateid.t; +} +and static_block_declaration = { + start : Stateid.t; + stop : Stateid.t; + dynamic_switch : Stateid.t; + carry_on_data : DynBlockData.t; +} (* Functions that work on a Vcs with a specific branch type *) module Vcs_aux : sig - val proof_nesting : (branch_type, 't,'i) Vcs_.t -> int + val proof_nesting : (branch_type, 't,'i,'c) Vcs_.t -> int val find_proof_at_depth : - (branch_type, 't, 'i) Vcs_.t -> int -> + (branch_type, 't, 'i,'c) Vcs_.t -> int -> Vcs_.Branch.t * branch_type Vcs_.branch_info exception Expired - val visit : (branch_type, transaction,'i) Vcs_.t -> Vcs_.Dag.node -> visit + val visit : (branch_type, transaction,'i,'c) Vcs_.t -> Vcs_.Dag.node -> visit end = struct (* {{{ *) @@ -274,7 +328,7 @@ module VCS : sig pos : id; } - type vcs = (branch_type, transaction, vcs state_info) Vcs_.t + type vcs = (branch_type, transaction, vcs state_info, box) Vcs_.t val init : id -> unit @@ -288,30 +342,32 @@ module VCS : sig val rewrite_merge : id -> ours:transaction -> at:id -> Branch.t -> unit val delete_branch : Branch.t -> unit val commit : id -> transaction -> unit - val mk_branch_name : ast -> Branch.t + val mk_branch_name : aast -> Branch.t val edit_branch : Branch.t val branch : ?root:id -> ?pos:id -> Branch.t -> branch_type -> unit val reset_branch : Branch.t -> id -> unit - val reachable : id -> Vcs_.NodeSet.t + val reachable : id -> Stateid.Set.t val cur_tip : unit -> id val get_info : id -> vcs state_info - val reached : id -> bool -> unit + val reached : id -> unit val goals : id -> int -> unit - val set_state : id -> state -> unit - val get_state : id -> state option + val set_state : id -> cached_state -> unit + 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 create_cluster : id list -> qed:id -> start:id -> unit - val cluster_of : id -> (id * id) option - val delete_cluster_of : id -> unit + val create_proof_task_box : id list -> qed:id -> start:id -> unit + val create_proof_block : static_block_declaration -> string -> unit + val box_of : id -> box list + val delete_boxes_of : id -> unit + val proof_task_box_of : id -> pt option val proof_nesting : unit -> int val checkout_shallowest_proof_branch : unit -> unit - val propagate_sideff : replay:ast option -> unit + val propagate_sideff : replay:aast option -> unit val gc : unit -> unit @@ -327,7 +383,6 @@ end = struct (* {{{ *) include Vcs_ exception Expired = Vcs_aux.Expired - module StateidSet = Set.Make(Stateid) open Printf let print_dag vcs () = @@ -345,11 +400,11 @@ end = struct (* {{{ *) | Qed { qast } -> string_of_ppcmds (pr_ast qast) in let is_green id = match get_info vcs id with - | Some { state = Some _ } -> true + | Some { state = Valid _ } -> true | _ -> false in let is_red id = match get_info vcs id with - | Some s -> Int.equal s.n_reached ~-1 + | Some { state = Error _ } -> true | _ -> false in let head = current_branch vcs in let heads = @@ -369,8 +424,6 @@ end = struct (* {{{ *) let edge tr = sprintf "<<FONT POINT-SIZE=\"12\" FACE=\"sans\">%s</FONT>>" (quote (string_of_transaction tr)) in - let ids = ref StateidSet.empty in - let clus = Hashtbl.create 13 in let node_info id = match get_info vcs id with | None -> "" @@ -383,39 +436,71 @@ end = struct (* {{{ *) let nodefmt oc id = fprintf oc "%s [label=%s,style=filled,fillcolor=%s];\n" (node id) (node_info id) (color id) in - let add_to_clus_or_ids from cf = - match cf with - | None -> ids := StateidSet.add from !ids; false - | Some c -> Hashtbl.replace clus c - (try let n = Hashtbl.find clus c in from::n - with Not_found -> [from]); true in + + let ids = ref Stateid.Set.empty in + let boxes = ref [] in + (* Fill in *) + Dag.iter graph (fun from _ _ l -> + ids := Stateid.Set.add from !ids; + List.iter (fun box -> boxes := box :: !boxes) + (Dag.property_of graph from); + List.iter (fun (dest, _) -> + ids := Stateid.Set.add dest !ids; + List.iter (fun box -> boxes := box :: !boxes) + (Dag.property_of graph dest)) + l); + boxes := CList.sort_uniquize Dag.Property.compare !boxes; + let oc = open_out fname_dot in output_string oc "digraph states {\n"; Dag.iter graph (fun from cf _ l -> - let c1 = add_to_clus_or_ids from cf in List.iter (fun (dest, trans) -> - let c2 = add_to_clus_or_ids dest (Dag.cluster_of graph dest) in - fprintf oc "%s -> %s [xlabel=%s,labelfloat=%b];\n" - (node from) (node dest) (edge trans) (c1 && c2)) l + fprintf oc "%s -> %s [xlabel=%s,labelfloat=true];\n" + (node from) (node dest) (edge trans)) l ); - StateidSet.iter (nodefmt oc) !ids; - Hashtbl.iter (fun c nodes -> - fprintf oc "subgraph cluster_%s {\n" (Dag.Cluster.to_string c); - List.iter (nodefmt oc) nodes; - fprintf oc "color=blue; }\n" - ) clus; + + let contains b1 b2 = + Stateid.Set.subset + (Dag.Property.having_it b2) (Dag.Property.having_it b1) in + let same_box = Dag.Property.equal in + let outerboxes boxes = + List.filter (fun b -> + not (List.exists (fun b1 -> + not (same_box b1 b) && contains b1 b) boxes) + ) boxes in + let rec rec_print b = + boxes := CList.remove same_box b !boxes; + let sub_boxes = List.filter (contains b) (outerboxes !boxes) in + fprintf oc "subgraph cluster_%s {\n" (Dag.Property.to_string b); + List.iter rec_print sub_boxes; + Stateid.Set.iter (fun id -> + if Stateid.Set.mem id !ids then begin + ids := Stateid.Set.remove id !ids; + nodefmt oc id + end) + (Dag.Property.having_it b); + match Dag.Property.data b with + | ProofBlock ({ dynamic_switch = id }, lbl) -> + fprintf oc "label=\"%s (test:%s)\";\n" lbl (Stateid.to_string id); + fprintf oc "color=red; }\n" + | ProofTask _ -> fprintf oc "color=blue; }\n" + in + List.iter rec_print (outerboxes !boxes); + Stateid.Set.iter (nodefmt oc) !ids; + List.iteri (fun i (b,id) -> let shape = if Branch.equal head b then "box3d" else "box" in fprintf oc "b%d -> %s;\n" i (node id); fprintf oc "b%d [shape=%s,label=\"%s\"];\n" i shape (Branch.to_string b); ) heads; + output_string oc "}\n"; close_out oc; ignore(Sys.command ("dot -Tpdf -Gcharset=latin1 " ^ fname_dot ^ " -o" ^ fname_ps)) - type vcs = (branch_type, transaction, vcs state_info) t + type vcs = (branch_type, transaction, vcs state_info, box) t let vcs : vcs ref = ref (empty Stateid.dummy) let init id = @@ -452,13 +537,12 @@ end = struct (* {{{ *) | Some x -> x | None -> raise Vcs_aux.Expired let set_state id s = - (get_info id).state <- Some s; + (get_info id).state <- s; if Flags.async_proofs_is_master () then Hooks.(call state_ready id) let get_state id = (get_info id).state - let reached id b = + let reached id = let info = get_info id in - if b then info.n_reached <- info.n_reached + 1 - else info.n_reached <- -1 + info.n_reached <- info.n_reached + 1 let goals id n = (get_info id).n_goals <- n let cur_tip () = get_branch_pos (current_branch ()) @@ -508,9 +592,19 @@ end = struct (* {{{ *) let l = nodes_in_slice ~start ~stop in let copy_info v id = Vcs_.set_info v id - { (get_info id) with state = None; vcs_backup = None,None } in + { (get_info id) with state = Empty; vcs_backup = None,None } in let copy_info_w_state v id = Vcs_.set_info v id { (get_info id) with vcs_backup = None,None } in + let copy_proof_blockes v = + let nodes = Vcs_.Dag.all_nodes (Vcs_.dag v) in + let props = + Stateid.Set.fold (fun n pl -> Vcs_.property_of !vcs n @ pl) nodes [] in + let props = CList.sort_uniquize Vcs_.Dag.Property.compare props in + List.fold_left (fun v p -> + Vcs_.create_property v + (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 = List.fold_right (fun (id,tr) v -> @@ -518,28 +612,52 @@ end = struct (* {{{ *) let v = copy_info v id in v) l v in (* Stm should have reached the beginning of proof *) - assert (not (Option.is_empty (get_info start).state)); + assert (match (get_info start).state with Valid _ -> true | _ -> false); (* We put in the new dag the most recent state known to master *) let rec fill id = - if (get_info id).state = None then fill (Vcs_aux.visit v id).next - else copy_info_w_state v id in + 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 (* We put in the new dag the first state (since Qed shall run on it, * see check_task_aux) *) - copy_info_w_state v start + let v = copy_info_w_state v start in + copy_proof_blockes v let nodes_in_slice ~start ~stop = List.rev (List.map fst (nodes_in_slice ~start ~stop)) - let create_cluster l ~qed ~start = vcs := create_cluster !vcs l (qed,start) - let cluster_of id = Option.map Dag.Cluster.data (cluster_of !vcs id) - let delete_cluster_of id = - Option.iter (fun x -> vcs := delete_cluster !vcs x) (Vcs_.cluster_of !vcs id) + let topo_invariant l = + let all = List.fold_right Stateid.Set.add l Stateid.Set.empty in + List.for_all + (fun x -> + let props = property_of !vcs x in + let sets = List.map Dag.Property.having_it props in + List.for_all (fun s -> Stateid.Set.(subset s all || subset all s)) sets) + l + + let create_proof_task_box l ~qed ~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 + 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) + let delete_boxes_of id = + List.iter (fun x -> vcs := delete_property !vcs x) (property_of !vcs id) + let proof_task_box_of id = + match + CList.map_filter (function ProofTask x -> Some x | _ -> None) (box_of id) + with + | [] -> None + | [x] -> Some x + | _ -> anomaly (str "node with more than 1 proof task box") let gc () = let old_vcs = !vcs in let new_vcs, erased_nodes = gc old_vcs in - Vcs_.NodeSet.iter (fun id -> + Stateid.Set.iter (fun id -> match (Vcs_aux.visit old_vcs id).step with | `Qed ({ fproof = Some (_, cancel_switch) }, _) | `Cmd { cqueue = `TacQueue cancel_switch } @@ -596,7 +714,10 @@ end = struct (* {{{ *) end (* }}} *) let state_of_id id = - try `Valid (VCS.get_info id).state + try match (VCS.get_info id).state with + | Valid s -> `Valid (Some s) + | Error (e,_) -> `Error e + | Empty -> `Valid None with VCS.Expired -> `Expired @@ -616,6 +737,7 @@ module State : sig val install_cached : Stateid.t -> unit val is_cached : ?cache:Summary.marshallable -> Stateid.t -> bool + val is_cached_and_valid : ?cache:Summary.marshallable -> Stateid.t -> bool val exn_on : Stateid.t -> ?valid:Stateid.t -> iexn -> iexn @@ -661,51 +783,60 @@ end = struct (* {{{ *) proof, Summary.project_summary (States.summary_of_state system) summary_pstate - let freeze marshallable id = VCS.set_state id (freeze_global_state marshallable) + let freeze marshallable id = + VCS.set_state id (Valid (freeze_global_state marshallable)) + let freeze_invalid id iexn = VCS.set_state id (Error iexn) - let is_cached ?(cache=`No) id = + let is_cached ?(cache=`No) id only_valid = if Stateid.equal id !cur_id then try match VCS.get_info id with - | { state = None } when cache = `Yes -> freeze `No id; true - | { state = None } when cache = `Shallow -> freeze `Shallow id; true + | { state = Empty } when cache = `Yes -> freeze `No id; true + | { state = Empty } when cache = `Shallow -> freeze `Shallow id; true | _ -> true with VCS.Expired -> false else try match VCS.get_info id with - | { state = Some _ } -> true - | _ -> false + | { state = Empty } -> false + | { state = Valid _ } -> true + | { state = Error _ } -> not only_valid with VCS.Expired -> false + let is_cached_and_valid ?cache id = is_cached ?cache id true + let is_cached ?cache id = is_cached ?cache id false + let install_cached id = - if Stateid.equal id !cur_id then () else (* optimization *) - let s = - match VCS.get_info id with - | { state = Some s } -> s - | _ -> anomaly (str "unfreezing a non existing state") in - unfreeze_global_state s; cur_id := id + match VCS.get_info id with + | { state = Valid s } -> + if Stateid.equal id !cur_id then () (* optimization *) + else begin unfreeze_global_state s; cur_id := id end + | { state = Error ie } -> cur_id := id; Exninfo.iraise ie + | _ -> + (* coqc has a 1 slot cache and only for valid states *) + if interactive () = `No && Stateid.equal id !cur_id then () + else anomaly (str "installing a non cached state") let get_cached id = try match VCS.get_info id with - | { state = Some s } -> s + | { state = Valid s } -> s | _ -> anomaly (str "not a cached state") with VCS.Expired -> anomaly (str "not a cached state (expired)") let assign id what = - if VCS.get_state id <> None then () else + if VCS.get_state id <> Empty then () else try match what with | `Full s -> let s = try let prev = (VCS.visit id).next in - if is_cached prev + if is_cached_and_valid prev then { s with proof = Proof_global.copy_terminators ~src:(get_cached prev).proof ~tgt:s.proof } else s with VCS.Expired -> s in - VCS.set_state id s + VCS.set_state id (Valid s) | `Proof(ontop,(pstate,counters)) -> - if is_cached ontop then + if is_cached_and_valid ontop then let s = get_cached ontop in let s = { s with proof = Proof_global.copy_terminators ~src:s.proof ~tgt:pstate } in @@ -714,7 +845,7 @@ end = struct (* {{{ *) (Summary.surgery_summary (States.summary_of_state s.system) counters) } in - VCS.set_state id s + VCS.set_state id (Valid s) with VCS.Expired -> () let exn_on id ?valid (e, info) = @@ -753,20 +884,22 @@ end = struct (* {{{ *) cur_id := id; if feedback_processed then Hooks.(call state_computed id ~in_cache:false); - VCS.reached id true; + VCS.reached id; if Proof_global.there_are_pending_proofs () then VCS.goals id (Proof_global.get_open_goals ()) with e -> let (e, info) = Errors.push e in let good_id = !cur_id in - cur_id := Stateid.dummy; - VCS.reached id false; - Hooks.(call unreachable_state id (e, info)); - match Stateid.get info, safe_id with - | None, None -> iraise (exn_on id ~valid:good_id (e, info)) - | None, Some good_id -> iraise (exn_on id ~valid:good_id (e, info)) - | Some _, None -> iraise (e, info) - | Some (_,at), Some id -> iraise (e, Stateid.add info ~valid:id at) + VCS.reached id; + let ie = + match Stateid.get info, safe_id with + | None, None -> (exn_on id ~valid:good_id (e, info)) + | None, Some good_id -> (exn_on id ~valid:good_id (e, info)) + | Some _, None -> (e, info) + | Some (_,at), Some id -> (e, Stateid.add info ~valid:id at) in + if cache = `Yes || cache = `Shallow then freeze_invalid id ie; + Hooks.(call unreachable_state id ie); + Exninfo.iraise ie end (* }}} *) @@ -842,7 +975,7 @@ end = struct (* {{{ *) let back_safe () = let id = fold_until (fun n (id,_,_,_,_) -> - if n >= 0 && State.is_cached id then `Stop id else `Cont (succ n)) + if n >= 0 && State.is_cached_and_valid id then `Stop id else `Cont (succ n)) 0 (VCS.get_branch_pos (VCS.current_branch ())) in backto id @@ -941,6 +1074,75 @@ let _ = Errors.register_handler (function | RemoteException ppcmd -> ppcmd | _ -> raise Unhandled) +(****************** proof structure for error recovery ************************) +(******************************************************************************) + +type document_node = { + indentation : int; + ast : Vernacexpr.vernac_expr; + id : Stateid.t; +} + +type document_view = { + entry_point : document_node; + prev_node : document_node -> document_node option; +} + +type static_block_detection = + document_view -> static_block_declaration option + +type recovery_action = { + base_state : Stateid.t; + goals_to_admit : Goal.goal list; + recovery_command : Vernacexpr.vernac_expr option; +} + +type dynamic_block_error_recovery = + static_block_declaration -> [ `ValidBlock of recovery_action | `Leaks ] + +let proof_block_delimiters = ref [] + +let register_proof_block_delimiter name static dynamic = + if List.mem_assoc name !proof_block_delimiters then + Errors.errorlabstrm "STM" (str "Duplicate block delimiter " ++ str name); + proof_block_delimiters := (name, (static,dynamic)) :: !proof_block_delimiters + +let mk_doc_node id = function + | { step = `Cmd { ctac; cast = { indentation; expr }}; next } when ctac -> + Some { indentation; ast = expr; id } + | { step = `Sideff (`Ast ({ indentation; expr }, _)); next } -> + Some { indentation; ast = expr; id } + | _ -> None +let prev_node { id } = + let id = (VCS.visit id).next in + mk_doc_node id (VCS.visit id) +let cur_node id = mk_doc_node id (VCS.visit id) + +let is_block_name_enabled name = + match !Flags.async_proofs_tac_error_resilience with + | `None -> false + | `All -> true + | `Only l -> List.mem name l + +let detect_proof_block id name = + let name = match name with None -> "indent" | Some x -> x in + if is_block_name_enabled name && + (if Flags.async_proofs_is_master () then + !Flags.async_proofs_mode != Flags.APoff else true) + then + match cur_node id with + | None -> () + | Some entry_point -> try + let static, _ = List.assoc name !proof_block_delimiters in + begin match static { prev_node; entry_point } with + | None -> () + | Some ({ start; stop } as decl) -> + VCS.create_proof_block decl name + end + with Not_found -> + Errors.errorlabstrm "STM" + (str "Unknown proof block delimiter " ++ str name) + (****************************** THE SCHEDULER *********************************) (******************************************************************************) @@ -1117,7 +1319,7 @@ end = struct (* {{{ *) Lemmas.(standard_proof_terminator [] (mk_hook (fun _ _ -> ()))) in vernac_interp stop ~proof:(pobject, terminator) - { verbose = false; loc; + { verbose = false; loc; indentation = 0; strlen = 0; expr = (VernacEndProof (Proved (Opaque None,None))) }) in ignore(Future.join checked_proof); end; @@ -1133,7 +1335,7 @@ end = struct (* {{{ *) let e_msg = iprint (e, info) in prerr_endline (fun () -> "failed with the following exception:"); prerr_endline (fun () -> string_of_ppcmds e_msg); - let e_safe_states = List.filter State.is_cached my_states in + let e_safe_states = List.filter State.is_cached_and_valid my_states in RespError { e_error_at; e_safe_id; e_msg; e_safe_states } let perform_states query = @@ -1151,12 +1353,12 @@ end = struct (* {{{ *) let prev = try let { next = prev; step } = VCS.visit id in - if State.is_cached prev && List.mem prev seen + if State.is_cached_and_valid prev && List.mem prev seen then Some (prev, State.get_cached prev, step) else None with VCS.Expired -> None in let this = - if State.is_cached id then Some (State.get_cached id) else None in + if State.is_cached_and_valid id then Some (State.get_cached id) else None in match prev, this with | _, None -> None | Some (prev, o, `Cmd { cast = { expr }}), Some n @@ -1258,7 +1460,7 @@ end = struct (* {{{ *) * looking at the ones that happen to be present in the current env *) Reach.known_state ~cache:`No start; vernac_interp stop ~proof - { verbose = false; loc; + { verbose = false; loc; indentation = 0; strlen = 0; expr = (VernacEndProof (Proved (Opaque None,None))) }; `OK proof end @@ -1411,7 +1613,7 @@ and TacTask : sig t_state : Stateid.t; t_state_fb : Stateid.t; t_assign : output Future.assignement -> unit; - t_ast : int * ast; + t_ast : int * aast; t_goal : Goal.goal; t_kill : unit -> unit; t_name : string } @@ -1428,7 +1630,7 @@ end = struct (* {{{ *) t_state : Stateid.t; t_state_fb : Stateid.t; t_assign : output Future.assignement -> unit; - t_ast : int * ast; + t_ast : int * aast; t_goal : Goal.goal; t_kill : unit -> unit; t_name : string } @@ -1437,7 +1639,7 @@ end = struct (* {{{ *) r_state : Stateid.t; r_state_fb : Stateid.t; r_document : VCS.vcs option; - r_ast : int * ast; + r_ast : int * aast; r_goal : Goal.goal; r_name : string } @@ -1467,8 +1669,7 @@ end = struct (* {{{ *) match resp with | RespBuiltSubProof o -> t_assign (`Val o); `Stay ((),[]) | RespError msg -> - let info = Stateid.add ~valid:t_state Exninfo.null t_state_fb in - let e = (RemoteException msg, info) in + let e = (RemoteException msg, Exninfo.null) in t_assign (`Exn e); t_kill (); `Stay ((),[]) @@ -1496,7 +1697,7 @@ end = struct (* {{{ *) List.for_all (Context.Named.Declaration.for_all (Evarutil.is_ground_term sigma0)) Evd.(evar_context g)) then - Errors.errorlabstrm "Stm" (strbrk("the par: goal selector supports ground "^ + Errors.errorlabstrm "STM" (strbrk("the par: goal selector supports ground "^ "goals only")) else begin let (i, ast) = r_ast in @@ -1504,12 +1705,12 @@ end = struct (* {{{ *) vernac_interp r_state_fb ast; let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in match Evd.(evar_body (find sigma r_goal)) with - | Evd.Evar_empty -> Errors.errorlabstrm "Stm" (str "no progress") + | Evd.Evar_empty -> Errors.errorlabstrm "STM" (str "no progress") | Evd.Evar_defined t -> let t = Evarutil.nf_evar sigma t in if Evarutil.is_ground_term sigma t then t, Evd.evar_universe_context sigma - else Errors.errorlabstrm "Stm" (str"The solution is not ground") + else Errors.errorlabstrm "STM" (str"The solution is not ground") end) () in RespBuiltSubProof (t,uc) @@ -1523,13 +1724,15 @@ end (* }}} *) and Partac : sig val vernac_interp : - cancel_switch -> int -> Stateid.t -> Stateid.t -> ast -> unit + cancel_switch -> int -> Stateid.t -> Stateid.t -> aast -> unit end = struct (* {{{ *) module TaskQueue = AsyncTaskQueue.MakeQueue(TacTask) - let vernac_interp cancel nworkers safe_id id { verbose; loc; expr = e } = + let vernac_interp cancel nworkers safe_id id + { indentation; verbose; loc; expr = e; strlen } + = let e, time, fail = let rec find time fail = function | VernacTime (_,e) | VernacRedirect (_,(_,e)) -> find true fail e @@ -1546,7 +1749,7 @@ end = struct (* {{{ *) Future.create_delegate ~name:(Printf.sprintf "subgoal %d" i) (State.exn_on id ~valid:safe_id) in - let t_ast = (i, { verbose; loc; expr = e }) in + let t_ast = (i, { indentation; verbose; loc; expr = e; strlen }) in let t_name = Goal.uid g in TaskQueue.enqueue_task queue ({ t_state = safe_id; t_state_fb = id; @@ -1580,16 +1783,16 @@ end (* }}} *) and QueryTask : sig - type task = { t_where : Stateid.t; t_for : Stateid.t ; t_what : ast } + type task = { t_where : Stateid.t; t_for : Stateid.t ; t_what : aast } include AsyncTaskQueue.Task with type task := task end = struct (* {{{ *) type task = - { t_where : Stateid.t; t_for : Stateid.t ; t_what : ast } + { t_where : Stateid.t; t_for : Stateid.t ; t_what : aast } type request = - { r_where : Stateid.t ; r_for : Stateid.t ; r_what : ast; r_doc : VCS.vcs } + { r_where : Stateid.t ; r_for : Stateid.t ; r_what : aast; r_doc : VCS.vcs } type response = unit let name = ref "queryworker" @@ -1635,7 +1838,7 @@ end (* }}} *) and Query : sig val init : unit -> unit - val vernac_interp : cancel_switch -> Stateid.t -> Stateid.t -> ast -> unit + val vernac_interp : cancel_switch -> Stateid.t -> Stateid.t -> aast -> unit end = struct (* {{{ *) @@ -1672,9 +1875,9 @@ let async_policy () = (!compilation_mode = BuildVio || !async_proofs_mode <> APoff) let delegate name = - let time = get_hint_bp_time name in - time >= 1.0 || !Flags.compilation_mode = Flags.BuildVio - || !Flags.async_proofs_full + get_hint_bp_time name >= !Flags.async_proofs_delegation_threshold + || !Flags.compilation_mode = Flags.BuildVio + || !Flags.async_proofs_full let collect_proof keep cur hd brkind id = prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id); @@ -1724,7 +1927,7 @@ let collect_proof keep cur hd brkind id = let name = name ids in `ASync (parent last,proof_using_ast last,accn,name,delegate name) | `Fork((_, hd', GuaranteesOpacity, ids), _) when - has_proof_no_using last && not (State.is_cached (parent last)) && + has_proof_no_using last && not (State.is_cached_and_valid (parent last)) && !Flags.compilation_mode = Flags.BuildVio -> assert (VCS.Branch.equal hd hd'||VCS.Branch.equal hd VCS.edit_branch); (try @@ -1760,7 +1963,7 @@ let collect_proof keep cur hd brkind id = let rc = collect (Some cur) [] id in if is_empty rc then make_sync `AlreadyEvaluated rc else if (keep == VtKeep || keep == VtKeepAsAxiom) && - (not(State.is_cached id) || !Flags.async_proofs_full) + (not(State.is_cached_and_valid id) || !Flags.async_proofs_full) then check_policy rc else make_sync `AlreadyEvaluated rc @@ -1790,6 +1993,71 @@ let log_processing_sync id name reason = log_string Printf.(sprintf let wall_clock_last_fork = ref 0.0 let known_state ?(redefine_qed=false) ~cache id = + + let error_absorbing_tactic id blockname exn = + (* We keep the static/dynamic part of block detection separate, since + the static part could be performed earlier. As of today there is + no advantage in doing so since no UI can exploit such piece of info *) + detect_proof_block id blockname; + + let boxes = VCS.box_of id in + let valid_boxes = CList.map_filter (function + | ProofBlock ({ stop } as decl, name) when Stateid.equal stop id -> + Some (decl, name) + | _ -> None) boxes in + assert(List.length valid_boxes < 2); + if valid_boxes = [] then iraise exn + else + let decl, name = List.hd valid_boxes in + try + let _, dynamic_check = List.assoc name !proof_block_delimiters in + match dynamic_check decl with + | `Leaks -> iraise exn + | `ValidBlock { base_state; goals_to_admit; recovery_command } -> begin + let tac = + let open Proofview.Notations in + Proofview.Goal.nf_enter { enter = fun gl -> + if CList.mem_f Evar.equal + (Proofview.Goal.goal gl) goals_to_admit then + Proofview.give_up else Proofview.tclUNIT () + } in + match (VCS.get_info base_state).state with + | Valid { proof } -> + Proof_global.unfreeze proof; + Proof_global.with_current_proof (fun _ p -> + feedback ~id:(State id) Feedback.AddedAxiom; + fst (Pfedit.solve Vernacexpr.SelectAll None tac p), ()); + Option.iter (fun expr -> vernac_interp id { + verbose = true; loc = Loc.ghost; expr; indentation = 0; + strlen = 0 }) + recovery_command + | _ -> assert false + end + with Not_found -> + Errors.errorlabstrm "STM" + (str "Unknown proof block delimiter " ++ str name) + in + + (* Absorb tactic errors from f () *) + let resilient_tactic id blockname f = + if !Flags.async_proofs_tac_error_resilience = `None || + (Flags.async_proofs_is_master () && + !Flags.async_proofs_mode = Flags.APoff) + then f () + else + try f () + with e when Errors.noncritical e -> + let ie = Errors.push e in + error_absorbing_tactic id blockname ie in + (* Absorb errors from f x *) + let resilient_command f x = + if not !Flags.async_proofs_cmd_error_resilience || + (Flags.async_proofs_is_master () && + !Flags.async_proofs_mode = Flags.APoff) + then f x + else + try f x + with e when Errors.noncritical e -> () in (* ugly functions to process nested lemmas, i.e. hard to reproduce * side effects *) @@ -1808,9 +2076,9 @@ let known_state ?(redefine_qed=false) ~cache id = and reach ?(redefine_qed=false) ?(cache=cache) id = prerr_endline (fun () -> "reaching: " ^ Stateid.to_string id); if not redefine_qed && State.is_cached ~cache id then begin - State.install_cached id; Hooks.(call state_computed id ~in_cache:true); - prerr_endline (fun () -> "reached (cache)") + prerr_endline (fun () -> "reached (cache)"); + State.install_cached id end else let step, cache_step, feedback_processed = let view = VCS.visit id in @@ -1820,29 +2088,38 @@ let known_state ?(redefine_qed=false) ~cache id = ), cache, true | `Cmd { cast = x; cqueue = `SkipQueue } -> (fun () -> reach view.next), cache, true - | `Cmd { cast = x; cqueue = `TacQueue cancel } -> (fun () -> - reach ~cache:`Shallow view.next; - Hooks.(call tactic_being_run true); - Partac.vernac_interp - cancel !Flags.async_proofs_n_tacworkers view.next id x; - Hooks.(call tactic_being_run false) + | `Cmd { cast = x; cqueue = `TacQueue cancel; cblock } -> (fun () -> + resilient_tactic id cblock (fun () -> + reach ~cache:`Shallow view.next; + Hooks.(call tactic_being_run true); + Partac.vernac_interp + cancel !Flags.async_proofs_n_tacworkers view.next id x; + Hooks.(call tactic_being_run false)) ), cache, true | `Cmd { cast = x; cqueue = `QueryQueue cancel } when Flags.async_proofs_is_master () -> (fun () -> reach view.next; Query.vernac_interp cancel view.next id x ), cache, false - | `Cmd { cast = x; ceff = eff; ctac } -> (fun () -> - reach view.next; - if ctac then Hooks.(call tactic_being_run true); + | `Cmd { cast = x; ceff = eff; ctac = true; cblock } -> (fun () -> + resilient_tactic id cblock (fun () -> + reach view.next; + Hooks.(call tactic_being_run true); + vernac_interp id x; + Hooks.(call tactic_being_run false)); + if eff then update_global_env () + ), (if eff then `Yes else cache), true + | `Cmd { cast = x; ceff = eff } -> (fun () -> + resilient_command reach view.next; vernac_interp id x; - if ctac then Hooks.(call tactic_being_run false); - if eff then update_global_env ()), (if eff then `Yes else cache), true + if eff then update_global_env () + ), (if eff then `Yes else cache), true | `Fork ((x,_,_,_), None) -> (fun () -> - reach view.next; vernac_interp id x; + resilient_command reach view.next; + vernac_interp id x; wall_clock_last_fork := Unix.gettimeofday () ), `Yes, true - | `Fork ((x,_,_,_), Some prev) -> (fun () -> + | `Fork ((x,_,_,_), Some prev) -> (fun () -> (* nested proof *) reach ~cache:`Shallow prev; reach view.next; (try vernac_interp id x; @@ -1859,7 +2136,7 @@ let known_state ?(redefine_qed=false) ~cache id = let drop_pt = keep == VtKeepAsAxiom in let stop, exn_info, loc = eop, (id, eop), x.loc in log_processing_async id name; - VCS.create_cluster nodes ~qed:id ~start; + VCS.create_proof_task_box nodes ~qed:id ~start; begin match brinfo, qed.fproof with | { VCS.kind = `Edit _ }, None -> assert false | { VCS.kind = `Edit (_,_,_, okeep, _) }, Some (ofp, cancel) -> @@ -2112,10 +2389,11 @@ let snapshot_vio ldir long_f_dot_v = let reset_task_queue = Slaves.reset_task_queue (* Document building *) -let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = +let process_transaction ?(newtip=Stateid.fresh ()) ~tty + ({ verbose; loc; expr } as x) c + = let warn_if_pos a b = if b then msg_warning(pr_ast a ++ str" should not be part of a script") in - let v, x = expr, { verbose = verbose; loc; expr } in prerr_endline (fun () -> "{{{ processing: "^ string_of_ppcmds (pr_ast x)); let vcs = VCS.backup () in try @@ -2170,7 +2448,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = | VtQuery (false,(report_id,route)), VtNow when tty = true -> finish (); (try Future.purify (vernac_interp report_id ~route) - { verbose = true; loc; expr } + {x with verbose = true } with e when Errors.noncritical e -> let e = Errors.push e in iraise (State.exn_on report_id e)); `Ok @@ -2189,8 +2467,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = may_pierce_opaque x then `SkipQueue else `MainQueue in - VCS.commit id (Cmd { - ctac=false;ceff=false;cast = x; cids = []; cqueue = queue }); + VCS.commit id (mkTransCmd x [] false queue); Backtrack.record (); if w == VtNow then finish (); `Ok | VtQuery (false,_), VtLater -> anomaly(str"classifier: VtQuery + VtLater must imply part_of_script") @@ -2213,8 +2490,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = anomaly(str"VtProofMode must be executed VtNow") | VtProofMode mode, VtNow -> let id = VCS.new_node ~id:newtip () in - VCS.commit id (Cmd { - ctac=false;ceff=false;cast = x;cids=[];cqueue = `MainQueue}); + VCS.commit id (mkTransCmd x [] false `MainQueue); List.iter (fun bn -> match VCS.get_branch bn with | { VCS.root; kind = `Master; pos } -> () @@ -2229,11 +2505,14 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = Backtrack.record (); finish (); `Ok - | VtProofStep paral, w -> + | VtProofStep { parallel; proof_block_detection = cblock }, w -> let id = VCS.new_node ~id:newtip () in - let queue = if paral then `TacQueue (ref false) else `MainQueue in - VCS.commit id (Cmd { - ctac = true;ceff = false;cast = x;cids = [];cqueue = queue }); + let queue = if parallel then `TacQueue (ref false) else `MainQueue in + VCS.commit id (mkTransTac x cblock queue); + (* Static proof block detection delayed until an error really occurs. + If/when and UI will make something useful with this piece of info, + detection should occur here. + detect_proof_block id cblock; *) Backtrack.record (); if w == VtNow then finish (); `Ok | VtQed keep, w -> let valid = if tty then Some(VCS.get_branch_pos head) else None in @@ -2250,8 +2529,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in let id = VCS.new_node ~id:newtip () in VCS.checkout VCS.Branch.master; - VCS.commit id (Cmd { - ctac=false;ceff=in_proof;cast=x;cids=l;cqueue=`MainQueue }); + VCS.commit id (mkTransCmd x l in_proof `MainQueue); (* We can't replay a Definition since universes may be differently * inferred. This holds in Coq >= 8.5 *) let replay = match x.expr with @@ -2286,8 +2564,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = VCS.branch bname (`Proof (proof_mode, VCS.proof_nesting () + 1)); Proof_global.activate_proof_mode proof_mode; end else begin - VCS.commit id (Cmd { - ctac=false;ceff=in_proof;cast=x;cids=[];cqueue=`MainQueue }); + VCS.commit id (mkTransCmd x [] in_proof `MainQueue); (* We hope it can be replayed, but we can't really know *) VCS.propagate_sideff ~replay:(Some x); VCS.checkout_shallowest_proof_branch (); @@ -2299,11 +2576,11 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = anomaly(str"classifier: VtUnknown must imply VtNow") end in (* Proof General *) - begin match v with + begin match expr with | VernacStm (PGLast _) -> if not (VCS.Branch.equal head VCS.Branch.master) then vernac_interp Stateid.dummy - { verbose = true; loc = Loc.ghost; + { verbose = true; loc = Loc.ghost; indentation = 0; strlen = 0; expr = VernacShow (ShowGoal OpenSubgoals) } | _ -> () end; @@ -2324,19 +2601,30 @@ let get_ast id = let stop_worker n = Slaves.cancel_worker n +(* You may need to know the len + indentation of previous command to compute + * the indentation of the current one. + * Eg. foo. bar. + * Here bar is indented of the indentation of foo + its strlen (4) *) +let ind_len_of id = + if Stateid.equal id Stateid.initial then 0 + else match (VCS.visit id).step with + | `Cmd { ctac = true; cast = { indentation; strlen } } -> + indentation + strlen + | _ -> 0 + let add ~ontop ?newtip ?(check=ignore) verb eid s = let cur_tip = VCS.cur_tip () in - if Stateid.equal ontop cur_tip then begin - let _, ast as loc_ast = vernac_parse ?newtip eid s in - check(loc_ast); - let clas = classify_vernac ast in - match process_transaction ?newtip ~tty:false verb clas loc_ast with - | `Ok -> VCS.cur_tip (), `NewTip - | `Unfocus qed_id -> qed_id, `Unfocus (VCS.cur_tip ()) - end else begin + if not (Stateid.equal ontop cur_tip) then (* For now, arbitrary edits should be announced with edit_at *) - anomaly(str"Not yet implemented, the GUI should not try this") - end + anomaly(str"Not yet implemented, the GUI should not try this"); + let indentation, strlen, loc, ast = + vernac_parse ~indlen_prev:(fun () -> ind_len_of ontop) ?newtip eid s in + check(loc,ast); + let clas = classify_vernac ast in + let aast = { verbose = verb; indentation; strlen; loc; expr = ast } in + match process_transaction ?newtip ~tty:false aast clas with + | `Ok -> VCS.cur_tip (), `NewTip + | `Unfocus qed_id -> qed_id, `Unfocus (VCS.cur_tip ()) let set_perspective id_list = Slaves.set_perspective id_list @@ -2351,15 +2639,15 @@ let query ~at ?(report_with=(Stateid.dummy,default_route)) s = if Stateid.equal at Stateid.dummy then finish () else Reach.known_state ~cache:`Yes at; let newtip, route = report_with in - let _, ast as loc_ast = vernac_parse ~newtip ~route 0 s in + let indentation, strlen, loc, ast = vernac_parse ~newtip ~route 0 s in let clas = classify_vernac ast in + let aast = { verbose = true; indentation; strlen; loc; expr = ast } in match clas with | VtStm (w,_), _ -> - ignore(process_transaction - ~tty:false true (VtStm (w,false), VtNow) loc_ast) + ignore(process_transaction ~tty:false aast (VtStm (w,false), VtNow)) | _ -> ignore(process_transaction - ~tty:false true (VtQuery (false,report_with), VtNow) loc_ast)) + ~tty:false aast (VtQuery (false,report_with), VtNow))) s let edit_at id = @@ -2384,7 +2672,7 @@ let edit_at id = | _ -> assert false in let is_ancestor_of_cur_branch id = - Vcs_.NodeSet.mem id + Stateid.Set.mem id (VCS.reachable (VCS.get_branch_pos (VCS.current_branch ()))) in let has_failed qed_id = match VCS.visit qed_id with @@ -2399,13 +2687,13 @@ let edit_at id = | { next } -> master_for_br root next in let reopen_branch start at_id mode qed_id tip old_branch = let master_id, cancel_switch, keep = - (* Hum, this should be the real start_id in the clusted and not next *) + (* Hum, this should be the real start_id in the cluster and not next *) match VCS.visit qed_id with | { step = `Qed ({ fproof = Some (_,cs); keep },_) } -> start, cs, keep - | _ -> anomaly (str "Cluster not ending with Qed") in + | _ -> anomaly (str "ProofTask not ending with Qed") in VCS.branch ~root:master_id ~pos:id VCS.edit_branch (`Edit (mode, qed_id, master_id, keep, old_branch)); - VCS.delete_cluster_of id; + VCS.delete_boxes_of id; cancel_switch := true; Reach.known_state ~cache:(interactive ()) id; VCS.checkout_shallowest_proof_branch (); @@ -2419,14 +2707,14 @@ let edit_at id = let { mine = brname, brinfo; others } = Backtrack.branches_of id in List.iter (fun (name,{ VCS.kind = k; root; pos }) -> if not(VCS.Branch.equal name VCS.Branch.master) && - Vcs_.NodeSet.mem root ancestors then + Stateid.Set.mem root ancestors then VCS.branch ~root ~pos name k) others; VCS.reset_branch VCS.Branch.master (master_for_br brinfo.VCS.root id); VCS.branch ~root:brinfo.VCS.root ~pos:brinfo.VCS.pos (Option.default brname bn) (no_edit brinfo.VCS.kind); - VCS.delete_cluster_of id; + VCS.delete_boxes_of id; VCS.gc (); VCS.print (); if not !Flags.async_proofs_full then @@ -2441,14 +2729,14 @@ let edit_at id = | Some{ mine = bn, { VCS.kind = `Proof(m,_) }} -> Some(m,bn) | Some{ mine = _, { VCS.kind = `Edit(m,_,_,_,bn) }} -> Some (m,bn) | _ -> None in - match focused, VCS.cluster_of id, branch_info with + match focused, VCS.proof_task_box_of id, branch_info with | _, Some _, None -> assert false - | false, Some (qed_id,start), Some(mode,bn) -> + | false, Some { qed = qed_id ; lemma = start }, Some(mode,bn) -> let tip = VCS.cur_tip () in if has_failed qed_id && is_pure qed_id && not !Flags.async_proofs_never_reopen_branch then reopen_branch start id mode qed_id tip bn else backto id (Some bn) - | true, Some (qed_id,_), Some(mode,bn) -> + | true, Some { qed = qed_id }, Some(mode,bn) -> if on_cur_branch id then begin assert false end else if is_ancestor_of_cur_branch id then begin @@ -2491,9 +2779,10 @@ let restore d = VCS.restore d (*********************** TTY API (PG, coqtop, coqc) ***************************) (******************************************************************************) -let interp verb (_,e as lexpr) = +let interp verb (loc,e) = let clas = classify_vernac e in - let rc = process_transaction ~tty:true verb clas lexpr in + let aast = { verbose = verb; indentation = 0; strlen = 0; loc; expr = e } in + let rc = process_transaction ~tty:true aast clas in if rc <> `Ok then anomaly(str"tty loop can't be mixed with the STM protocol"); if interactive () = `Yes || (!Flags.async_proofs_mode = Flags.APoff && diff --git a/stm/stm.mli b/stm/stm.mli index 6ffe0beb44..37ec1f0a13 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -20,7 +20,9 @@ open Loc The sentence [s] is parsed in the state [ontop]. If [newtip] is provided, then the returned state id is guaranteed to be [newtip] *) -val add : ontop:Stateid.t -> ?newtip:Stateid.t -> ?check:(vernac_expr located -> unit) -> +val add : + ontop:Stateid.t -> ?newtip:Stateid.t -> + ?check:(vernac_expr located -> unit) -> bool -> edit_id -> string -> Stateid.t * [ `NewTip | `Unfocus of Stateid.t ] @@ -96,6 +98,82 @@ module ProofTask : AsyncTaskQueue.Task module TacTask : AsyncTaskQueue.Task module QueryTask : AsyncTaskQueue.Task +(** document structure customization *************************************** **) + +(* A proof block delimiter defines a syntactic delimiter for sub proofs + that, when contain an error, do not impact the rest of the proof. + While checking a proof, if an error occurs in a (valid) block then + processing can skip the entire block and go on to give feedback + on the rest of the proof. + + static_block_detection and dynamic_block_validation are run when + the closing block marker is parsed/executed respectively. + + static_block_detection is for example called when "}" is parsed and + declares a block containing all proof steps between it and the matching + "{". + + dynamic_block_validation is called when an error "crosses" the "}" statement. + Depending on the nature of the goal focused by "{" the block may absorb the + error or not. For example if the focused goal occurs in the type of + another goal, then the block is leaky. + Note that one can design proof commands that need no dynamic validation. + + Example of document: + + .. { tac1. tac2. } .. + + Corresponding DAG: + + .. (3) <-- { -- (4) <-- tac1 -- (5) <-- tac2 -- (6) <-- } -- (7) .. + + Declaration of block [-------------------------------------------] + + start = 5 the first state_id that could fail in the block + stop = 7 the node that may absorb the error + dynamic_switch = 4 dynamic check on this node + carry_on_data = () no need to carry extra data from static to dynamic + checks +*) + +module DynBlockData : Dyn.S + +type static_block_declaration = { + start : Stateid.t; + stop : Stateid.t; + dynamic_switch : Stateid.t; + carry_on_data : DynBlockData.t; +} + +type document_node = { + indentation : int; + ast : Vernacexpr.vernac_expr; + id : Stateid.t; +} + +type document_view = { + entry_point : document_node; + prev_node : document_node -> document_node option; +} + +type static_block_detection = + document_view -> static_block_declaration option + +type recovery_action = { + base_state : Stateid.t; + goals_to_admit : Goal.goal list; + recovery_command : Vernacexpr.vernac_expr option; +} + +type dynamic_block_error_recovery = + static_block_declaration -> [ `ValidBlock of recovery_action | `Leaks ] + +val register_proof_block_delimiter : + Vernacexpr.proof_block_name -> + static_block_detection -> + dynamic_block_error_recovery -> + unit + (** customization ********************************************************** **) (* From the master (or worker, but beware that to install the hook @@ -122,7 +200,8 @@ type state = { proof : Proof_global.state; shallow : bool } -val state_of_id : Stateid.t -> [ `Valid of state option | `Expired ] +val state_of_id : + Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ] (** read-eval-print loop compatible interface ****************************** **) diff --git a/stm/stm.mllib b/stm/stm.mllib index bd792b01f6..939ee187ae 100644 --- a/stm/stm.mllib +++ b/stm/stm.mllib @@ -8,4 +8,5 @@ Lemmas CoqworkmgrApi AsyncTaskQueue Stm +ProofBlockDelimiter Vio_checking diff --git a/stm/vcs.ml b/stm/vcs.ml index 38c029901d..c483ea4a9d 100644 --- a/stm/vcs.ml +++ b/stm/vcs.ml @@ -22,51 +22,49 @@ module type S = sig end type id - - (* Branches have [branch_info] attached to them. *) + type ('kind) branch_info = { kind : [> `Master] as 'kind; root : id; pos : id; } - - type ('kind,'diff,'info) t constraint 'kind = [> `Master ] - - val empty : id -> ('kind,'diff,'info) t - - val current_branch : ('k,'e,'i) t -> Branch.t - val branches : ('k,'e,'i) t -> Branch.t list - - val get_branch : ('k,'e,'i) t -> Branch.t -> 'k branch_info - val reset_branch : ('k,'e,'i) t -> Branch.t -> id -> ('k,'e,'i) t + + type ('kind,'diff,'info,'property_data) t constraint 'kind = [> `Master ] + + val empty : id -> ('kind,'diff,'info,'property_data) t + + val current_branch : ('k,'e,'i,'c) t -> Branch.t + val branches : ('k,'e,'i,'c) t -> Branch.t list + + val get_branch : ('k,'e,'i,'c) t -> Branch.t -> 'k branch_info + val reset_branch : ('k,'e,'i,'c) t -> Branch.t -> id -> ('k,'e,'i,'c) t val branch : - ('kind,'e,'i) t -> ?root:id -> ?pos:id -> - Branch.t -> 'kind -> ('kind,'e,'i) t - val delete_branch : ('k,'e,'i) t -> Branch.t -> ('k,'e,'i) t + ('kind,'e,'i,'c) t -> ?root:id -> ?pos:id -> + Branch.t -> 'kind -> ('kind,'e,'i,'c) t + val delete_branch : ('k,'e,'i,'c) t -> Branch.t -> ('k,'e,'i,'c) t val merge : - ('k,'diff,'i) t -> id -> ours:'diff -> theirs:'diff -> ?into:Branch.t -> - Branch.t -> ('k,'diff,'i) t - val commit : ('k,'diff,'i) t -> id -> 'diff -> ('k,'diff,'i) t + ('k,'diff,'i,'c) t -> id -> ours:'diff -> theirs:'diff -> ?into:Branch.t -> + Branch.t -> ('k,'diff,'i,'c) t + val commit : ('k,'diff,'i,'c) t -> id -> 'diff -> ('k,'diff,'i,'c) t val rewrite_merge : - ('k,'diff,'i) t -> id -> ours:'diff -> theirs:'diff -> at:id -> - Branch.t -> ('k,'diff,'i) t - val checkout : ('k,'e,'i) t -> Branch.t -> ('k,'e,'i) t - - val set_info : ('k,'e,'info) t -> id -> 'info -> ('k,'e,'info) t - val get_info : ('k,'e,'info) t -> id -> 'info option + ('k,'diff,'i,'c) t -> id -> ours:'diff -> theirs:'diff -> at:id -> + Branch.t -> ('k,'diff,'i,'c) t + val checkout : ('k,'e,'i,'c) t -> Branch.t -> ('k,'e,'i,'c) t - module NodeSet : Set.S with type elt = id - - val gc : ('k,'e,'info) t -> ('k,'e,'info) t * NodeSet.t - - val reachable : ('k,'e,'info) t -> id -> NodeSet.t + val set_info : ('k,'e,'info,'c) t -> id -> 'info -> ('k,'e,'info,'c) t + val get_info : ('k,'e,'info,'c) t -> id -> 'info option + (* Read only dag *) module Dag : Dag.S with type node = id - val dag : ('kind,'diff,'info) t -> ('diff,'info,id*id) Dag.t + val dag : ('kind,'diff,'info,'cdata) t -> ('diff,'info,'cdata) Dag.t + + val create_property : ('k,'e,'i,'c) t -> id list -> 'c -> ('k,'e,'i,'c) t + val property_of : ('k,'e,'i,'c) t -> id -> 'c Dag.Property.t list + val delete_property : ('k,'e,'i,'c) t -> 'c Dag.Property.t -> ('k,'e,'i,'c) t - val create_cluster : ('k,'e,'i) t -> id list -> (id * id) -> ('k,'e,'i) t - val cluster_of : ('k,'e,'i) t -> id -> (id * id) Dag.Cluster.t option - val delete_cluster : ('k,'e,'i) t -> (id * id) Dag.Cluster.t -> ('k,'e,'i) t + (* Removes all unreachable nodes and returns them *) + val gc : ('k,'e,'info,'c) t -> ('k,'e,'info,'c) t * Dag.NodeSet.t + val reachable : ('k,'e,'info,'c) t -> id -> Dag.NodeSet.t end @@ -78,7 +76,6 @@ type id = OT.t module NodeSet = Dag.NodeSet - module Branch = struct type t = string @@ -99,10 +96,10 @@ type 'kind branch_info = { pos : id; } -type ('kind,'edge,'info) t = { +type ('kind,'edge,'info,'property_data) t = { cur_branch : Branch.t; heads : 'kind branch_info BranchMap.t; - dag : ('edge,'info,id*id) Dag.t; + dag : ('edge,'info,'property_data) Dag.t; } let empty root = { @@ -167,9 +164,9 @@ let checkout vcs name = { vcs with cur_branch = name } let set_info vcs id info = { vcs with dag = Dag.set_info vcs.dag id info } let get_info vcs id = Dag.get_info vcs.dag id -let create_cluster vcs l i = { vcs with dag = Dag.create_cluster vcs.dag l i } -let cluster_of vcs i = Dag.cluster_of vcs.dag i -let delete_cluster vcs c = { vcs with dag = Dag.del_cluster vcs.dag c } +let create_property vcs l i = { vcs with dag = Dag.create_property vcs.dag l i } +let property_of vcs i = Dag.property_of vcs.dag i +let delete_property vcs c = { vcs with dag = Dag.del_property vcs.dag c } let branches vcs = BranchMap.fold (fun x _ accu -> x :: accu) vcs.heads [] let dag vcs = vcs.dag diff --git a/stm/vcs.mli b/stm/vcs.mli index 8f22fee843..46b40f8a4c 100644 --- a/stm/vcs.mli +++ b/stm/vcs.mli @@ -19,10 +19,11 @@ As a consequence, "checkout" just updates the current branch. The type [id] is the type of commits (a node in the dag) - The type [Vcs.t] has 3 parameters: + The type [Vcs.t] has 4 parameters: ['info] data attached to a node (like a system state) ['diff] data attached to an edge (the commit content, a "patch") ['kind] extra data attached to a branch (like being the master branch) + ['cdata] extra data hold by dag properties *) module type S = sig @@ -45,46 +46,51 @@ module type S = sig pos : id; } - type ('kind,'diff,'info) t constraint 'kind = [> `Master ] + type ('kind,'diff,'info,'property_data) t constraint 'kind = [> `Master ] - val empty : id -> ('kind,'diff,'info) t + val empty : id -> ('kind,'diff,'info,'property_data) t - val current_branch : ('k,'e,'i) t -> Branch.t - val branches : ('k,'e,'i) t -> Branch.t list + val current_branch : ('k,'e,'i,'c) t -> Branch.t + val branches : ('k,'e,'i,'c) t -> Branch.t list - val get_branch : ('k,'e,'i) t -> Branch.t -> 'k branch_info - val reset_branch : ('k,'e,'i) t -> Branch.t -> id -> ('k,'e,'i) t + val get_branch : ('k,'e,'i,'c) t -> Branch.t -> 'k branch_info + val reset_branch : ('k,'e,'i,'c) t -> Branch.t -> id -> ('k,'e,'i,'c) t val branch : - ('kind,'e,'i) t -> ?root:id -> ?pos:id -> - Branch.t -> 'kind -> ('kind,'e,'i) t - val delete_branch : ('k,'e,'i) t -> Branch.t -> ('k,'e,'i) t + ('kind,'e,'i,'c) t -> ?root:id -> ?pos:id -> + Branch.t -> 'kind -> ('kind,'e,'i,'c) t + val delete_branch : ('k,'e,'i,'c) t -> Branch.t -> ('k,'e,'i,'c) t val merge : - ('k,'diff,'i) t -> id -> ours:'diff -> theirs:'diff -> ?into:Branch.t -> - Branch.t -> ('k,'diff,'i) t - val commit : ('k,'diff,'i) t -> id -> 'diff -> ('k,'diff,'i) t + ('k,'diff,'i,'c) t -> id -> ours:'diff -> theirs:'diff -> ?into:Branch.t -> + Branch.t -> ('k,'diff,'i,'c) t + val commit : ('k,'diff,'i,'c) t -> id -> 'diff -> ('k,'diff,'i,'c) t val rewrite_merge : - ('k,'diff,'i) t -> id -> ours:'diff -> theirs:'diff -> at:id -> - Branch.t -> ('k,'diff,'i) t - val checkout : ('k,'e,'i) t -> Branch.t -> ('k,'e,'i) t + ('k,'diff,'i,'c) t -> id -> ours:'diff -> theirs:'diff -> at:id -> + Branch.t -> ('k,'diff,'i,'c) t + val checkout : ('k,'e,'i,'c) t -> Branch.t -> ('k,'e,'i,'c) t - val set_info : ('k,'e,'info) t -> id -> 'info -> ('k,'e,'info) t - val get_info : ('k,'e,'info) t -> id -> 'info option + val set_info : ('k,'e,'info,'c) t -> id -> 'info -> ('k,'e,'info,'c) t + val get_info : ('k,'e,'info,'c) t -> id -> 'info option - module NodeSet : Set.S with type elt = id + (* Read only dag *) + module Dag : Dag.S with type node = id + val dag : ('kind,'diff,'info,'cdata) t -> ('diff,'info,'cdata) Dag.t - (* Removes all unreachable nodes and returns them *) - val gc : ('k,'e,'info) t -> ('k,'e,'info) t * NodeSet.t + (* Properties are not a concept typical of a VCS, but a useful metadata + * of a DAG (or graph). *) + val create_property : ('k,'e,'i,'c) t -> id list -> 'c -> ('k,'e,'i,'c) t + val property_of : ('k,'e,'i,'c) t -> id -> 'c Dag.Property.t list + val delete_property : ('k,'e,'i,'c) t -> 'c Dag.Property.t -> ('k,'e,'i,'c) t - val reachable : ('k,'e,'info) t -> id -> NodeSet.t + (* Removes all unreachable nodes and returns them *) + val gc : ('k,'e,'info,'c) t -> ('k,'e,'info,'c) t * Dag.NodeSet.t + val reachable : ('k,'e,'info,'c) t -> id -> Dag.NodeSet.t - (* read only dag *) - module Dag : Dag.S with type node = id - val dag : ('kind,'diff,'info) t -> ('diff,'info,id * id) Dag.t - val create_cluster : ('k,'e,'i) t -> id list -> (id * id) -> ('k,'e,'i) t - val cluster_of : ('k,'e,'i) t -> id -> (id * id) Dag.Cluster.t option - val delete_cluster : ('k,'e,'i) t -> (id * id) Dag.Cluster.t -> ('k,'e,'i) t - end -module Make(OT : Map.OrderedType) : S with type id = OT.t +module Make(OT : Map.OrderedType) : S +with type id = OT.t +and type Dag.node = OT.t +and type Dag.NodeSet.t = Set.Make(OT).t +and type Dag.NodeSet.elt = OT.t + diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index b1df3c9ca6..a602d6b8a8 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -21,8 +21,9 @@ let string_of_vernac_type = function | VtQed VtKeep -> "Qed(keep)" | VtQed VtKeepAsAxiom -> "Qed(admitted)" | VtQed VtDrop -> "Qed(drop)" - | VtProofStep false -> "ProofStep" - | VtProofStep true -> "ProofStep (parallel)" + | VtProofStep { parallel; proof_block_detection } -> + "ProofStep " ^ if parallel then "par " else "" ^ + Option.default "" proof_block_detection | VtProofMode s -> "ProofMode " ^ s | VtQuery (b,(id,route)) -> "Query " ^ string_of_in_script b ^ " report " ^ Stateid.to_string id ^ @@ -93,7 +94,9 @@ let rec classify_vernac e = (match classify_vernac e with | ( VtQuery _ | VtProofStep _ | VtSideff _ | VtStm _ | VtProofMode _ ), _ as x -> x - | VtQed _, _ -> VtProofStep false, VtNow + | VtQed _, _ -> + VtProofStep { parallel = false; proof_block_detection = None }, + VtNow | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow) (* Qed *) | VernacAbort _ -> VtQed VtDrop, VtLater @@ -105,12 +108,19 @@ let rec classify_vernac e = VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater (* ProofStep *) | VernacProof _ - | VernacBullet _ | VernacFocus _ | VernacUnfocus - | VernacSubproof _ | VernacEndSubproof + | VernacSubproof _ | VernacCheckGuard | VernacUnfocused - | VernacSolveExistential _ -> VtProofStep false, VtLater + | VernacSolveExistential _ -> + VtProofStep { parallel = false; proof_block_detection = None }, VtLater + | VernacBullet _ -> + VtProofStep { parallel = false; proof_block_detection = Some "bullet" }, + VtLater + | VernacEndSubproof -> + VtProofStep { parallel = false; + proof_block_detection = Some "curly" }, + VtLater (* Options changing parser *) | VernacUnsetOption (["Default";"Proof";"Using"]) | VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow @@ -219,4 +229,4 @@ let rec classify_vernac e = let classify_as_query = VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater let classify_as_sideeff = VtSideff [], VtLater -let classify_as_proofstep = VtProofStep false, VtLater +let classify_as_proofstep = VtProofStep { parallel = false; proof_block_detection = None}, VtLater diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 858cc482ae..991922d909 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1661,7 +1661,7 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) if n<0 then error "Applied theorem has not enough premisses."; let clause = make_clenv_binding_apply env sigma (Some n) (c,thm_ty) lbind in Clenvtac.res_pf clause ~with_evars ~flags - with UserError _ as exn -> + with exn when catchable_exception exn -> Proofview.tclZERO exn in let rec try_red_apply thm_ty (exn0, info) = diff --git a/test-suite/Makefile b/test-suite/Makefile index 91b8a4ed08..b9c27a2fcf 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -421,7 +421,7 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake)) @echo "TEST $<" $(HIDE){ \ echo $(call log_intro,$<); \ - $(BIN)fake_ide $< "$(BIN)coqtop -boot -async-proofs on" 2>&1; \ + $(BIN)fake_ide $< "$(BIN)coqtop -boot -async-proofs on -async-proofs-tactic-error-resiliency off -async-proofs-command-error-resiliency off" 2>&1; \ if [ $$? = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ diff --git a/test-suite/bugs/closed/4782.v b/test-suite/bugs/closed/4782.v new file mode 100644 index 0000000000..ed44437861 --- /dev/null +++ b/test-suite/bugs/closed/4782.v @@ -0,0 +1,9 @@ +(* About typing of with bindings *) + +Record r : Type := mk_r { type : Type; cond : type -> Prop }. + +Inductive p : Prop := consp : forall (e : r) (x : type e), cond e x -> p. + +Goal p. +Fail apply consp with (fun _ : bool => mk_r unit (fun x => True)) nil. + diff --git a/test-suite/bugs/closed/4813.v b/test-suite/bugs/closed/4813.v new file mode 100644 index 0000000000..5f8ea74c1a --- /dev/null +++ b/test-suite/bugs/closed/4813.v @@ -0,0 +1,9 @@ +(* On the strength of "apply with" (see also #4782) *) + +Record ProverT := { Facts : Type }. +Record ProverT_correct (P : ProverT) := { Valid : Facts P -> Prop ; + Valid_weaken : Valid = Valid }. +Definition reflexivityValid (_ : unit) := True. +Definition reflexivityProver_correct : ProverT_correct {| Facts := unit |}. +Proof. + eapply Build_ProverT_correct with (Valid := reflexivityValid). diff --git a/test-suite/bugs/closed/4816.v b/test-suite/bugs/closed/4816.v new file mode 100644 index 0000000000..86597c88fa --- /dev/null +++ b/test-suite/bugs/closed/4816.v @@ -0,0 +1,17 @@ +Section foo. +Polymorphic Universes A B. +Fail Constraint A <= B. +End foo. +(* gives an anomaly Universe undefined *) + +Universes X Y. +Section Foo. + Polymorphic Universes Z W. + Polymorphic Constraint W < Z. + + Fail Definition bla := Type@{W}. + Polymorphic Definition bla := Type@{W}. + Section Bar. + Fail Constraint X <= Z. + End Bar. +End Foo. diff --git a/test-suite/interactive/proof_block.v b/test-suite/interactive/proof_block.v new file mode 100644 index 0000000000..31e3493768 --- /dev/null +++ b/test-suite/interactive/proof_block.v @@ -0,0 +1,66 @@ +Goal False /\ True. +Proof. +split. + idtac. + idtac. + exact I. +idtac. +idtac. +exact I. +Qed. + +Lemma baz : (exists n, n = 3 /\ n = 3) /\ True. +Proof. +split. { eexists. split. par: trivial. } +trivial. +Qed. + +Lemma baz1 : (True /\ False) /\ True. +Proof. +split. { split. par: trivial. } +trivial. +Qed. + +Lemma foo : (exists n, n = 3 /\ n = 3) /\ True. +Proof. +split. + { idtac. + unshelve eexists. + { apply 3. } + { split. + { idtac. trivialx. } + { reflexivity. } } } + trivial. +Qed. + +Lemma foo1 : False /\ True. +Proof. +split. + { exact I. } + { exact I. } +Qed. + +Definition banana := true + 4. + +Check banana. + +Lemma bar : (exists n, n = 3 /\ n = 3) /\ True. +Proof. +split. + - idtac. + unshelve eexists. + + apply 3. + + split. + * idtacx. trivial. + * reflexivity. + - trivial. +Qed. + +Lemma baz2 : ((1=0 /\ False) /\ True) /\ False. +Proof. +split. split. split. + - solve [ auto ]. + - solve [ trivial ]. + - solve [ trivial ]. + - exact 6. +Qed.
\ No newline at end of file diff --git a/test-suite/success/ltacprof.v b/test-suite/success/ltacprof.v new file mode 100644 index 0000000000..d5552695c4 --- /dev/null +++ b/test-suite/success/ltacprof.v @@ -0,0 +1,8 @@ +(** Some LtacProf tests *) + +Set Ltac Profiling. +Ltac multi := (idtac + idtac). +Goal True. + try (multi; fail). (* Used to result in: Anomaly: Uncaught exception Failure("hd"). Please report. *) +Admitted. +Show Ltac Profile. diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 32c22f9e62..45e843e609 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -50,8 +50,9 @@ let section s = let lib_dirs = ["kernel"; "lib"; "library"; "parsing"; "pretyping"; "interp"; "printing"; "intf"; - "proofs"; "tactics"; "tools"; "toplevel"; - "stm"; "grammar"; "config"; "ltac"; "engine"] + "proofs"; "tactics"; "tools"; "ltacprof"; + "toplevel"; "stm"; "grammar"; "config"; + "ltac"; "engine"] let usage () = diff --git a/tools/coqc.ml b/tools/coqc.ml index f957200ab5..18b2a24fa0 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -88,7 +88,7 @@ let parse_args () = (* Options for coqtop : a) options with 0 argument *) - | ("-notactics"|"-bt"|"-debug"|"-nolib"|"-boot"|"-time" + | ("-notactics"|"-bt"|"-debug"|"-nolib"|"-boot"|"-time"|"-profile-ltac" |"-batch"|"-noinit"|"-nois"|"-noglob"|"-no-glob" |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet" |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit" diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 869f6bb931..a488bb3e64 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -370,6 +370,11 @@ let get_int opt n = with Failure _ -> prerr_endline ("Error: integer expected after option "^opt); exit 1 +let get_float opt n = + try float_of_string n + with Failure _ -> + prerr_endline ("Error: float expected after option "^opt); exit 1 + let get_host_port opt s = match CString.split ':' s with | [host; portr; portw] -> @@ -379,6 +384,11 @@ let get_host_port opt s = prerr_endline ("Error: host:port or stdfds expected after option "^opt); exit 1 +let get_error_resilience opt = function + | "on" | "all" | "yes" -> `All + | "off" | "no" -> `None + | s -> `Only (String.split ',' s) + let get_task_list s = List.map int_of_string (Str.split (Str.regexp ",") s) let vio_tasks = ref [] @@ -492,6 +502,12 @@ let parse_args arglist = Flags.async_proofs_worker_priority := get_priority opt (next ()) |"-async-proofs-private-flags" -> Flags.async_proofs_private_flags := Some (next ()); + |"-async-proofs-tactic-error-resilience" -> + Flags.async_proofs_tac_error_resilience := get_error_resilience opt (next ()) + |"-async-proofs-command-error-resilience" -> + Flags.async_proofs_cmd_error_resilience := get_bool opt (next ()) + |"-async-proofs-delegation-threshold" -> + Flags.async_proofs_delegation_threshold:= get_float opt (next ()) |"-worker-id" -> set_worker_id opt (next ()) |"-compat" -> let v = get_compat_version (next ()) in Flags.compat_version := v; add_compat_require v |"-compile" -> add_compile false (next ()) @@ -549,6 +565,7 @@ let parse_args arglist = else native_compiler := true |"-notop" -> unset_toplevel_name () |"-output-context" -> output_context := true + |"-profile-ltac" -> Flags.profile_ltac := true |"-q" -> no_load_rc () |"-quiet"|"-silent" -> Flags.make_silent true; Flags.make_warn false |"-quick" -> Flags.compilation_mode := BuildVio diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index ad848ccfc8..e17cd20863 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -69,12 +69,12 @@ let rec contract3' env a b c = function let (env',t1,t2) = contract2 env' t1 t2 in contract3 env a b c, ConversionFailed (env',t1,t2) | NotSameArgSize | NotSameHead | NoCanonicalStructure - | MetaOccurInBody _ | InstanceNotSameType _ + | MetaOccurInBody _ | InstanceNotSameType _ | ProblemBeyondCapabilities | UnifUnivInconsistency _ as x -> contract3 env a b c, x - | CannotSolveConstraint ((pb,env,t,u),x) -> - let env,t,u = contract2 env t u in + | CannotSolveConstraint ((pb,env',t,u),x) -> + let env',t,u = contract2 env' t u in let y,x = contract3' env a b c x in - y,CannotSolveConstraint ((pb,env,t,u),x) + y,CannotSolveConstraint ((pb,env',t,u),x) (** Ad-hoc reductions *) @@ -323,6 +323,8 @@ let explain_unification_error env sigma p1 p2 = function (strbrk "cannot satisfy constraint " ++ pr_lconstr_env env sigma t ++ str " == " ++ pr_lconstr_env env sigma u) :: aux t u e + | ProblemBeyondCapabilities -> + [] in match aux p1 p2 e with | [] -> mt () diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 52117f13f6..b22d53f546 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -827,7 +827,7 @@ let make_interpretation_type isrec isonlybinding = function | NtnInternTypeConstr | NtnInternTypeIdent -> if isonlybinding then NtnTypeOnlyBinder else NtnTypeConstr | NtnInternTypeBinder when isrec -> NtnTypeBinderList - | NtnInternTypeBinder -> error "Type not allowed in recursive notation." + | NtnInternTypeBinder -> error "Type binder is only for use in recursive notations for binders." let make_interpretation_vars recvars allvars = let eq_subscope (sc1, l1) (sc2, l2) = diff --git a/toplevel/usage.ml b/toplevel/usage.ml index f855c096e3..5359a288ac 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -77,6 +77,7 @@ let print_usage_channel co command = \n the directory $COQ_XML_LIBRARY_ROOT (if set) or to\ \n stdout (if unset)\ \n -time display the time taken by each command\ +\n -profile-ltac display the time taken by each (sub)tactic\ \n -m, --memory display total heap size at program exit\ \n (use environment variable\ \n OCAML_GC_STATS=\"/tmp/gclog.txt\"\ |