From 5f3d20dc53ffd0537a84c93acd761c3c69081342 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 10 Jun 2016 19:12:49 -0400 Subject: Add transparent_abstract tactic --- doc/refman/RefMan-ltac.tex | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) (limited to 'doc') diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 9378529cbe..46274e12f3 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -1087,8 +1087,8 @@ Fail all:let n:= numgoals in guard n=2. Reset Initial. \end{coq_eval} -\subsubsection[Proving a subgoal as a separate lemma]{Proving a subgoal as a separate lemma\tacindex{abstract}\comindex{Qed exporting} -\index{Tacticals!abstract@{\tt abstract}}} +\subsubsection[Proving a subgoal as a separate lemma]{Proving a subgoal as a separate lemma\tacindex{abstract}\tacindex{transparent\_abstract}\comindex{Qed exporting} +\index{Tacticals!abstract@{\tt abstract}}\index{Tacticals!transparent\_abstract@{\tt transparent\_abstract}}} From the outside ``\texttt{abstract \tacexpr}'' is the same as {\tt solve \tacexpr}. Internally it saves an auxiliary lemma called @@ -1114,13 +1114,17 @@ on. This can be obtained thanks to the option below. {\tt Set Shrink Abstract} \end{quote} -When set, all lemmas generated through \texttt{abstract {\tacexpr}} are -quantified only over the variables that appear in the term constructed by -\texttt{\tacexpr}. +When set, all lemmas generated through \texttt{abstract {\tacexpr}} +and \texttt{transparent\_abstract {\tacexpr}} are quantified only over the +variables that appear in the term constructed by \texttt{\tacexpr}. \begin{Variants} \item \texttt{abstract {\tacexpr} using {\ident}}.\\ Give explicitly the name of the auxiliary lemma. +\item \texttt{transparent\_abstract {\tacexpr}}.\\ + Save the subproof in a transparent lemma rather than an opaque one. +\item \texttt{transparent\_abstract {\tacexpr} using {\ident}}.\\ + Give explicitly the name of the auxiliary transparent lemma. \end{Variants} \ErrMsg \errindex{Proof is not complete} -- cgit v1.2.3 From 84845f766d9b9d532f615352fbc8a0e78e1727e9 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 27 Mar 2017 13:28:17 -0400 Subject: Mark transparent_abstract as risky in docs As per Enrico's request. --- doc/refman/RefMan-ltac.tex | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'doc') diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 46274e12f3..c2f52e23bc 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -1121,10 +1121,17 @@ variables that appear in the term constructed by \texttt{\tacexpr}. \begin{Variants} \item \texttt{abstract {\tacexpr} using {\ident}}.\\ Give explicitly the name of the auxiliary lemma. + Use this feature at your own risk; explicitly named and reused subterms + don't play well with asynchronous proofs. \item \texttt{transparent\_abstract {\tacexpr}}.\\ Save the subproof in a transparent lemma rather than an opaque one. + Use this feature at your own risk; building computationally relevant terms + with tactics is fragile. \item \texttt{transparent\_abstract {\tacexpr} using {\ident}}.\\ Give explicitly the name of the auxiliary transparent lemma. + Use this feature at your own risk; building computationally relevant terms + with tactics is fragile, and explicitly named and reused subterms + don't play well with asynchronous proofs. \end{Variants} \ErrMsg \errindex{Proof is not complete} -- cgit v1.2.3 From e574b4bdd974daa7d2ceecf799762be92fadff44 Mon Sep 17 00:00:00 2001 From: Paul Steckler Date: Thu, 27 Apr 2017 12:05:51 -0400 Subject: fix order of command-line arguments mentioned in Add LoadPath --- doc/refman/RefMan-oth.tex | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'doc') diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 56ce753cd6..a25da7d926 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -697,8 +697,8 @@ which can be any valid path. \subsection[\tt Add LoadPath {\str} as {\dirpath}.]{\tt Add LoadPath {\str} as {\dirpath}.\comindex{Add LoadPath}\label{AddLoadPath}} -This command is equivalent to the command line option {\tt -Q {\dirpath} - {\str}}. It adds the physical directory {\str} to the current {\Coq} +This command is equivalent to the command line option {\tt -Q {\str} + {\dirpath}}. It adds the physical directory {\str} to the current {\Coq} loadpath and maps it to the logical directory {\dirpath}. \begin{Variants} @@ -707,8 +707,8 @@ Performs as {\tt Add LoadPath {\str} as {\dirpath}} but for the empty directory \end{Variants} \subsection[\tt Add Rec LoadPath {\str} as {\dirpath}.]{\tt Add Rec LoadPath {\str} as {\dirpath}.\comindex{Add Rec LoadPath}\label{AddRecLoadPath}} -This command is equivalent to the command line option {\tt -R {\dirpath} - {\str}}. It adds the physical directory {\str} and all its +This command is equivalent to the command line option {\tt -R {\str} + {\dirpath}}. It adds the physical directory {\str} and all its subdirectories to the current {\Coq} loadpath. \begin{Variants} -- cgit v1.2.3 From 4a84961049f4f00897ae72a13954edbcc9aaba5e Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 3 May 2017 10:23:46 +0200 Subject: Fix outdated description in RefMan. --- doc/refman/RefMan-pro.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index c37367de5b..4c333379bd 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -118,7 +118,7 @@ the current proof and declare the initial goal as an axiom. \subsection[\tt Proof {\term}.]{\tt Proof {\term}.\comindex{Proof} \label{BeginProof}} This command applies in proof editing mode. It is equivalent to {\tt - exact {\term}; Save.} That is, you have to give the full proof in + exact {\term}. Qed.} That is, you have to give the full proof in one gulp, as a proof term (see Section~\ref{exact}). \variant {\tt Proof.} -- cgit v1.2.3 From 4cc655377e3c73fd3066cd8136d17605f167ef56 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 4 May 2017 10:28:56 +0200 Subject: Improve documentation of assert / pose proof / specialize. This commits documents the as clause of specialize and that the as clause of pose proof is optional. It also mentions a feature of assert ( := ) that was available since 8.5 and was mentionned by @herbelin in: https://github.com/coq/coq/pull/248#issuecomment-297970503 --- doc/refman/RefMan-tac.tex | 28 ++++++++++++++++++---------- 1 file changed, 18 insertions(+), 10 deletions(-) (limited to 'doc') diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 0edc66f839..87b9e4914f 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1275,15 +1275,18 @@ in the list of subgoals remaining to prove. \item{\tt assert ( {\ident} := {\term} )} - This behaves as {\tt assert ({\ident} :\ {\type});[exact - {\term}|idtac]} where {\type} is the type of {\term}. This is - deprecated in favor of {\tt pose proof}. + This behaves as {\tt assert ({\ident} :\ {\type}) by exact {\term}} + where {\type} is the type of {\term}. This is deprecated in favor of + {\tt pose proof}. + + If the head of {\term} is {\ident}, the tactic behaves as + {\tt specialize \term}. \ErrMsg \errindex{Variable {\ident} is already declared} -\item \texttt{pose proof {\term} as {\intropattern}\tacindex{pose proof}} +\item \texttt{pose proof {\term} \zeroone{as {\intropattern}}\tacindex{pose proof}} - This tactic behaves like \texttt{assert T as {\intropattern} by + This tactic behaves like \texttt{assert T \zeroone{as {\intropattern}} by exact {\term}} where \texttt{T} is the type of {\term}. In particular, \texttt{pose proof {\term} as {\ident}} behaves as @@ -1326,8 +1329,8 @@ in the list of subgoals remaining to prove. following subgoals: {\tt U -> T} and \texttt{U}. The subgoal {\tt U -> T} comes first in the list of remaining subgoal to prove. -\item {\tt specialize ({\ident} \term$_1$ \dots\ \term$_n$)\tacindex{specialize}} \\ - {\tt specialize {\ident} with \bindinglist} +\item {\tt specialize ({\ident} \term$_1$ \dots\ \term$_n$)\tacindex{specialize} \zeroone{as \intropattern}}\\ + {\tt specialize {\ident} with {\bindinglist} \zeroone{as \intropattern}} The tactic {\tt specialize} works on local hypothesis \ident. The premises of this hypothesis (either universal @@ -1338,14 +1341,19 @@ in the list of subgoals remaining to prove. second form, all instantiation elements must be given, whereas in the first form the application to \term$_1$ {\ldots} \term$_n$ can be partial. The first form is equivalent to - {\tt assert (\ident' := {\ident} {\term$_1$} \dots\ \term$_n$); - clear \ident; rename \ident' into \ident}. + {\tt assert ({\ident} := {\ident} {\term$_1$} \dots\ \term$_n$)}. + + With the {\tt as} clause, the local hypothesis {\ident} is left + unchanged and instead, the modified hypothesis is introduced as + specified by the {\intropattern}. The name {\ident} can also refer to a global lemma or hypothesis. In this case, for compatibility reasons, the behavior of {\tt specialize} is close to that of {\tt generalize}: the instantiated statement becomes an additional - premise of the goal. + premise of the goal. The {\tt as} clause is especially useful + in this case to immediately introduce the instantiated statement + as a local hypothesis. \begin{ErrMsgs} \item \errindexbis{{\ident} is used in hypothesis \ident'}{is used in hypothesis} -- cgit v1.2.3 From 06f3ce00971283d2718e272ec9f123430d75ffa6 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Thu, 11 May 2017 15:16:21 +0200 Subject: Documenting Printing Compact Contexts + CHANGES --- doc/refman/RefMan-oth.tex | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) (limited to 'doc') diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 56ce753cd6..0f6978b255 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -960,6 +960,22 @@ time of writing this documentation, the default value is 50). \subsection[\tt Test Printing Depth.]{\tt Test Printing Depth.\optindex{Printing Depth}} This command displays the current nesting depth used for display. +\subsection[\tt Unset Printing Compact Contexts.]{\tt Unset Printing Compact Contexts.\optindex{Printing Compact Contexts}} +This command resets the displaying of goals contexts to non compact +mode (default at the time of writing this documentation). Non compact +means that consecutive variables of different types are printed on +different lines. + +\subsection[\tt Set Printing Compact Contexts.]{\tt Set Printing Compact Contexts.\optindex{Printing Compact Contexts}} +This command sets the displaying of goals contexts to compact mode. +The printer tries to reduce the vertical size of goals contexts by +putting several variables (even if of different types) on the same +line provided it does not exceed the printing width (See {\tt Set + Printing Width} above). + +\subsection[\tt Test Printing Compact Contexts.]{\tt Test Printing Compact Contexts.\optindex{Printing Compact Contexts}} +This command displays the current state of compaction of goal d'isolat. + \subsection[\tt Set Printing Dependent Evars Line.]{\tt Set Printing Dependent Evars Line.\optindex{Printing Dependent Evars Line}} This command enables the printing of the ``{\tt (dependent evars: \ldots)}'' line when {\tt -emacs} is passed. -- cgit v1.2.3 From 6c9fb0b16fa5674a3135a49adff201d6e4415cd1 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 10 May 2017 20:48:37 -0400 Subject: Add documentation for Set Ltac Batch Debug --- doc/refman/RefMan-ltac.tex | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index c2f52e23bc..0346c4a555 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -1242,7 +1242,7 @@ This will automatically print the same trace as {\tt Info \num} at each tactic c The current value for the {\tt Info Level} option can be checked using the {\tt Test Info Level} command. -\subsection[Interactive debugger]{Interactive debugger\optindex{Ltac Debug}} +\subsection[Interactive debugger]{Interactive debugger\optindex{Ltac Debug}\optindex{Ltac Batch Debug}} The {\ltac} interpreter comes with a step-by-step debugger. The debugger can be activated using the command @@ -1273,6 +1273,17 @@ r $n$: & advance $n$ steps further\\ r {\qstring}: & advance up to the next call to ``{\tt idtac} {\qstring}''\\ \end{tabular} +A non-interactive mode for the debugger is available via the command + +\begin{quote} +{\tt Set Ltac Batch Debug.} +\end{quote} + +This option has the effect of presenting a newline at every prompt, +when the debugger is on. The debug log thus created, which does not +require user input to generate when this option is set, can then be +run through external tools such as \texttt{diff}. + \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. -- cgit v1.2.3