Some edition in the coq_makefile/_CoqProject section.

There are still two items I do not undertand fully (the last one about
-extra-phony, and the removal of external libraries at make clean time,
that I could not reproduce on a toy example.

1 files changed, 83 insertions, 53 deletions

diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index 4960542aac..a5e2883f55 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -79,72 +79,102 @@ See the man page of {\tt coqdep} for more details and options.
 \ttindex{coq\_Makefile}
 \ttindex{\_CoqProject}}
 
-\paragraph{\_CoqProject}
-When a proof development becomes a larger project, split into several
-files or containing {\ocaml} plugins, files share common options that
-must be specified to all the executables used during the development
-of the project. It is therefore convenient to write a file that could
-be read all the components (the IDE, the compiler, etc.) that
-specify all the files and the common options of the project.
-
-An attempt to set up a format to write project files has been made
-from the command line option of the {\Coq} makefile generator
-\texttt{coq\_makefile}. It is described by \texttt{\% coq\_makefile
-  --help}. The default name for the project file understood by
-\texttt{coq\_makefile}, \texttt{coqide} and \texttt{Proof General} is
-\texttt{\_CoqProject}.
-
-A minimal usable project file can probably be obtained by the
-invocation
+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{Makfile} 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 subdirectories. 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 subdirectory \texttt{MyFancyLib} of
+the \texttt{user-contrib} directory  (of the user's {\Coq} libraries
+location). This subdirectory 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.}
 
-While customizing a project file, mind the following requirements:
 \begin{itemize}
-\item {\Coq} files must end in \texttt{.v}, {\ocaml} modules in
-  \texttt{.ml4} if they require camlp preprocessing (and in
-  \texttt{.ml} otherwise), {\ocaml} module signatures, library
-  description and packing files respectively in \texttt{.mli},
-  \texttt{.mllib} and \texttt{.mlpack}.
-
-Any other argument that is not a valid option will be considered as a
-subdirectory. A specified subdirectory must have an inner
-\texttt{Makefile}. The phony targets \texttt{all} and \texttt{clean}
-will recursively call this target in all the subdirectories.
-
-\item \texttt{-R} and \texttt{-Q} options are for {\Coq}, \texttt{-I}
-  for {\ocaml}. The same directory may be ``included'' by both.
-
-  Using \texttt{-R} or \texttt{-Q} gives a correct logical path
-  and a correct installation location to your coq files.
-\item dependency on an external library must not be declared using a
-  \texttt{-Q \dots} in the \texttt{\_CoqProject} to include it in the
-  path, as the \textit{make clean} command would erase it! Instead,
-  install your dependency in a place automatically included by
-  {\Coq}. You can take advantage of the \texttt{COQPATH} variable
-  (see \ref{envars}) without installation if necessary.
-\item Use \texttt{-extra-phony} with no command to add an extra
+\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
+  subdirectory. Any subdirectory 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 subdirectory.
+
+\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:
+  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}
 
-\paragraph{Coq\_makefile}
-The writing of a generic and complete \texttt{Makefile} may be tedious
-work and that's why {\Coq} provides a tool to automate its creation
-from the \texttt{\_CoqProject} file, \texttt{coq\_makefile}.
-
-Use
-\begin{quotation}
-\texttt{coq\_makefile -f \_CoqProject -o Makefile}
-\end{quotation}
-to generate a \texttt{Makefile} the first time. \texttt{Makefile} will be
-automatically regenerated when \texttt{\_CoqProject} is updated afterward.
 
 \section[Documenting \Coq\ files with coqdoc]{Documenting \Coq\ files with coqdoc\label{coqdoc}
 \ttindex{coqdoc}}