From 20de2185c8b9887d0ad83fc7c2bb82ab6bfe39d6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 1 Apr 2015 19:00:54 +0200
Subject: Documenting "From * Require *" and clearing a bit the loadpath
 chapter.

---
 doc/refman/RefMan-ext.tex | 59 ++++++++++++++++++++++++++---------------------
 1 file changed, 33 insertions(+), 26 deletions(-)

(limited to 'doc/refman/RefMan-ext.tex')

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index d1ce3bf41d..ca240ff04a 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1061,42 +1061,49 @@ 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
+\textrm{\textsl{path}} {\tt Lib}. All subfolders of {\textsl{path}} are
+recursively associated to the logical path {\tt Lib} extended with the
+corresponding suffix coming from the physical path. For instance, the
+folder {\tt path/fOO/Bar} maps to {\tt Lib.fOO.Bar}. 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
+Thanks to this mechanism, {\texttt{.vo}} files are made available through the
+logical name of the folder they are in, extended with their own basename. For
+example, the name associated to the file {\tt path/fOO/Bar/File.vo} is
+{\tt Lib.fOO.Bar.File}. The same caveat applies for invalid identifiers.
+
+Some folders have a special status and are automatically put in the path.
+{\Coq} commands 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
+with the same physical-to-logical translation and with an empty logical prefix.
+
+The command line option \texttt{-R} is a variant of \texttt{-Q} which has the
+strictly same behavior regarding loadpaths, but which also makes the
+corresponding \texttt{.vo} files available through their short names in a
+way not unlike the {\tt Import} command~(see {\ref{Import}}). For instance,
+\texttt{-R} \textrm{\textsl{path}} \texttt{Lib} associates to the file
+\texttt{path/fOO/Bar/File.vo} the logical name \texttt{Lib.fOO.Bar.File}, but
+allows this file to be accessed through the short names \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 {\ocaml} files. The {\ocaml} 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
-{\ocaml} loadpath.
+qualification is recommended. The {\tt From} argument of the {\tt Require}
+command can be used to bypass the implicit shortening by providing an absolute
+root to the required file.
+
+There also exists another independent loadpath mechanism attached to {\ocaml}
+object files (\texttt{.cmo} or \texttt{.cmxs}) rather than {\Coq} object files
+as described above. The {\ocaml} loadpath is managed using the option
+\texttt{-I path}. As in the {\ocaml} world, there is neither 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 {\ocaml} loadpath.
 
 See Section~\ref{coqoptions} for a more general view over the {\Coq}
 command line options.
-- 
cgit v1.2.3


From 81ce0dbd13a6d50b2a4e7617be3684db16b8b2f8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 1 Apr 2015 20:12:22 +0200
Subject: More clarifications on loadpaths.

---
 doc/refman/RefMan-ext.tex | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'doc/refman/RefMan-ext.tex')

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index ca240ff04a..85f191104e 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1059,7 +1059,7 @@ 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
+A logical prefix {\tt Lib} can associated to a physical path
 \textrm{\textsl{path}} using the command line option {\tt -Q}
 \textrm{\textsl{path}} {\tt Lib}. All subfolders of {\textsl{path}} are
 recursively associated to the logical path {\tt Lib} extended with the
@@ -1073,6 +1073,8 @@ Thanks to this mechanism, {\texttt{.vo}} files are made available through the
 logical name of the folder they are in, extended with their own basename. For
 example, the name associated to the file {\tt path/fOO/Bar/File.vo} is
 {\tt Lib.fOO.Bar.File}. The same caveat applies for invalid identifiers.
+When compiling a source file, the {\texttt{.vo}} file stores its logical name,
+so that an error is issued if it is loaded with the wrong loadpath afterwards.
 
 Some folders have a special status and are automatically put in the path.
 {\Coq} commands associate automatically a logical path to files
@@ -1086,7 +1088,7 @@ with the same physical-to-logical translation and with an empty logical prefix.
 The command line option \texttt{-R} is a variant of \texttt{-Q} which has the
 strictly same behavior regarding loadpaths, but which also makes the
 corresponding \texttt{.vo} files available through their short names in a
-way not unlike the {\tt Import} command~(see {\ref{Import}}). For instance,
+way not unlike the {\tt Import} command (see~{\ref{Import}}). For instance,
 \texttt{-R} \textrm{\textsl{path}} \texttt{Lib} associates to the file
 \texttt{path/fOO/Bar/File.vo} the logical name \texttt{Lib.fOO.Bar.File}, but
 allows this file to be accessed through the short names \texttt{fOO.Bar.File},
@@ -1095,7 +1097,7 @@ 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. The {\tt From} argument of the {\tt Require}
 command can be used to bypass the implicit shortening by providing an absolute
-root to the required file.
+root to the required file (see~\ref{Require}).
 
 There also exists another independent loadpath mechanism attached to {\ocaml}
 object files (\texttt{.cmo} or \texttt{.cmxs}) rather than {\Coq} object files
-- 
cgit v1.2.3


From 226bf474155092f41cbb0d3e47143ac221947342 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 1 Apr 2015 21:32:38 +0200
Subject: Fixing a few typos + some uniformization of writing in doc.

---
 doc/refman/RefMan-ext.tex | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'doc/refman/RefMan-ext.tex')

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 85f191104e..cc5239a779 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1059,7 +1059,7 @@ 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 prefix {\tt Lib} can associated to a physical path
+A logical prefix {\tt Lib} can be associated to a physical path
 \textrm{\textsl{path}} using the command line option {\tt -Q}
 \textrm{\textsl{path}} {\tt Lib}. All subfolders of {\textsl{path}} are
 recursively associated to the logical path {\tt Lib} extended with the
@@ -1102,8 +1102,8 @@ root to the required file (see~\ref{Require}).
 There also exists another independent loadpath mechanism attached to {\ocaml}
 object files (\texttt{.cmo} or \texttt{.cmxs}) rather than {\Coq} object files
 as described above. The {\ocaml} loadpath is managed using the option
-\texttt{-I path}. As in the {\ocaml} world, there is neither a notion of logical
-name prefix nor a way to access files in subdirectories of \texttt{path}.
+\texttt{-I path} (in the {\ocaml} world, there is neither 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 {\ocaml} loadpath.
 
-- 
cgit v1.2.3

