diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/Makefile.rt | 43 | ||||
| -rw-r--r-- | doc/RecTutorial/RecTutorial.v | 111 | ||||
| -rw-r--r-- | doc/common/title.tex | 2 | ||||
| -rw-r--r-- | doc/refman/RefMan-pre.tex | 114 | ||||
| -rw-r--r-- | doc/refman/RefMan-syn.tex | 14 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 16 | ||||
| -rw-r--r-- | doc/refman/RefMan-uti.tex | 80 | ||||
| -rw-r--r-- | doc/rt/RefMan-cover.tex | 45 | ||||
| -rw-r--r-- | doc/rt/Tutorial-cover.tex | 47 | ||||
| -rw-r--r-- | doc/tools/Translator.tex | 2 |
10 files changed, 251 insertions, 223 deletions
diff --git a/doc/Makefile.rt b/doc/Makefile.rt deleted file mode 100644 index 6c32813462..0000000000 --- a/doc/Makefile.rt +++ /dev/null @@ -1,43 +0,0 @@ -# Makefile for building Coq Technical Reports - -# if coqc,coqtop,coq-tex are not in your PATH, you need the environment -# variable COQBIN to be correctly set -# (COQTOP is autodetected) -# (some files are preprocessed using Coq and some part of the documentation -# is automatically built from the theories sources) - -# To compile documentation, you need the following tools: -# Dvi: latex (latex2e), bibtex, makeindex, dviselect (package RPM dviutils) -# Ps: dvips, psutils (ftp://ftp.dcs.ed.ac.uk/pub/ajcd/psutils.tar.gz) -# Pdf: pdflatex -# Html: -# - hevea: http://para.inria.fr/~maranget/hevea/ -# - htmlSplit: http://coq.inria.fr/~delahaye -# Rapports INRIA: dviselect, rrkit (par Michel Mauny) - -include ./Makefile - -################### -# RT -################### -# Fabrication d'un RT INRIA (utilise rrkit de Michel Mauny) -rt/Reference-Manual-RT.dvi: refman/Reference-Manual.dvi rt/RefMan-cover.tex - dviselect -i refman/Reference-Manual.dvi -o rt/RefMan-body.dvi 3: - (cd rt; $(LATEX) RefMan-cover.tex) - set a=`tail -1 refman/Reference-Manual.log`;\ - set a=expr \("$$a" : '.*(\(.*\) pages.*'\) % 2;\ - (cd rt; if $(TEST) "$$a = 0";\ - then rrkit RefMan-cover.dvi RefMan-body.dvi Reference-Manual-RT.dvi;\ - else rrkit -odd RefMan-cover.dvi RefMan-body.dvi Reference-Manual-RT.dvi;\ - fi) - -# Fabrication d'un RT INRIA (utilise rrkit de Michel Mauny) -rt/Tutorial-RT.dvi : tutorial/Tutorial.v.dvi rt/Tutorial-cover.tex - dviselect -i rt/Tutorial.v.dvi -o rt/Tutorial-body.dvi 3: - (cd rt; $(LATEX) Tutorial-cover.tex) - set a=`tail -1 tutorial/Tutorial.v.log`;\ - set a=expr \("$$a" : '.*(\(.*\) pages.*'\) % 2;\ - (cd rt; if $(TEST) "$$a = 0";\ - then rrkit Tutorial-cover.dvi Tutorial-body.dvi Tutorial-RT.dvi;\ - else rrkit -odd Tutorial-cover.dvi Tutorial-body.dvi Tutorial-RT.dvi;\ - fi) diff --git a/doc/RecTutorial/RecTutorial.v b/doc/RecTutorial/RecTutorial.v index 8cfeebc28b..4b0ab31254 100644 --- a/doc/RecTutorial/RecTutorial.v +++ b/doc/RecTutorial/RecTutorial.v @@ -1,3 +1,5 @@ +Unset Automatic Introduction. + Check (forall A:Type, (exists x:A, forall (y:A), x <> y) -> 2 = 3). @@ -69,13 +71,13 @@ Check (Prop::Set::nil). Require Import Bvector. -Print vector. +Print Vector.t. -Check (Vnil nat). +Check (Vector.nil nat). -Check (fun (A:Type)(a:A)=> Vcons _ a _ (Vnil _)). +Check (fun (A:Type)(a:A)=> Vector.cons _ a _ (Vector.nil _)). -Check (Vcons _ 5 _ (Vcons _ 3 _ (Vnil _))). +Check (Vector.cons _ 5 _ (Vector.cons _ 3 _ (Vector.nil _))). Lemma eq_3_3 : 2 + 1 = 3. Proof. @@ -146,6 +148,7 @@ Proof. intros; absurd (p < p); eauto with arith. Qed. +Require Extraction. Extraction max. @@ -300,8 +303,8 @@ Section Le_case_analysis. (HS : forall m, n <= m -> Q (S m)). Check ( match H in (_ <= q) return (Q q) with - | le_n => H0 - | le_S m Hm => HS m Hm + | le_n _ => H0 + | le_S _ m Hm => HS m Hm end ). @@ -317,16 +320,16 @@ Proof. Qed. Definition Vtail_total - (A : Type) (n : nat) (v : vector A n) : vector A (pred n):= -match v in (vector _ n0) return (vector A (pred n0)) with -| Vnil => Vnil A -| Vcons _ n0 v0 => v0 + (A : Type) (n : nat) (v : Vector.t A n) : Vector.t A (pred n):= +match v in (Vector.t _ n0) return (Vector.t A (pred n0)) with +| Vector.nil _ => Vector.nil A +| Vector.cons _ _ n0 v0 => v0 end. -Definition Vtail' (A:Type)(n:nat)(v:vector A n) : vector A (pred n). +Definition Vtail' (A:Type)(n:nat)(v:Vector.t A n) : Vector.t A (pred n). intros A n v; case v. simpl. - exact (Vnil A). + exact (Vector.nil A). simpl. auto. Defined. @@ -498,10 +501,8 @@ Inductive typ : Type := Definition typ_inject: typ. split. -exact typ. +Fail exact typ. (* -Defined. - Error: Universe Inconsistency. *) Abort. @@ -920,7 +921,6 @@ Defined. Print minus_decrease. - Definition div_aux (x y:nat)(H: Acc lt x):nat. fix 3. intros. @@ -969,40 +969,40 @@ let rec div_aux x y = | Right -> div_aux (minus x y) y) *) -Lemma vector0_is_vnil : forall (A:Type)(v:vector A 0), v = Vnil A. +Lemma vector0_is_vnil : forall (A:Type)(v:Vector.t A 0), v = Vector.nil A. Proof. intros A v;inversion v. Abort. (* - Lemma vector0_is_vnil_aux : forall (A:Type)(n:nat)(v:vector A n), - n= 0 -> v = Vnil A. + Lemma vector0_is_vnil_aux : forall (A:Type)(n:nat)(v:Vector.t A n), + n= 0 -> v = Vector.nil A. Toplevel input, characters 40281-40287 -> Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:vector A n), n= 0 -> v = Vnil A. +> Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:Vector.t A n), n= 0 -> v = Vector.nil A. > ^^^^^^ Error: In environment A : Set n : nat -v : vector A n +v : Vector.t A n e : n = 0 -The term "Vnil A" has type "vector A 0" while it is expected to have type - "vector A n" +The term "Vector.nil A" has type "Vector.t A 0" while it is expected to have type + "Vector.t A n" *) Require Import JMeq. (* On devrait changer Set en Type ? *) -Lemma vector0_is_vnil_aux : forall (A:Type)(n:nat)(v:vector A n), - n= 0 -> JMeq v (Vnil A). +Lemma vector0_is_vnil_aux : forall (A:Type)(n:nat)(v:Vector.t A n), + n= 0 -> JMeq v (Vector.nil A). Proof. destruct v. auto. intro; discriminate. Qed. -Lemma vector0_is_vnil : forall (A:Type)(v:vector A 0), v = Vnil A. +Lemma vector0_is_vnil : forall (A:Type)(v:Vector.t A 0), v = Vector.nil A. Proof. intros a v;apply JMeq_eq. apply vector0_is_vnil_aux. @@ -1010,56 +1010,56 @@ Proof. Qed. -Implicit Arguments Vcons [A n]. -Implicit Arguments Vnil [A]. -Implicit Arguments Vhead [A n]. -Implicit Arguments Vtail [A n]. +Implicit Arguments Vector.cons [A n]. +Implicit Arguments Vector.nil [A]. +Implicit Arguments Vector.hd [A n]. +Implicit Arguments Vector.tl [A n]. -Definition Vid : forall (A : Type)(n:nat), vector A n -> vector A n. +Definition Vid : forall (A : Type)(n:nat), Vector.t A n -> Vector.t A n. Proof. destruct n; intro v. - exact Vnil. - exact (Vcons (Vhead v) (Vtail v)). + exact Vector.nil. + exact (Vector.cons (Vector.hd v) (Vector.tl v)). Defined. -Eval simpl in (fun (A:Type)(v:vector A 0) => (Vid _ _ v)). +Eval simpl in (fun (A:Type)(v:Vector.t A 0) => (Vid _ _ v)). -Eval simpl in (fun (A:Type)(v:vector A 0) => v). +Eval simpl in (fun (A:Type)(v:Vector.t A 0) => v). -Lemma Vid_eq : forall (n:nat) (A:Type)(v:vector A n), v=(Vid _ n v). +Lemma Vid_eq : forall (n:nat) (A:Type)(v:Vector.t A n), v=(Vid _ n v). Proof. destruct v. reflexivity. reflexivity. Defined. -Theorem zero_nil : forall A (v:vector A 0), v = Vnil. +Theorem zero_nil : forall A (v:Vector.t A 0), v = Vector.nil. Proof. intros. - change (Vnil (A:=A)) with (Vid _ 0 v). + change (Vector.nil (A:=A)) with (Vid _ 0 v). apply Vid_eq. Defined. Theorem decomp : - forall (A : Type) (n : nat) (v : vector A (S n)), - v = Vcons (Vhead v) (Vtail v). + forall (A : Type) (n : nat) (v : Vector.t A (S n)), + v = Vector.cons (Vector.hd v) (Vector.tl v). Proof. intros. - change (Vcons (Vhead v) (Vtail v)) with (Vid _ (S n) v). + change (Vector.cons (Vector.hd v) (Vector.tl v)) with (Vid _ (S n) v). apply Vid_eq. Defined. Definition vector_double_rect : - forall (A:Type) (P: forall (n:nat),(vector A n)->(vector A n) -> Type), - P 0 Vnil Vnil -> - (forall n (v1 v2 : vector A n) a b, P n v1 v2 -> - P (S n) (Vcons a v1) (Vcons b v2)) -> - forall n (v1 v2 : vector A n), P n v1 v2. + forall (A:Type) (P: forall (n:nat),(Vector.t A n)->(Vector.t A n) -> Type), + P 0 Vector.nil Vector.nil -> + (forall n (v1 v2 : Vector.t A n) a b, P n v1 v2 -> + P (S n) (Vector.cons a v1) (Vector.cons b v2)) -> + forall n (v1 v2 : Vector.t A n), P n v1 v2. induction n. intros; rewrite (zero_nil _ v1); rewrite (zero_nil _ v2). auto. @@ -1069,24 +1069,23 @@ Defined. Require Import Bool. -Definition bitwise_or n v1 v2 : vector bool n := - vector_double_rect bool (fun n v1 v2 => vector bool n) - Vnil - (fun n v1 v2 a b r => Vcons (orb a b) r) n v1 v2. - +Definition bitwise_or n v1 v2 : Vector.t bool n := + vector_double_rect bool (fun n v1 v2 => Vector.t bool n) + Vector.nil + (fun n v1 v2 a b r => Vector.cons (orb a b) r) n v1 v2. -Fixpoint vector_nth (A:Type)(n:nat)(p:nat)(v:vector A p){struct v} +Fixpoint vector_nth (A:Type)(n:nat)(p:nat)(v:Vector.t A p){struct v} : option A := match n,v with - _ , Vnil => None - | 0 , Vcons b _ _ => Some b - | S n', Vcons _ p' v' => vector_nth A n' p' v' + _ , Vector.nil => None + | 0 , Vector.cons b _ => Some b + | S n', @Vector.cons _ _ p' v' => vector_nth A n' p' v' end. Implicit Arguments vector_nth [A p]. -Lemma nth_bitwise : forall (n:nat) (v1 v2: vector bool n) i a b, +Lemma nth_bitwise : forall (n:nat) (v1 v2: Vector.t bool n) i a b, vector_nth i v1 = Some a -> vector_nth i v2 = Some b -> vector_nth i (bitwise_or _ v1 v2) = Some (orb a b). 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-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-syn.tex b/doc/refman/RefMan-syn.tex index 084317776b..d8a353300f 100644 --- a/doc/refman/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex @@ -980,7 +980,7 @@ delimited by key {\tt nat}, and bound to the type {\tt nat} (see \ref{bindscope} This scope includes the standard arithmetical operators and relations on type {\tt N} (binary natural numbers). It is delimited by key {\tt N} -and comes with an interpretation for numerals as closed term of type {\tt Z}. +and comes with an interpretation for numerals as closed term of type {\tt N}. \subsubsection{\tt Z\_scope} @@ -1014,16 +1014,8 @@ fractions of an integer and a strictly positive integer. This scope includes the standard arithmetical operators and relations on type {\tt R} (axiomatic real numbers). It is delimited by key {\tt R} -and comes with an interpretation for numerals as term of type {\tt -R}. The interpretation is based on the binary decomposition. The -numeral 2 is represented by $1+1$. The interpretation $\phi(n)$ of an -odd positive numerals greater $n$ than 3 is {\tt 1+(1+1)*$\phi((n-1)/2)$}. -The interpretation $\phi(n)$ of an even positive numerals greater $n$ -than 4 is {\tt (1+1)*$\phi(n/2)$}. Negative numerals are represented as the -opposite of the interpretation of their absolute value. E.g. the -syntactic object {\tt -11} is interpreted as {\tt --(1+(1+1)*((1+1)*(1+(1+1))))} where the unit $1$ and all the operations are -those of {\tt R}. +and comes with an interpretation for numerals using the {\tt IZR} +morphism from binary integer numbers to {\tt R}. \subsubsection{\tt bool\_scope} diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index b3b0df5c8a..6e27357008 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3269,7 +3269,7 @@ The call-by-value strategy is the one used in ML languages: the arguments of a function call are systematically weakly evaluated first. Despite the lazy strategy always performs fewer reductions than the call-by-value strategy, the latter is generally more efficient for -evaluating purely computational expressions (i.e. with few dead code). +evaluating purely computational expressions (i.e. with little dead code). \begin{Variants} \item {\tt compute} \tacindex{compute}\\ @@ -3317,6 +3317,20 @@ evaluating purely computational expressions (i.e. with few dead code). compilation cost is higher, so it is worth using only for intensive computations. + On Linux, if you have the {\tt perf} profiler installed, you can profile {\tt native\_compute} evaluations. + The command + \begin{quote} + {\tt Set Native Compute Profiling} + \end{quote} + enables profiling. Use the command + \begin{quote} + {\tt Set NativeCompute Profile Filename \str} + \end{quote} + to specify the profile output; the default is {\tt native\_compute\_profile.data}. The actual filename used + will contain extra characters to avoid overwriting an existing file; that filename is reported to the user. That means + you can individually profile multiple uses of {\tt native\_compute} in a script. From the Linux command line, run {\tt perf report} on + the profile file to see the results. Consult the {\tt perf} documentation for more details. + \end{Variants} % Obsolete? Anyway not very important message 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/rt/RefMan-cover.tex b/doc/rt/RefMan-cover.tex deleted file mode 100644 index ac1686c25e..0000000000 --- a/doc/rt/RefMan-cover.tex +++ /dev/null @@ -1,45 +0,0 @@ -\documentstyle[RRcover]{book} - % The use of the style `french' forces the french abstract to appear first. - -\RRtitle{Manuel de r\'ef\'erence du syst\`eme Coq \\ version V7.1} -\RRetitle{The Coq Proof Assistant \\ Reference Manual \\ Version 7.1 -\thanks -{This research was partly supported by ESPRIT Basic Research -Action ``Types'' and by the GDR ``Programmation'' co-financed by MRE-PRC and CNRS.} -} -\RRauthor{Bruno Barras, Samuel Boutin, Cristina Cornes, -Judica\"el Courant, Jean-Christophe Filli\^atre, Eduardo Gim\'enez, -Hugo Herbelin, G\'erard Huet, C\'esar Mu\~noz, Chetan Murthy, -Catherine Parent, Christine Paulin-Mohring, -Amokrane Sa{\"\i}bi, Benjamin Werner} -\authorhead{} -\titlehead{Coq V7.1 Reference Manual} -\RRtheme{2} -\RRprojet{Coq} -\RRNo{0123456789} -\RRdate{May 1997} -%\RRpages{} -\URRocq - -\RRresume{Coq est un syst\`eme permettant le d\'eveloppement et la -v\'erification de preuves formelles dans une logique d'ordre -sup\'erieure incluant un riche langage de d\'efinitions de fonctions. -Ce document constitue le manuel de r\'ef\'erence de la version V7.1 -qui est distribu\'ee par ftp anonyme \`a l'adresse -\url{ftp://ftp.inria.fr/INRIA/coq/}} - -\RRmotcle{Coq, Syst\`eme d'aide \`a la preuve, Preuves formelles, -Calcul des Constructions Inductives} - - -\RRabstract{Coq is a proof assistant based on a higher-order logic -allowing powerful definitions of functions. -Coq V7.1 is available by anonymous -ftp at \url{ftp://ftp.inria.fr/INRIA/coq/}} - -\RRkeyword{Coq, Proof Assistant, Formal Proofs, Calculus of Inductives -Constructions} - -\begin{document} -\makeRT -\end{document} diff --git a/doc/rt/Tutorial-cover.tex b/doc/rt/Tutorial-cover.tex deleted file mode 100644 index aefea8d429..0000000000 --- a/doc/rt/Tutorial-cover.tex +++ /dev/null @@ -1,47 +0,0 @@ -\documentstyle[RRcover]{book} - % The use of the style `french' forces the french abstract to appear first. -\RRetitle{ -The Coq Proof Assistant \\ A Tutorial \\ Version 7.1 -\thanks{This research was partly supported by ESPRIT Basic Research -Action ``Types'' and by the GDR ``Programmation'' co-financed by MRE-PRC and CNRS.} -} -\RRtitle{Coq \\ Une introduction \\ V7.1 } -\RRauthor{G\'erard Huet, Gilles Kahn and Christine Paulin-Mohring} -\RRtheme{2} -\RRprojet{{Coq -\\[15pt] -{INRIA Rocquencourt} -{\hskip -5.25pt} -~~{\bf ---}~~ - \def\thefootnote{\arabic{footnote}\hss} -{CNRS - ENS Lyon} -\footnote[1]{LIP URA 1398 du CNRS, -46 All\'ee d'Italie, 69364 Lyon CEDEX 07, France.} -{\hskip -14pt}}} - -%\RRNo{0123456789} -\RRNo{0204} -\RRdate{Ao\^ut 1997} - -\URRocq -\RRresume{Coq est un syst\`eme permettant le d\'eveloppement et la -v\'erification de preuves formelles dans une logique d'ordre -sup\'erieure incluant un riche langage de d\'efinitions de fonctions. -Ce document constitue une introduction pratique \`a l'utilisation de -la version V7.1 qui est distribu\'ee par ftp anonyme \`a l'adresse -\url{ftp://ftp.inria.fr/INRIA/coq/}} - -\RRmotcle{Coq, Syst\`eme d'aide \`a la preuve, Preuves formelles, Calcul -des Constructions Inductives} - -\RRabstract{Coq is a proof assistant based on a higher-order logic -allowing powerful definitions of functions. This document is a -tutorial for the version V7.1 of Coq. This version is available by -anonymous ftp at \url{ftp://ftp.inria.fr/INRIA/coq/}} - -\RRkeyword{Coq, Proof Assistant, Formal Proofs, Calculus of Inductives -Constructions} - -\begin{document} -\makeRT -\end{document} diff --git a/doc/tools/Translator.tex b/doc/tools/Translator.tex index ed1d336d9e..3ee65d6f22 100644 --- a/doc/tools/Translator.tex +++ b/doc/tools/Translator.tex @@ -614,7 +614,7 @@ is compiled by a Makefile with the following constraints: \begin{itemize} \item compilation is achieved by invoking make without specifying a target \item options are passed to Coq with make variable COQFLAGS that - includes variables OPT, COQLIBS, OTHERFLAGS and COQ_XML. + includes variables OPT, COQLIBS, and OTHERFLAGS. \end{itemize} These constraints are met by the makefiles produced by {\tt coq\_makefile} |