# HG changeset patch # User wenzelm # Date 903971638 -7200 # Node ID 8521cd8b0a407b64ae4c21ba231246d355ffaac1 # Parent f8bd38d9f8f32856ff488781b6bbb56beebec2c6 emacs local vars; isatool install; diff -r f8bd38d9f8f3 -r 8521cd8b0a40 doc-src/System/misc.tex --- a/doc-src/System/misc.tex Mon Aug 24 17:13:26 1998 +0200 +++ b/doc-src/System/misc.tex Mon Aug 24 17:13:58 1998 +0200 @@ -46,7 +46,7 @@ of the files are renamed to have the suffix~\verb'~~'. -\section{Get logic images --- \texttt{isatool findlogics}} +\section{Getting logic images --- \texttt{isatool findlogics}} The \tooldx{findlogics} utility traverses all directories specified in \texttt{ISABELLE_PATH}, looking for Isabelle logic images. Its usage @@ -113,6 +113,35 @@ \texttt{ISABELLE_PATH} (and also of \texttt{ISABELLE_OUTPUT}). +\section{Installing Isabelle binaries with absolute references -- \texttt{isatool install}} +\label{sec:tool-install} + +Usually, the Isabelle binaries (\texttt{isabelle}, \texttt{isatool} +etc.) are just run from their location within the distribution +directory, probably indirectly by the shell through its \texttt{PATH}. +In some cases, though, another more traditional installation scheme +might be preferably where executables are put into some global system +directory (like \texttt{/usr/local/bin}). + +Doing a plain copy of the Isabelle executables just would not work, +though. One should use the \tooldx{install} utility instead: +\begin{ttbox} +Usage: install DIR + + Install binaries in directory DIR with absolute references to + \$ISABELLE_HOME/bin (non-movable). +\end{ttbox} + +The generated executables contain absolute references to +\texttt{ISABELLE_HOME}, as figured out by the \texttt{isatool} +invocation. While the scripts themselves may be relocated afterwards, +they would cease working if the referenced Isabelle distribution is +moved. This is an example use of \texttt{install}: +\begin{ttbox} + isatool install /usr/local/bin +\end{ttbox} + + \section{Isabelle's version of make --- \texttt{isatool make}} The Isabelle \tooldx{make} utility is a very simple wrapper for @@ -225,3 +254,8 @@ object-logics as a model for your own developements. For example, see \texttt{src/FOL/IsaMakefile}. + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "system" +%%% End: