diff options
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 18 | ||||
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 24 | ||||
| -rw-r--r-- | doc/refman/RefMan-pro.tex | 15 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 96 | ||||
| -rw-r--r-- | doc/refman/RefMan-tus.tex | 2 | ||||
| -rw-r--r-- | doc/refman/RefMan-uti.tex | 196 |
6 files changed, 202 insertions, 149 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 0346c4a555..bb679ecba7 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -522,6 +522,19 @@ to have \emph{at least} one success. \ErrMsg \errindex{No applicable tactic} +\variant {\tt first {\tacexpr}} + +This is an Ltac alias that gives a primitive access to the {\tt first} tactical +as a Ltac definition without going through a parsing rule. It expects to be +given a list of tactics through a {\tt Tactic Notation}, allowing to write +notations of the following form. + +\Example + +\begin{quote} +{\tt Tactic Notation "{foo}" tactic\_list(tacs) := first tacs.} +\end{quote} + \subsubsection[Left-biased branching]{Left-biased branching\tacindex{$\mid\mid$} \index{Tacticals!orelse@{\tt $\mid\mid$}}} @@ -600,6 +613,11 @@ $v_2$ and so on. It fails if there is no solving tactic. \ErrMsg \errindex{Cannot solve the goal} +\variant {\tt solve {\tacexpr}} + +This is an Ltac alias that gives a primitive access to the {\tt solve} tactical. +See the {\tt first} tactical for more information. + \subsubsection[Identity]{Identity\label{ltac:idtac}\tacindex{idtac} \index{Tacticals!idtac@{\tt idtac}}} diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 56ce753cd6..3daaac88b1 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} @@ -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. diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 6d54b4de15..0760d716e3 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -90,25 +90,12 @@ memory overflow. Defines the proved term as a transparent constant. -\item {\tt Save.} -\comindex{Save} - - This is a deprecated equivalent to {\tt Qed}. - \item {\tt Save {\ident}.} Forces the name of the original goal to be {\ident}. This command (and the following ones) can only be used if the original goal has been opened using the {\tt Goal} command. -\item {\tt Save Theorem {\ident}.} \\ - {\tt Save Lemma {\ident}.} \\ - {\tt Save Remark {\ident}.}\\ - {\tt Save Fact {\ident}.} - {\tt Save Corollary {\ident}.} - {\tt Save Proposition {\ident}.} - - Are equivalent to {\tt Save {\ident}.} \end{Variants} \subsection[\tt Admitted.]{\tt Admitted.\comindex{Admitted}\label{Admitted}} @@ -118,7 +105,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.} diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 87b9e4914f..253eb7f01b 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1155,6 +1155,15 @@ Section~\ref{Occurrences_clauses}. These are the general forms that combine the previous possibilities. +\item {\tt eset ( {\ident$_0$} \nelistnosep{\binder} := {\term} ) in {\occgoalset}}\tacindex{eset}\\ + {\tt eset {\term} in {\occgoalset}} + + While the different variants of \texttt{set} expect that no + existential variables are generated by the tactic, \texttt{eset} + removes this constraint. In practice, this is relevant only when + \texttt{eset} is used as a synonym of \texttt{epose}, i.e. when the + term does not occur in the goal. + \item {\tt remember {\term} as {\ident}}\tacindex{remember} This behaves as {\tt set ( {\ident} := {\term} ) in *} and using a @@ -1170,6 +1179,15 @@ Section~\ref{Occurrences_clauses}. This is a more general form of {\tt remember} that remembers the occurrences of {\term} specified by an occurrences set. +\item + {\tt eremember {\term} as {\ident}}\tacindex{eremember}\\ + {\tt eremember {\term} as {\ident} in {\occgoalset}}\\ + {\tt eremember {\term} as {\ident} eqn:{\ident}} + + While the different variants of \texttt{remember} expect that no + existential variables are generated by the tactic, \texttt{eremember} + removes this constraint. + \item {\tt pose ( {\ident} := {\term} )}\tacindex{pose} This adds the local definition {\ident} := {\term} to the current @@ -1187,6 +1205,14 @@ Section~\ref{Occurrences_clauses}. This behaves as {\tt pose ( {\ident} := {\term} )} but {\ident} is generated by {\Coq}. +\item {\tt epose ( {\ident} := {\term} )}\tacindex{epose}\\ + {\tt epose ( {\ident} \nelistnosep{\binder} := {\term} )}\\ + {\tt epose {\term}} + + While the different variants of \texttt{pose} expect that no + existential variables are generated by the tactic, \texttt{epose} + removes this constraint. + \end{Variants} \subsection{\tt decompose [ {\qualid$_1$} \dots\ {\qualid$_n$} ] \term} @@ -1284,6 +1310,14 @@ in the list of subgoals remaining to prove. \ErrMsg \errindex{Variable {\ident} is already declared} +\item \texttt{eassert {\form} as {\intropattern} by {\tac}}\tacindex{eassert}\tacindex{eassert as}\tacindex{eassert by}\\ + {\tt assert ( {\ident} := {\term} )} + + While the different variants of \texttt{assert} expect that no + existential variables are generated by the tactic, \texttt{eassert} + removes this constraint. This allows not to specify the asserted + statement completely before starting to prove it. + \item \texttt{pose proof {\term} \zeroone{as {\intropattern}}\tacindex{pose proof}} This tactic behaves like \texttt{assert T \zeroone{as {\intropattern}} by @@ -1294,6 +1328,11 @@ in the list of subgoals remaining to prove. as {\intropattern}} is the same as applying the {\intropattern} to {\term}. +\item \texttt{epose proof {\term} \zeroone{as {\intropattern}}\tacindex{epose proof}} + + While \texttt{pose proof} expects that no existential variables are generated by the tactic, + \texttt{epose proof} removes this constraint. + \item \texttt{enough ({\ident} :\ {\form})}\tacindex{enough} This adds a new hypothesis of name {\ident} asserting {\form} to the @@ -1320,6 +1359,14 @@ in the list of subgoals remaining to prove. destructed. If the \texttt{as} {\intropattern} clause generates more than one subgoal, {\tac} is applied to all of them. +\item \texttt{eenough ({\ident} :\ {\form}) by {\tac}}\tacindex{eenough}\tacindex{eenough as}\tacindex{eenough by}\\ + \texttt{eenough {\form} by {\tac}}\tacindex{enough by}\\ + \texttt{eenough {\form} as {\intropattern} by {\tac}} + + While the different variants of \texttt{enough} expect that no + existential variables are generated by the tactic, \texttt{eenough} + removes this constraint. + \item {\tt cut {\form}}\tacindex{cut} This tactic applies to any goal. It implements the non-dependent @@ -1337,12 +1384,16 @@ in the list of subgoals remaining to prove. quantifications or non-dependent implications) are instantiated by concrete terms coming either from arguments \term$_1$ $\ldots$ \term$_n$ or from a bindings list (see - Section~\ref{Binding-list} for more about bindings lists). In the - second form, all instantiation elements must be given, whereas - in the first form the application to \term$_1$ {\ldots} + Section~\ref{Binding-list} for more about bindings lists). + 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$)}. + In the second form, instantiation elements can also be partial. + In this case the uninstantiated arguments are inferred by + unification if possible or left quantified in the hypothesis + otherwise. + With the {\tt as} clause, the local hypothesis {\ident} is left unchanged and instead, the modified hypothesis is introduced as specified by the {\intropattern}. @@ -2187,32 +2238,24 @@ the given bindings to instantiate parameters or hypotheses of {\term}. \label{injection} \tacindex{injection} -The {\tt injection} tactic is based on the fact that constructors of -inductive sets are injections. That means that if $c$ is a constructor -of an inductive set, and if $(c~\vec{t_1})$ and $(c~\vec{t_2})$ are two -terms that are equal then $~\vec{t_1}$ and $~\vec{t_2}$ are equal -too. +The {\tt injection} tactic exploits the property that constructors of +inductive types are injective, i.e. that if $c$ is a constructor +of an inductive type and $c~\vec{t_1}$ and $c~\vec{t_2}$ are equal +then $\vec{t_1}$ and $\vec{t_2}$ are equal too. If {\term} is a proof of a statement of conclusion {\tt {\term$_1$} = {\term$_2$}}, -then {\tt injection} applies injectivity as deep as possible to -derive the equality of all the subterms of {\term$_1$} and {\term$_2$} -placed in the same positions. For example, from {\tt (S - (S n))=(S (S (S m)))} we may derive {\tt n=(S m)}. To use this -tactic {\term$_1$} and {\term$_2$} should be elements of an inductive -set and they should be neither explicitly equal, nor structurally -different. We mean by this that, if {\tt n$_1$} and {\tt n$_2$} are -their respective normal forms, then: -\begin{itemize} -\item {\tt n$_1$} and {\tt n$_2$} should not be syntactically equal, -\item there must not exist any pair of subterms {\tt u} and {\tt w}, - {\tt u} subterm of {\tt n$_1$} and {\tt w} subterm of {\tt n$_2$} , - placed in the same positions and having different constructors as - head symbols. -\end{itemize} -If these conditions are satisfied, then, the tactic derives the -equality of all the subterms of {\term$_1$} and {\term$_2$} placed in -the same positions and puts them as antecedents of the current goal. +then {\tt injection} applies the injectivity of constructors as deep as possible to +derive the equality of all the subterms of {\term$_1$} and {\term$_2$} at positions +where {\term$_1$} and {\term$_2$} start to differ. +For example, from {\tt (S p, S n) = (q, S (S m)} we may derive {\tt S + p = q} and {\tt n = S m}. For this tactic to work, {\term$_1$} and +{\term$_2$} should be typed with an inductive +type and they should be neither convertible, nor having a different +head constructor. If these conditions are satisfied, the tactic +derives the equality of all the subterms of {\term$_1$} and +{\term$_2$} at positions where they differ and adds them as +antecedents to the conclusion of the current goal. \Example Consider the following goal: @@ -2251,6 +2294,7 @@ context using \texttt{intros until \ident}. \item \errindex{Not a projectable equality but a discriminable one} \item \errindex{Nothing to do, it is an equality between convertible terms} \item \errindex{Not a primitive equality} +\item \errindex{Nothing to inject} \end{ErrMsgs} \begin{Variants} diff --git a/doc/refman/RefMan-tus.tex b/doc/refman/RefMan-tus.tex index 017de6d484..7e5bb81a90 100644 --- a/doc/refman/RefMan-tus.tex +++ b/doc/refman/RefMan-tus.tex @@ -707,7 +707,7 @@ Once all the existential variables have been defined the derivation is completed, and a construction can be generated from the proof tree, replacing each of the existential variables by its definition. This is exactly what happens when one of the commands -\texttt{Qed}, \texttt{Save} or \texttt{Defined} is invoked +\texttt{Qed} or \texttt{Defined} is invoked (see Section~\ref{Qed}). The saved theorem becomes a defined constant, whose body is the proof object generated. diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index 9962ce9961..08cdbee503 100644 --- a/doc/refman/RefMan-uti.tex +++ b/doc/refman/RefMan-uti.tex @@ -51,6 +51,95 @@ arguments. In other cases, the debugger is simply called without additional arguments. Such a wrapper can be found in the \texttt{dev/} subdirectory of the sources. +\section[Building a \Coq\ project with {\tt coq\_makefile}] +{Building a \Coq\ project with {\tt coq\_makefile} +\label{Makefile} +\ttindex{Makefile} +\ttindex{coq\_Makefile} +\ttindex{\_CoqProject}} + +The majority of \Coq\ projects are very similar: a collection of {\tt .v} +files and eventually some {\tt .ml} ones (a \Coq\ plugin). The main piece +of metadata needed in order to build the project are the command +line options to {\tt coqc} (e.g. {\tt -R, -I}, +\SeeAlso Section~\ref{coqoptions}). Collecting the list of files and +options is the job of the {\tt \_CoqProject} file. + +A simple example of a {\tt \_CoqProject} file follows: + +\begin{verbatim} +-R theories/ MyCode +theories/foo.v +theories/bar.v +-I src/ +src/baz.ml4 +src/bazaux.ml +src/qux_plugin.mlpack +\end{verbatim} + +Currently, both \CoqIDE{} and Proof General (version $\geq$ 4.3pre) understand +{\tt \_CoqProject} files and invoke \Coq\ with the desired options. + +The {\tt coq\_makefile} utility can be used to set up a build infrastructure +for the \Coq\ project based on makefiles. The recommended way of +invoking {\tt coq\_makefile} is the following one: + +\begin{verbatim} +coq_makefile -f _CoqProject -o CoqMakefile +\end{verbatim} + +Such command generates the following files: +\begin{description} + \item[{\tt CoqMakefile}] is a generic makefile for GNU Make that provides targets to build the project (both {\tt .v} and {\tt .ml*} files), to install it system-wide in the {\tt coq-contrib} directory (i.e. where \Coq\ is installed) as well as to invoke {\tt coqdoc} to generate html documentation. + + \item[{\tt CoqMakefile.conf}] contains make variables assignments that reflect the contents of the {\tt \_CoqProject} file as well as the path relevant to \Coq{}. +\end{description} + +An optional file {\bf {\tt CoqMakefile.local}} can be provided by the user in order to extend {\tt CoqMakefile}. In particular one can declare custom actions to be performed before or after the build process. Similarly one can customize the install target or even provide new targets. Extension points are documented in the {\tt CoqMakefile} file. + +The extensions of the files listed in {\tt \_CoqProject} is +used in order to decide how to build them In particular: + +\begin{itemize} +\item {\Coq} files must use the \texttt{.v} extension +\item {\ocaml} files must use the \texttt{.ml} or \texttt{.mli} extension +\item {\ocaml} files that require pre processing for syntax extensions (like {\tt VERNAC EXTEND}) must use the \texttt{.ml4} extension +\item In order to generate a plugin one has to list all {\ocaml} modules (i.e. ``Baz'' for ``baz.ml'') in a \texttt{.mlpack} file (or \texttt{.mllib} file). +\end{itemize} + +The use of \texttt{.mlpack} files has to be preferred over \texttt{.mllib} +files, since it results in a ``packed'' plugin: All auxiliary +modules (as {\tt Baz} and {\tt Bazaux}) are hidden inside +the plugin's ``name space'' ({\tt Qux\_plugin}). +This reduces the chances of begin unable to load two distinct plugins +because of a clash in their auxiliary module names. + +\paragraph{Notes about including the generated Makefile} + +This practice is discouraged. The contents of this file, including variable names +and status of rules shall change in the future. Users are advised to +include {\tt Makefile.conf} or call a target of the generated Makefile +as in {\tt make -f Makefile target} from another Makefile. + +\paragraph{Notes for users of {\tt coq\_makefile} with version $<$ 8.7} + +\begin{itemize} +\item Support for ``sub-directory'' is deprecated. To perform actions before + or after the build (like invoking make on a subdirectory) one can + hook in {\tt pre-all} and {\tt post-all} extension points +\item \texttt{-extra-phony} and \texttt{-extra} are deprecated. To provide + additional target ({\tt .PHONY} or not) please use + {\tt CoqMakefile.local} +\end{itemize} + +\paragraph{Note: building a subset of the targets with -j} + +To build, say, two targets \texttt{foo.vo} and \texttt{bar.vo} +in parallel one can use \texttt{make only TGTS="foo.vo bar.vo" -j}. + +Note that \texttt{make foo.vo bar.vo -j} has a different meaning for +the make utility, in particular it may build a shared prerequisite twice. + \section[Modules dependencies]{Modules dependencies\label{Dependencies}\index{Dependencies} \ttindex{coqdep}} @@ -73,110 +162,9 @@ instead for the \ocaml\ modules dependencies. See the man page of {\tt coqdep} for more details and options. - -\section[Creating a {\tt Makefile} for \Coq\ modules] -{Creating a {\tt Makefile} for \Coq\ modules -\label{Makefile} -\ttindex{Makefile} -\ttindex{coq\_Makefile} -\ttindex{\_CoqProject}} - -A project is a proof development split into several files, possibly -including the sources of some {\ocaml} plugins, that are located (in -various sub-directories of) a certain directory. The -\texttt{coq\_makefile} command allows to generate generic and complete -\texttt{Makefile} files, that can be used to compile the different -components of the project. A \_CoqProject file -specifies both the list of target files relevant to the project -and the common options that should be passed to each executable at -compilation times, for the IDE, etc. - -\paragraph{\_CoqProject file as an argument to coq\_Makefile.} -In particular, a \_CoqProject file contains the relevant -arguments to be passed to the \texttt{coq\_makefile} makefile -generator using for instance the command: - -\begin{quotation} -\texttt{\% coq\_makefile -f \_CoqProject -o Makefile} -\end{quotation} - -This command generates a file \texttt{Makefile} that can be used to -compile all the sources of the current project. It follows the -syntax described by the output of \texttt{\% coq\_makefile -{}-help}. -Once the \texttt{Makefile} file has been generated a first time, it -can be used by the \texttt{make} command to compile part or all of -the project. Note that once it has been generated once, as soon as -\texttt{\_CoqProject} file is updated, the \texttt{Makefile} file is -automatically regenerated by an invocation of \texttt{make}. - -The following command generates a minimal example of -\texttt{\_CoqProject} file: -\begin{quotation} -\texttt{\% ( echo "-R .\ }\textit{MyFancyLib}\texttt{" ; find .\ -name - "*.v" -print ) > \_CoqProject} -\end{quotation} -when executed at the root of the directory containing the -project. Here the \texttt{\_CoqProject} lists all the \texttt{.v} files -that are present in the current directory and its sub-directories. But no -plugin sources is listed. If a \texttt{Makefile} is generated from -this \texttt{\_CoqProject}, the command \texttt{make install} will -install the compiled project in a sub-directory \texttt{MyFancyLib} of -the \texttt{user-contrib} directory (of the user's {\Coq} libraries -location). This sub-directory is created if it does not already exist. - -\paragraph{\_CoqProject file as a configuration for IDEs.} - -A \texttt{\_CoqProject} file can also be used to configure the options -of the \texttt{coqtop} process executed by a user interface. This -allows to import the libraries of the project under a correct name, -both as a developer of the project, working in the directory -containing its sources, and as a user, using the project after -the installation of its libraries. Currently, both \CoqIDE{} and Proof -General (version $\geq$ 4.3pre) support configuration via -\texttt{\_CoqProject} files. - -\paragraph{Remarks.} - -\begin{itemize} -\item Every {\Coq} files must use a \texttt{.v} file extension. - The {\ocaml} modules must use a \texttt{.ml4} file extension - if they require camlp preprocessing (and in \texttt{.ml} otherwise). - The {\ocaml} module signatures, library - description and packing files must use respectively \texttt{.mli}, - \texttt{.mllib} and \texttt{.mlpack} file extension. - -\item Any argument that is not a valid option is considered as a - sub-directory. Any sub-directory specified in the list of targets must - itself contain a \texttt{Makefile}. - -\item The phony targets \texttt{all} and \texttt{clean} recursively - call their target in every sub-directory. - -\item \texttt{-R} and \texttt{-Q} options are for {\Coq} files, \texttt{-I} - for {\ocaml} ones. A same directory can be passed to both nature of - options, in the same \texttt{\_CoqProject}. - -\item Using \texttt{-R} or \texttt{-Q} is the appropriate way to - obtain both a correct logical path and a correct installation location to - the libraries of a given project. - -\item Dependencies on external libraries to the project must be - declared with care. If in the \texttt{\_CoqProject} file an external - library \texttt{foo} is passed to a \texttt{-Q} option, like in - \texttt{-Q foo}, the subsequent \textit{make clean} command can - erase \textit{foo}. It is hence safer to customize the - \texttt{COQPATH} variable (see \ref{envars}), to include the - location of the required external libraries. - -\item Using \texttt{-extra-phony} with no command adds extra - dependencies on already defined rules. For example the following - skeleton appends ``something'' to the \texttt{install} rule: -\begin{quotation} -\texttt{-extra-phony "install" "install-my-stuff" "" - -extra-phony "install-my-stuff" "" "something"} -\end{quotation} -\end{itemize} - +The build infrastructure generated by {\tt coq\_makefile} +uses {\tt coqdep} to automatically compute the dependencies +among the files part of the project. \section[Documenting \Coq\ files with coqdoc]{Documenting \Coq\ files with coqdoc\label{coqdoc} \ttindex{coqdoc}} |