diff options
Diffstat (limited to 'doc/refman')
| -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 |
3 files changed, 80 insertions, 30 deletions
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}} |