Update RefMan with respect to new loadpath management

3 files changed, 102 insertions, 88 deletions

diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 3feabb228..96b93a8c0 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -67,13 +67,15 @@ option \verb:-q:.
 \index{Environment variables}\label{envars}}
 
 Load path can be specified to the \Coq\ system by setting up
-\verb:$COQPATH: environment variable. It is a list of directories separated by \verb|:|
-(\verb|;| on windows).
+\verb:$COQPATH: environment variable. It is a list of directories
+separated by \verb|:| (\verb|;| on windows). {\Coq} will also honour
+\verb:$XDG_DATA_HOME: and \verb:$XDG_DATA_DIRS: (see section
+\ref{loadpath}).
 
-\Coq will also honour \verb:$XDG_DATA_HOME: and \verb:$XDG_DATA_DIRS: (see
-\url{http://standards.freedesktop.org/basedir-spec/basedir-spec-latest.html}).
-\Coq adds \verb:${XDG_DATA_HOME}/coq: and \verb:${XDG_DATA_DIRS}/coq: to its
-search path.
+Some {\Coq} commands call other {\Coq} commands. In this case, they
+look for the commands in directory specified by \verb:$COQBIN:. If
+this variable is not set, they look for the command in the executable
+path.
 
 \subsection{By command line options\index{Options of the command line}
 \label{vmoption}
@@ -83,26 +85,30 @@ The following command-line options are recognized by the commands {\tt
   coqc} and {\tt coqtop}, unless stated otherwise:
 
 \begin{description}
-\item[{\tt -I} {\em directory}, {\tt -include} {\em directory}[ {\tt -as} {\em dirpath}]]\ 
+\item[{\tt -I} {\em directory}, {\tt -include} {\em directory}]\
 
-Add physical path {\em directory} to the list of directories where to look for a
-file and bind it to the empty logical directory/the logical directory {\em
-  dirpath}. The sub-directory structure of {\em directory} is recursively available
-from {\Coq} using absolute names (extending the {\dirpath} prefix) (see
-Section~\ref{LongNames}).
+Add physical path {\em directory} to the Objective Caml loadpath.
 
-  \SeeAlso {\tt Add LoadPath} in Section~\ref{AddLoadPath} and logical
-  paths in Section~\ref{Libraries}.
+  \SeeAlso Section~\ref{Libraries} and the command {\tt Declare ML Module} Section \ref{compiled}.
+
+\item[\texttt{-Q} \emph{directory} {\dirpath}]\
+
+  Add physical path \emph{directory} to the list of directories where
+  {\Coq} looks for a file and bind it to the the logical directory
+  \emph{dirpath}. The sub-directory structure of \emph{directory} is
+  recursively available from {\Coq} using absolute names (extending
+  the {\dirpath} prefix) (see Section~\ref{LongNames}).
+  
+  \SeeAlso Section~\ref{Libraries}.
 
 \item[{\tt -R} {\em directory} {\dirpath}, {\tt -R} {\em directory} [{\tt -as} {\dirpath}]]\
 
-  Do as {\tt -I} {\em directory} {\tt -as} {\dirpath} but make the
-  sub-directory structure of {\em directory} recursively visible so
-  that the recursive contents of physical {\em directory} is available
+  Do as \texttt{-Q} \emph{directory} {\dirpath} but make the
+  sub-directory structure of \emph{directory} recursively visible so
+  that the recursive contents of physical \emph{directory} is available
   from {\Coq} using short or partially qualified names.
   
-  \SeeAlso {\tt Add Rec LoadPath} in Section~\ref{AddRecLoadPath} and logical
-  paths in Section~\ref{Libraries}.
+  \SeeAlso Section~\ref{Libraries}.
 
 \item[{\tt -top} {\dirpath}, {\tt -notop}]\ 
 
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index c4163b3b0..e594327fa 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -922,36 +922,25 @@ section is closed.
 
 \section{Libraries and qualified names}
 
-\subsection{Names of libraries and files
+\subsection{Names of libraries
 \label{Libraries}
-\index{Libraries}
-\index{Physical paths}
-\index{Logical paths}}
-
-\paragraph{Libraries}
+\index{Libraries}}
 
 The theories developed in {\Coq} are stored in {\em library files}
 which are hierarchically classified into {\em libraries} and {\em
-sublibraries}. To express this hierarchy, library names are
+  sublibraries}. To express this hierarchy, library names are
 represented by qualified identifiers {\qualid}, i.e. as list of
 identifiers separated by dots (see Section~\ref{qualid}). For
 instance, the library file {\tt Mult} of the standard {\Coq} library
-{\tt Arith} has name {\tt Coq.Arith.Mult}. The identifier
-that starts the name of a library is called a {\em library root}.
-All library files of the standard library of {\Coq} have reserved root
-{\tt Coq} but library file names based on other roots can be obtained
-by using {\tt coqc} options {\tt -I} or {\tt -R} (see
-Section~\ref{coqoptions}). Also, when an interactive {\Coq} session
-starts, a library of root {\tt Top} is started, unless option {\tt
--top} or {\tt -notop} is set (see Section~\ref{coqoptions}).
-
-As library files are stored on the file system of the underlying
-operating system, a translation from file-system names to {\Coq} names
-is needed. In this translation, names in the file system are called
-{\em physical} paths while {\Coq} names are contrastingly called {\em
-logical} names. Logical names are mapped to physical paths using the
-commands {\tt Add LoadPath} or {\tt Add Rec LoadPath} (see
-Sections~\ref{AddLoadPath} and~\ref{AddRecLoadPath}).
+{\tt Arith} is named {\tt Coq.Arith.Mult}. The identifier that starts
+the name of a library is called a {\em library root}.  All library
+files of the standard library of {\Coq} have the reserved root {\tt Coq}
+but library file names based on other roots can be obtained by using
+{\Coq} commands ({\tt coqc}, {\tt coqtop}, {\tt coqdep}, \dots) options
+{\tt -Q} or {\tt -R} (see Section~\ref{coqoptions}). Also, when an
+interactive {\Coq} session starts, a library of root {\tt Top} is
+started, unless option {\tt -top} or {\tt -notop} is set (see
+Section~\ref{coqoptions}).
 
 \subsection{Qualified names
 \label{LongNames}
@@ -998,11 +987,6 @@ partially qualified name is mapped to the absolute name in {\Coq} name
 table. Definitions flagged as {\tt Local} are only accessible with their
 fully qualified name (see \ref{Definition}).
 
-A similar table exists for library file names. It is updated by the
-vernacular commands {\tt Add LoadPath} and {\tt Add Rec LoadPath} (or
-their equivalent as options of the {\Coq} executables, {\tt -I} and
-{\tt -R}).
-
 It may happen that a visible name is hidden by the short name or a
 qualified name of another construction. In this case, the name that
 has been hidden must be referred to using one more level of
@@ -1024,6 +1008,61 @@ Locate nat.
 \SeeAlso Command {\tt Locate} in Section~\ref{Locate} and {\tt Locate
 Library} in Section~\ref{Locate Library}.
 
+\subsection{Libraries and filesystem\label{loadpath}\index{Loadpath}
+\index{Physical paths} \index{Logical paths}}
+
+Please note that the questions described here have been subject to
+redesign in Coq v8.5. Former versions of Coq use the same terminology
+to describe slightly different things.
+
+Compiled files (\texttt{.vo} and \texttt{.vi}) store sub-libraries. In
+order to refer to them inside {\Coq}, a translation from file-system
+names to {\Coq} names is needed. In this translation, names in the
+file system are called {\em physical} paths while {\Coq} names are
+contrastingly called {\em logical} names.
+
+A logical name {\tt Lib} can associated to a physical path
+\textrm{\textsl{path}} using the command line option {\tt -Q}
+\textrm{\textsl{path}} {\tt Lib}. This associates a logical name to
+all the compiled files in the directory tree rooted at
+\textrm{\textsl{path}}. The name associated to the file {\tt
+  path/fOO/Bar/File.vo} is {\tt Lib.fOO.Bar.File}. Subdirectories
+corresponding to invalid {\Coq} identifiers are skipped, and, by
+convention, subdirectories named {\tt CVS} or {\tt \_darcs} are
+skipped too.
+
+{\Coq} commands also associate automatically a logical path to files
+in the repository trees rooted at the directory from where the command
+is launched, \textit{coqlib}\texttt{/user-contrib/}, the directories
+listed in the \verb:$COQPATH:, \verb:${XDG_DATA_HOME}/coq/: and
+\verb:${XDG_DATA_DIRS}/coq/: environment variables (see
+\url{http://standards.freedesktop.org/basedir-spec/basedir-spec-latest.html})
+with the same $/ \to .$ convention but no prefix.
+
+The command line option \texttt{-R} is a variant of \texttt{-Q} that
+associates to a physical path the same logical path as \texttt{-Q}, as
+well as all suffixes of that logical path. The option \texttt{-R}
+\textrm{\textsl{path}} \texttt{Lib} associates to
+\texttt{path/fOO/Bar/File.vo} the logical names
+\texttt{Lib.fOO.Bar.File}, \texttt{fOO.Bar.File}, \texttt{Bar.File}
+and \texttt{File}. If several files with identical base name are
+present in different subdirectories of a recursive loadpath, which of
+these files is found first may be system-dependent and explicit
+qualification is recommended.
+
+There are currently two loadpaths in {\Coq}. There is one loadpath
+where seeking {\Coq} files (extensions \texttt{.v} or \texttt{.vo} or
+\texttt{.vi}) whose management has been explained just above, and one
+where seeking Objective Caml files. The Objective Caml loadpath is
+managed using the option \texttt{-I path}. As in {\ocaml} world, there
+is nether a notion of logical name prefix nor a way to access files in
+subdirectories of \texttt{path}. See the command \texttt{Declare ML
+  Module} in Section~\ref{compiled} to understand the need of the
+Objective Caml loadpath.
+
+See Section~\ref{coqoptions} for a more general view over the {\Coq}
+command line options.
+
 %% \paragraph{The special case of remarks and facts}
 %% 
 %% In contrast with definitions, lemmas, theorems, axioms and parameters,
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index ac0193b2f..0c7a534b7 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -708,12 +708,11 @@ This print the name of all \ocaml{} modules loaded with \texttt{Declare
   ML Module}. To know from where these module were loaded, the user
 should use the command \texttt{Locate File} (see Section~\ref{Locate File})
 
-\section[Loadpath]{Loadpath\label{loadpath}\index{Loadpath}}
+\section[Loadpath]{Loadpath}
 
-There are currently two loadpaths in \Coq. A loadpath where seeking
-{\Coq} files (extensions {\tt .v} or {\tt .vo} or {\tt .vi}) and one where
-seeking Objective Caml files. The default loadpath contains the
-directory ``\texttt{.}'' denoting the current directory and mapped to the empty logical path (see Section~\ref{LongNames}).
+Loadpaths are preferably managed using {\Coq} command line options
+(see Section~\ref{loadpath}) but there remains vernacular commands to
+manage them.
 
 \subsection[\tt Pwd.]{\tt Pwd.\comindex{Pwd}\label{Pwd}}
 This command displays the current working directory.
@@ -729,15 +728,9 @@ 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 adds the physical directory {\str} to the current {\Coq}
-loadpath and maps it to the logical directory {\dirpath}, which means
-that every file \textrm{\textsl{dirname}}/\textrm{\textsl{basename.v}}
-physically lying in subdirectory {\str}/\textrm{\textsl{dirname}}
-becomes accessible in {\Coq} through absolute logical name
-{\dirpath}{\tt .}\textrm{\textsl{dirname}}{\tt
-.}\textrm{\textsl{basename}}.
-
-\Rem {\tt Add LoadPath} also adds {\str} to the current ML loadpath.
+This command is equivament to the command line option {\tt -Q {\dirpath}
+  {\str}}. It adds the physical directory {\str} to the current {\Coq}
+loadpath and maps it to the logical directory {\dirpath}.
 
 \begin{Variants}
 \item {\tt Add LoadPath {\str}.}\\
@@ -745,29 +738,9 @@ 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 adds the physical directory {\str} and all its subdirectories to
-the current \Coq\ loadpath. The top directory {\str} is mapped to the
-logical directory {\dirpath} and any subdirectory {\textsl{pdir}} of it is
-mapped to logical name {\dirpath}{\tt .}\textsl{pdir} and
-recursively. Subdirectories corresponding to invalid {\Coq}
-identifiers are skipped, and, by convention, subdirectories named {\tt
-CVS} or {\tt \_darcs} are skipped too.
-
-Otherwise, said, {\tt Add Rec LoadPath {\str} as {\dirpath}} behaves
-as {\tt Add LoadPath {\str} as {\dirpath}} excepts that files lying in
-validly named subdirectories of {\str} need not be qualified to be
-found.
-
-In case of files with identical base name, files lying in most recently
-declared {\dirpath} are found first and explicit qualification is
-required to refer to the other files of same base name.
-
-If several files with identical base name are present in different
-subdirectories of a recursive loadpath declared via a single instance of
-{\tt Add Rec LoadPath}, which of these files is found first is
-system-dependent and explicit qualification is recommended.
-
-\Rem {\tt Add Rec LoadPath} also recursively adds {\str} to the current ML loadpath.
+This command is equivalent to the command line option {\tt -R {\dirpath}
+  {\str}}. It adds the physical directory {\str} and all its
+subdirectories to the current {\Coq} loadpath.
 
 \begin{Variants}
 \item {\tt Add Rec LoadPath {\str}.}\\
@@ -789,15 +762,11 @@ Works as {\tt Print LoadPath} but displays only the paths that extend the {\dirp
 This command adds the path {\str} to the current Objective Caml loadpath (see
 the command {\tt Declare ML Module} in the Section~\ref{compiled}).
 
-\Rem This command is implied by {\tt Add LoadPath {\str} as {\dirpath}}.
-
 \subsection[\tt Add Rec ML Path {\str}.]{\tt Add Rec ML Path {\str}.\comindex{Add Rec ML Path}}
 This command adds the directory {\str} and all its subdirectories 
 to the current Objective Caml loadpath (see
 the command {\tt Declare ML Module} in the Section~\ref{compiled}).
 
-\Rem This command is implied by {\tt Add Rec LoadPath {\str} as {\dirpath}}.
-
 \subsection[\tt Print ML Path {\str}.]{\tt Print ML Path {\str}.\comindex{Print ML Path}}
 This command displays the current Objective Caml loadpath.
 This command makes sense only under the bytecode version of {\tt