diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/common/title.tex | 2 | ||||
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 78 | ||||
| -rw-r--r-- | doc/refman/RefMan-pre.tex | 114 | ||||
| -rw-r--r-- | doc/refman/RefMan-ssr.tex | 12 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 2 | ||||
| -rw-r--r-- | doc/refman/RefMan-uti.tex | 80 | ||||
| -rw-r--r-- | doc/refman/Setoid.tex | 2 |
7 files changed, 252 insertions, 38 deletions
diff --git a/doc/common/title.tex b/doc/common/title.tex index 0e072b6b65..76e50f65d2 100644 --- a/doc/common/title.tex +++ b/doc/common/title.tex @@ -45,7 +45,7 @@ V\coqversion, \today %END LATEX \copyright INRIA 1999-2004 ({\Coq} versions 7.x) -\copyright INRIA 2004-2016 ({\Coq} versions 8.x) +\copyright INRIA 2004-2017 ({\Coq} versions 8.x) #3 \end{flushleft} diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 713f344cbe..7af4e9313a 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -279,15 +279,78 @@ of the chapter devoted to coercions. \label{prim-proj} The option {\tt Set Primitive Projections} turns on the use of primitive -projections when defining subsequent records. Primitive projections +projections when defining subsequent records (even through the {\tt + Inductive} and {\tt CoInductive} commands). Primitive projections extended the Calculus of Inductive Constructions with a new binary term constructor {\tt r.(p)} representing a primitive projection p applied to a record object {\tt r} (i.e., primitive projections are always applied). Even if the record type has parameters, these do not appear at applications of the projection, considerably reducing the sizes of terms when manipulating parameterized records and typechecking time. On the -user level, primitive projections are a transparent replacement -for the usual defined ones. +user level, primitive projections can be used as a replacement for the +usual defined ones, although there are a few notable differences. + +The internally omitted parameters can be reconstructed at printing time +even though they are absent in the actual AST manipulated by the kernel. This +can be obtained by setting the {\tt Printing Primitive Projection Parameters} +flag. Another compatibility printing can be activated thanks to the +{\tt Printing Primitive Projection Compatibility} option which governs the +printing of pattern-matching over primitive records. + +\subsubsection{Primitive Record Types} +When the {\tt Set Primitive Projections} option is on, definitions of +record types change meaning. When a type is declared with primitive +projections, its {\tt match} construct is disabled (see +\ref{primproj:compat} though). To eliminate the (co-)inductive type, one +must use its defined primitive projections. + +There are currently two ways to introduce primitive records types: +\begin{itemize} +\item Through the {\tt Record} command, in which case the type has to be + non-recursive. The defined type enjoys eta-conversion definitionally, + that is the generalized form of surjective pairing for records: + {\tt $r$ = Build\_R ($r$.($p_1$) .. $r$.($p_n$))}. Eta-conversion allows to define + dependent elimination for these types as well. +\item Through the {\tt Inductive} and {\tt CoInductive} commands, when + the body of the definition is a record declaration of the form {\tt + Build\_R \{ $p_1$ : $t_1$; .. ; $p_n$ : $t_n$ \}}. In this case the types can be + recursive and eta-conversion is disallowed. These kind of record types + differ from their traditional versions in the sense that dependent + elimination is not available for them and only non-dependent case analysis + can be defined. +\end{itemize} + +\subsubsection{Reduction} + +The basic reduction rule of a primitive projection is {\tt $p_i$ + (Build\_R $t_1$ .. $t_n$) $\rightarrow_{\iota}$ $t_i$}. However, to take the $\delta$ flag into +account, projections can be in two states: folded or unfolded. An +unfolded primitive projection application obeys the rule above, while +the folded version delta-reduces to the unfolded version. This allows to +precisely mimic the usual unfolding rules of constants. Projections +obey the usual {\tt simpl} flags of the {\tt Arguments} command in particular. + +There is currently no way to input unfolded primitive projections at the +user-level, and one must use the {\tt Printing Primitive Projection + Compatibility} to display unfolded primitive projections as matches +and distinguish them from folded ones. + +\subsubsection{Compatibility Projections and {\tt match}} +\label{primproj:compat} +To ease compatibility with ordinary record types, each primitive +projection is also defined as a ordinary constant taking parameters and +an object of the record type as arguments, and whose body is an +application of the unfolded primitive projection of the same name. These +constants are used when elaborating partial applications of the +projection. One can distinguish them from applications of the primitive +projection if the {\tt Printing Primitive Projection Parameters} option +is off: for a primitive projection application, parameters are printed +as underscores while for the compatibility projections they are printed +as usual. + +Additionally, user-written {\tt match} constructs on primitive records +are desugared into substitution of the projections, they cannot be +printed back as {\tt match} constructs. % - r.(p) and (p r) elaborate to native projection application, and % the parameters cannot be mentioned. The following arguments are @@ -305,13 +368,6 @@ for the usual defined ones. % - [pattern x at n], [rewrite x at n] and in general abstraction and selection % of occurrences may fail due to the disappearance of parameters. -The internally omitted parameters can be reconstructed at printing time -even though they are absent in the actual AST manipulated by the kernel. This -can be obtained by setting the {\tt Printing Primitive Projection Parameters} -flag. Another compatibility printing can be activated thanks to the -{\tt Printing Primitive Projection Compatibility} option which governs the -printing of pattern-matching over primitive records. - \section{Variants and extensions of {\mbox{\tt match}} \label{Extensions-of-match} \index{match@{\tt match\ldots with\ldots end}}} @@ -1664,7 +1720,7 @@ to be given as if none arguments were implicit. By symmetry, this also affects printing. To restore parsing and normal printing of implicit arguments, use: \begin{quote} -{\tt Set Parsing Explicit.} +{\tt Unset Parsing Explicit.} \end{quote} \subsection{Canonical structures diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index 0441f952df..0c2a18eb2e 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -1220,6 +1220,120 @@ Paris, November 2016,\\ Matthieu Sozeau and the {\Coq} development team\\ \end{flushright} +\section*{Credits: version 8.7} + +{\Coq} version 8.7 contains the result of refinements, stabilization of +features and cleanups of the internals of the system along with a few +new features. The main user visible changes are: +\begin{itemize} +\item New tactics: variants of tactics supporting existential variables + \texttt{eassert}, \texttt{eenough}, etc... by Hugo Herbelin. Tactics + \texttt{extensionality in H} and \texttt{inversion\_sigma} by Jason + Gross, \texttt{specialize with ...} accepting partial bindings by + Pierre Courtieu. +\item Cumulative Polymorphic Inductive Types, allowing cumulativity of + universes to go through applied inductive types, by Amin Timany and + Matthieu Sozeau. +\item Integration of the \texttt{SSReflect} plugin and its documentation in the + reference manual, by Enrico Tassi, Assia Mahboubi and Maxime Dénès. +\item The \texttt{coq\_makefile} tool was completely redesigned to improve its + maintainability and the extensibility of generated Makefiles, and to + make \texttt{\_CoqProject} files more palatable to IDEs by Enrico Tassi. +\end{itemize} + +{\Coq} 8.7 involved a large amount of work on cleaning and speeding up +the code base, notably the work of Pierre-Marie Pédrot on making the +tactic-level system insensitive to existential variable expansion, +providing a safer API to plugin writers and making the code more +robust. The \texttt{dev/doc/changes.txt} file documents the numerous +changes to the implementation and improvements of interfaces. An effort +to provide an official, streamlined API to plugin writers is in +progress, thanks to the work of Matej Košík. + +Version 8.7 also comes with a bunch of smaller-scale changes and improvements +regarding the different components of the system. We shall only list a +few of them. + +The efficiency of the whole system has been significantly improved +thanks to contributions from Pierre-Marie Pédrot, Maxime Dénès and +Matthieu Sozeau and performance issue tracking by Jason Gross and Paul +Steckler. + +Thomas Sibut-Pinote and Hugo Herbelin added support for side effects +hooks in \texttt{cbv}, \texttt{cbn} and \texttt{simpl}. The side +effects are provided via a plugin available at +\url{https://github.com/herbelin/reduction-effects/}. + +The \texttt{BigN}, \texttt{BigZ}, \texttt{BigQ} libraries are no longer +part of the {\Coq} standard library, they are now provided by a separate +repository \url{https://github.com/coq/bignums}, maintained by Pierre +Letouzey. + +In the \texttt{Reals} library, \texttt{IZR} has been changed to produce +a compact representation of integers and real constants are now +represented using \texttt{IZR} (work by Guillaume Melquiond). + +Standard library additions and improvements by Jason Gross, Pierre +Letouzey and others, documented in the CHANGES file. + +The mathematical proof language/declarative mode plugin was removed from +the archive. + +The OPAM repository for {\Coq} packages has been maintained by Guillaume +Melquiond, Matthieu Sozeau, Enrico Tassi with contributions from many +users. A list of packages is available at +\url{https://coq.inria.fr/opam/www/}. + +Packaging tools and software development kits were prepared by Michael +Soegtrop with the help of Maxime Dénès and Enrico Tassi for Windows, and +Maxime Dénès for MacOS X. Packages are regularly built on the +Travis continuous integration server. + +The contributors for this version are Abhishek Anand, C.J. Bell, Yves +Bertot, Frédéric Besson, Tej Chajed, Pierre Courtieu, Maxime Dénès, +Julien Forest, Gaëtan Gilbert, Jason Gross, Hugo Herbelin, Emilio Jesús +Gallego Arias, Ralf Jung, Matej Košík, Xavier Leroy, Pierre Letouzey, +Assia Mahboubi, Cyprien Mangin, Erik Martin-Dorel, Olivier Marty, +Guillaume Melquiond, Sam Pablo Kuper, Benjamin Pierce, Pierre-Marie +Pédrot, Lars Rasmusson, Lionel Rieg, Valentin Robert, Yann Régis-Gianas, +Thomas Sibut-Pinote, Michael Soegtrop, Matthieu Sozeau, Arnaud Spiwack, +Paul Steckler, George Stelle, Pierre-Yves Strub, Enrico Tassi, Hendrik +Tews, Amin Timany, Laurent Théry, Vadim Zaliva and Théo Zimmermann. + +The development process was coordinated by Matthieu Sozeau with the help +of Maxime Dénès, who was also in charge of the release process. Théo +Zimmermann is the maintainer of this release. + +Many power users helped to improve the design of the new features via +the bug tracker, the pull request system, the {\Coq} development mailing +list or the coq-club mailing list. Special thanks to the users who +contributed patches and intensive brain-storming and code reviews, +starting with Jason Gross, Ralf Jung, Robbert Krebbers, Xavier Leroy, +Clément Pit--Claudel and Gabriel Scherer. It would however be impossible +to mention exhaustively the names of everybody who to some extent +influenced the development. + +Version 8.7 is the second release of {\Coq} developed on a time-based +development cycle. Its development spanned 9 months from the release of +{\Coq} 8.6 and was based on a public road-map. It attracted many external +contributions. Code reviews and continuous integration testing were +systematically used before integration of new features, with an +important focus given to compatibility and performance issues, resulting +in a hopefully more robust release than {\Coq} 8.6 while maintaining +compatibility. + +Coq Enhancement Proposals (CEPs for short) and open pull-requests +discussions were used to discuss publicly the new features. + +The {\Coq} consortium, an organization directed towards users and +supporters of the system, is now upcoming and will rely on Inria's +newly created Foundation. + +\begin{flushright} +Paris, August 2017,\\ +Matthieu Sozeau and the {\Coq} development team\\ +\end{flushright} + %new Makefile diff --git a/doc/refman/RefMan-ssr.tex b/doc/refman/RefMan-ssr.tex index 61f7421c44..db794e5a63 100644 --- a/doc/refman/RefMan-ssr.tex +++ b/doc/refman/RefMan-ssr.tex @@ -42,7 +42,7 @@ Proofs written in \ssr{} typically look quite different from the ones written using only tactics as per Chapter~\ref{Tactics}. We try to summarise here the most ``visible'' ones in order to help the reader already accustomed to the tactics described in -Chapter~\ref{Tactics}to read this chapter. +Chapter~\ref{Tactics} to read this chapter. The first difference between the tactics described in this chapter and the tactics described in Chapter~\ref{Tactics} is the way @@ -79,19 +79,19 @@ expansion and partial evaluation participate all to a same concept of rewriting a goal in a larger sense. As such, all these functionalities are provided by the \ssrC{rewrite} tactic. -\ssrC{} includes a little language of patterns to select subterms in tactics +\ssr{} includes a little language of patterns to select subterms in tactics or tacticals where it matters. Its most notable application is in the \ssrC{rewrite} tactic, where patterns are used to specify where the rewriting step has to take place. -Finally, \ssr{} supports the so-called reflection steps, typically +Finally, \ssr{} supports so-called reflection steps, typically allowing to switch back and forth between the computational view and logical view of a concept. To conclude it is worth mentioning that \ssr{} tactics can be mixed with non \ssr{} tactics in the same proof, -or in the same LTac expression. The few exceptions -to this statement are described in section~\label{sec:compat}. +or in the same Ltac expression. The few exceptions +to this statement are described in section~\ref{sec:compat}. \iffalse %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -130,7 +130,7 @@ ProofGeneral provided in the distribution: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \subsection*{Acknowledgments} -The authors would like to thank Fr\'ed\'eric Blanqui, Fran\,cois Pottier +The authors would like to thank Frédéric Blanqui, François Pottier and Laurence Rideau for their comments and suggestions. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 6e27357008..8fbcfdf308 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3309,7 +3309,7 @@ evaluating purely computational expressions (i.e. with little dead code). fine-tuned. It is specially interesting for full evaluation of algebraic objects. This includes the case of reflection-based tactics. -\item {\tt native\_compute} \tacindex{native\_compute} +\item {\tt native\_compute} \tacindex{native\_compute} \optindex{NativeCompute Profiling} This tactic evaluates the goal by compilation to \ocaml{} as described in \cite{FullReduction}. If \Coq{} is running in native code, it can be typically diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index 768d0df763..f6371f8e5c 100644 --- a/doc/refman/RefMan-uti.tex +++ b/doc/refman/RefMan-uti.tex @@ -51,6 +51,8 @@ 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} @@ -95,7 +97,7 @@ Such command generates the following files: \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. +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 paragraph \ref{coqmakefile:local}. The extensions of the files listed in {\tt \_CoqProject} is used in order to decide how to build them. In particular: @@ -114,7 +116,52 @@ 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{Timing targets and performance testing} +\paragraph{CoqMakefile.local} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\label{coqmakefile:local} + +The optional file {\tt CoqMakefile.local} is included by the generated file +{\tt CoqMakefile}. Such can contain two kinds of directives. + +\begin{description} + \item[Variable assignment] to the variables listed in the {\tt Parameters} + section of the generated makefile. Here we describe only few of them. + \begin{description} + \item[CAMLPKGS] can be used to specify third party findlib packages, and is + passed to the OCaml compiler on building or linking of modules. + Eg: {\tt -package yojson}. + \item[CAMLFLAGS] can be used to specify additional flags to the OCaml + compiler, like {\tt -bin-annot} or {\tt -w...}. + \item[COQC, COQDEP, COQDOC] can be set in order to use alternative + binaries (e.g. wrappers) + \end{description} +\item[Rule extension] + The following makefile rules can be extended. For example +\begin{verbatim} +pre-all:: + echo "This line is print before making the all target" +install-extra:: + cp ThisExtraFile /there/it/goes +\end{verbatim} + \begin{description} + \item[pre-all::] run before the {\tt all} target. One can use this + to configure the project, or initialize sub modules or check + dependencies are met. + \item[post-all::] run after the {\tt all} target. One can use this + to run a test suite, or compile extracted code. + \item[install-extra::] run after {\tt install}. One can use this + to install extra files. + \item[install-doc::] One can use this to install extra doc. + \item[uninstall::] + \item[uninstall-doc::] + \item[clean::] + \item[cleanall::] + \item[archclean::] + \item[merlin-hook::] One can append lines to the generated {\tt .merlin} + file extending this target. + \end{description} +\end{description} + +\paragraph{Timing targets and performance testing} %%%%%%%%%%%%%%%%%%%%%%%%%%% The generated \texttt{Makefile} supports the generation of two kinds of timing data: per-file build-times, and per-line times for an individual file. @@ -273,9 +320,10 @@ After | Code | Before || C \texttt{Note}: This target requires \texttt{python} to build the table. \end{itemize} -\paragraph{Notes about including the generated Makefile} +\paragraph{Reusing/extending the generated Makefile} %%%%%%%%%%%%%%%%%%%%%%%%% -This practice is discouraged. The contents of this file, including variable names +Including the generated makefile with an {\tt include} directive 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. @@ -303,21 +351,23 @@ invoke-coqmakefile: CoqMakefile .PHONY: invoke-coqmakefile $(KNOWNFILES) #################################################################### -#################################################################### -#################################################################### -#################################################################### ## Your targets here ## #################################################################### -#################################################################### -#################################################################### -#################################################################### # This should be the last rule, to handle any targets not declared above %: invoke-coqmakefile @true \end{verbatim} -\paragraph{Notes for users of {\tt coq\_makefile} with version $<$ 8.7} +\paragraph{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. + +\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 @@ -328,13 +378,7 @@ invoke-coqmakefile: CoqMakefile {\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}} diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex index 6c79284389..0c8cd408f2 100644 --- a/doc/refman/Setoid.tex +++ b/doc/refman/Setoid.tex @@ -223,7 +223,7 @@ the following command. \comindex{Add Parametric Morphism} \begin{quote} - \texttt{Add Parametric Morphism} ($x_1 : \T_!$) \ldots ($x_k : \T_k$)\\ + \texttt{Add Parametric Morphism} ($x_1 : \T_1$) \ldots ($x_k : \T_k$) : (\textit{f $t_1$ \ldots $t_n$})\\ \texttt{~with signature} \textit{sig}\\ \texttt{~as id}.\\ |