diff options
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 59 | ||||
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 14 |
2 files changed, 45 insertions, 28 deletions
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index d1ce3bf41..ca240ff04 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. diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 556a2dab5..85deb3175 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -553,10 +553,11 @@ the form {\dirpath}{\tt .}{\textsl{ident}} and the file {\ident}{\tt mapped in {\Coq} loadpath to the logical path {\dirpath} (see Section~\ref{loadpath}). The mapping between physical directories and logical names at the time of requiring the file must be consistent -with the mapping used to compile the file. +with the mapping used to compile the file. If several files match, one of them +is picked in an unspecified fashion. \begin{Variants} -\item {\tt Require Import {\qualid}.} \comindex{Require} +\item {\tt Require Import {\qualid}.} \comindex{Require Import} This loads and declares the module {\qualid} and its dependencies then imports the contents of {\qualid} as described in @@ -585,6 +586,15 @@ with the mapping used to compile the file. given, it also imports {\qualid}$_1$, \ldots, {\qualid}$_n$ and all the recursive dependencies that were marked or transitively marked as {\tt Export}. + +\item {\tt From {\dirpath} Require {\qualid}.} + \comindex{From Require} + + This command acts as {\tt Require}, but picks any library whose absolute name + is of the form {\tt{\dirpath}.{\dirpath'}.{\qualid}} for some {\dirpath'}. + This is useful to ensure that the {\qualid} library comes from a given + package by expliciting its absolute root. + \end{Variants} \begin{ErrMsgs} |