From 9bd38c853461b5483fa208085548497ea8c211e5 Mon Sep 17 00:00:00 2001 From: pboutill Date: Mon, 19 Mar 2012 15:26:55 +0000 Subject: RefMan: Environment variables description update There is no mention in the refman of relative search of the lib from the binaries directory and of the use of _CoqProject by CoqIdE. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15052 85f007b7-540e-0410-9357-904b9bb8a0f7 --- doc/refman/RefMan-com.tex | 31 +++++++++++----------------- doc/refman/RefMan-uti.tex | 52 +++++++++++++++++++++++------------------------ 2 files changed, 38 insertions(+), 45 deletions(-) (limited to 'doc/refman') diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index c37e581ba..bcc68c78d 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -49,8 +49,9 @@ Notice that the \verb!-byte! and \verb!-opt! options are still available with \verb!coqc! and allow you to select the byte-code or native-code versions of the system. +\section[Customization]{Customization at launch time} -\section[Resource file]{Resource file\index{Resource file}} +\subsection{By resource file\index{Resource file}} When \Coq\ is launched, with either {\tt coqtop} or {\tt coqc}, the resource file \verb:$XDG_CONFIG_HOME/coq/coqrc.xxx: is loaded, where @@ -67,27 +68,19 @@ directories to the load path of \Coq. It is possible to skip the loading of the resource file with the option \verb:-q:. -\section[Environment variables]{Environment variables\label{EnvVariables} -\index{Environment variables}} - -There are four environment variables used by the \Coq\ system. -\verb:$COQBIN: for the directory where the binaries are, -\verb:$COQLIB: for the directory where the standard library is, -\verb:$COQPATH: for a list of directories separated by \verb|:| -(\verb|;| on windows) to add to the load path, and -\verb:$COQTOP: for the directory of the sources. The latter is useful -only for developers that are writing their own tactics and are using -\texttt{coq\_makefile} (see \ref{Makefile}). If \verb:$COQBIN: or -\verb:$COQLIB: are not defined, \Coq\ will use the default values -(defined at installation time). So these variables are useful only if -you move the \Coq\ binaries and library after installation. - -Coq will also honor \verb:$XDG_DATA_HOME: and \verb:$XDG_DATA_DIRS: (see +\section{By environment variables\label{EnvVariables} +\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). + +\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 +\Coq adds \verb:${XDG_DATA_HOME}/coq: and \verb:${XDG_DATA_DIRS}/coq: to its search path. -\section[Options]{Options\index{Options of the command line} +\subsection{By command line options\index{Options of the command line} \label{vmoption} \label{coqoptions}} diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index bda4cff9b..f51784456 100644 --- a/doc/refman/RefMan-uti.tex +++ b/doc/refman/RefMan-uti.tex @@ -78,47 +78,47 @@ See the man page of {\tt coqdep} for more details and options. \index{Makefile@{\tt Makefile}} \index{CoqMakefile@{\tt coq\_Makefile}}} -When a proof development becomes large and is split into several files, -it becomes crucial to use a tool like {\tt make} to compile \Coq\ -modules. +When a proof development becomes large, is split into several files or contains +Ocaml plugins, it becomes crucial to use a tool like {\tt make} to compile +\Coq\ modules. The writing of a generic and complete {\tt Makefile} may be a tedious work and that's why \Coq\ provides a tool to automate its creation, {\tt coq\_makefile}. -Arguments are explain by \texttt{\% coq\_makefile --help}. They can be directly -written in the command line but it is recommended to write them in a file (called -for example {\tt Make}) and then call {\tt coq\_makefile -f Make -o - Makefile}. That means options are in {\tt Make} file and output is {\tt - Makefile} This way, {\tt Makefile} will be automatically regenerated if -something changes in {\tt Make}. +You can get a description of the arguments by the command \texttt{\% coq\_makefile + --help}. Arguments can be directly written on the command line interface but it is recommended +to write them in a file ({\tt \_CoqProject} by default) and then call {\tt + coq\_makefile -f \_CoqProject -o Makefile}. That means options are read from {\tt + \_CoqProject} and written in {\tt Makefile}. This way, {\tt Makefile} will be +automagically regenerated when something changes in {\tt \_CoqProject}. The first time you use this tool, you may be happy with: \begin{quotation} \texttt{\% \{ echo '-R .} {\em MyFancyLib} \texttt{' ; find -name '*.v' -print \} > - Make \&\& coq\_makefile -f Make -o Makefile} + \_CoqProject \&\& coq\_makefile -f \_CoqProject -o Makefile} \end{quotation} -To customize things afterwards, remember: +To customize things further, remember the following: \begin{itemize} -\item Coq files must end in {\tt .v}, caml modules in {\tt .ml4} if they - require camlp preproccessing (and in {\tt .ml} otherwise), and caml module signatures in {\tt - .mli}. -\item If you give a directory directly as argument, it is because you provide a - Makefile for it in it. -\item {\tt -R} option is for Coq, {\tt -I} for caml. The same directory can +\item \Coq files must end in {\tt .v}, \ocaml modules in {\tt .ml4} if they + require camlp preproccessing (and in {\tt .ml} otherwise), and \ocaml module + signatures in {\tt .mli}. +\item Whenever a directory is passed as argument, any inner {\tt Makefile} will be + recursively called. +\item {\tt -R} option is for \Coq, {\tt -I} for \ocaml. The same directory can be ``included'' by both. - Using {\tt -R} option gives a right logical path and a correct installation + + Using {\tt -R} option gives a correct logical path and a correct installation emplacement to your coq files. -\item If your files depend on an external library that isn't install somewhere - looked by coqc, use {\tt OTHERFLAGS = '-R path/to/lib lib\_name'} option in your {\tt - Make} but don't do {\tt -R \dots} directly, the {\em make clean} command would - erase it! +\item If your files depend on an external library, never use {\tt -R \dots} to + include it in the path, the {\em make clean} command would erase it! Take + advantage of the \verb:COQPATH: variable (see \ref{envars}) instead if + necessary. \end{itemize} -\Warning To compile a project containing \ocaml{} files you must keep -the sources of \Coq{} somewhere and have an environment variable named -\texttt{COQTOP} that points to that directory. +Under normal circumstances, the only other variable that you may use is +\verb:$COQBIN: to specify the directory where the binaries are. \section[Documenting \Coq\ files with coqdoc]{Documenting \Coq\ files with coqdoc\label{coqdoc} \index{Coqdoc@{\sf coqdoc}}} @@ -142,7 +142,7 @@ after each phrase. Starting with a file {\em file}{\tt.tex} containing \Coq\ phrases, the {\tt coq-tex} filter produces a file named {\em file}{\tt.v.tex} with -the \Coq\ outcome. +the \Coq\ outcome. There are options to produce the \Coq\ parts in smaller font, italic, between horizontal rules, etc. -- cgit v1.2.3