From 81b43a0c8137dc890fe1eb462cf278c39cac3a5f Mon Sep 17 00:00:00 2001 From: Pierre Boutillier Date: Fri, 29 Aug 2014 18:17:54 +0200 Subject: Update RefMan with respect to new loadpath management --- doc/refman/RefMan-com.tex | 44 ++++++++++++---------- doc/refman/RefMan-ext.tex | 95 +++++++++++++++++++++++++++++++++-------------- doc/refman/RefMan-oth.tex | 51 +++++-------------------- 3 files changed, 102 insertions(+), 88 deletions(-) (limited to 'doc') 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 -- cgit v1.2.3