emacs local vars;
Mon, 24 Aug 1998 17:13:58 +0200
changeset 5366 8521cd8b0a40
parent 5365 f8bd38d9f8f3
child 5367 33f81e980c93
emacs local vars; isatool install;
--- 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}}
+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:
+Usage: install DIR
+  Install binaries in directory DIR with absolute references to
+  \$ISABELLE_HOME/bin (non-movable).
+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}:
+  isatool install /usr/local/bin
 \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
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "system"
+%%% End: