53 Usage: isatool findlogics |
53 Usage: isatool findlogics |
54 |
54 |
55 Collect heap file names from ISABELLE_PATH. |
55 Collect heap file names from ISABELLE_PATH. |
56 \end{ttbox} |
56 \end{ttbox} |
57 The base names of all files found on the path are printed --- sorted and with |
57 The base names of all files found on the path are printed --- sorted and with |
58 duplicates removed. Also note that \texttt{ISABELLE_PATH} implicitly depends |
58 duplicates removed. Also note that lookup in \texttt{ISABELLE_PATH} includes |
59 upon \texttt{ML_SYSTEM} and \texttt{ML_PLATFORM}. Thus switching to another |
59 the current values of \texttt{ML_SYSTEM} and \texttt{ML_PLATFORM}. Thus |
60 {\ML} compiler may change the set of logic images available. |
60 switching to another {\ML} compiler may change the set of logic images |
|
61 available. |
61 |
62 |
62 |
63 |
63 \section{Inspecting the settings environment -- \texttt{isatool getenv}} |
64 \section{Inspecting the settings environment -- \texttt{isatool getenv}} |
64 \label{sec:tool-getenv} |
65 \label{sec:tool-getenv} |
65 |
66 |
83 causes only the values to be printed. |
84 causes only the values to be printed. |
84 |
85 |
85 |
86 |
86 \subsection*{Examples} |
87 \subsection*{Examples} |
87 |
88 |
88 Get the {\ML} system identifier and the location where the compiler binaries |
89 Get the {\ML} system name and the location where the compiler binaries are |
89 are supposed to reside as follows: |
90 supposed to reside as follows: |
90 \begin{ttbox} |
91 \begin{ttbox} |
91 isatool getenv ML_SYSTEM ML_HOME |
92 isatool getenv ML_SYSTEM ML_HOME |
92 {\out ML_SYSTEM=smlnj-110} |
93 {\out ML_SYSTEM=polyml} |
93 {\out ML_HOME=/usr/local/smlnj-110/bin} |
94 {\out ML_HOME=/usr/share/polyml/x86-linux} |
94 \end{ttbox} |
95 \end{ttbox} |
95 |
96 |
96 The next one peeks at the search path that \texttt{isabelle} uses to locate |
97 The next one peeks at the output directory for \texttt{isabelle} logic images: |
97 logic images: |
98 \begin{ttbox} |
98 \begin{ttbox} |
99 isatool getenv -b ISABELLE_OUTPUT |
99 isatool getenv -b ISABELLE_PATH |
100 {\out /home/me/isabelle/heaps/polyml_x86-linux} |
100 {\out /home/me/isabelle/heaps/smlnj-110:/usr/local/isabelle/heaps/smlnj-110} |
|
101 \end{ttbox} |
101 \end{ttbox} |
102 Here we have used the \texttt{-b} option to suppress the |
102 Here we have used the \texttt{-b} option to suppress the |
103 \texttt{ISABELLE_PATH=} prefix. The value above is what became of the |
103 \texttt{ISABELLE_OUTPUT=} prefix. The value above is what became of the |
104 following assignment in the default settings file: |
104 following assignment in the default settings file: |
105 \begin{ttbox} |
105 \begin{ttbox} |
106 ISABELLE_PATH=\$ISABELLE_HOME_USER/heaps:\$ISABELLE_HOME/heaps |
106 ISABELLE_OUTPUT="\$ISABELLE_HOME_USER/heaps" |
107 \end{ttbox} |
107 \end{ttbox} |
108 Note how the \texttt{ML_SYSTEM} value got appended automatically to each path |
108 Note how the \texttt{ML_IDENTIFIER} value got appended automatically to each |
109 component. This is a special feature of \texttt{ISABELLE_PATH} (and also of |
109 path component. This is a special feature of \texttt{ISABELLE_OUTPUT}. |
110 \texttt{ISABELLE_OUTPUT}). |
|
111 |
110 |
112 |
111 |
113 \section{Installing standalone Isabelle executables -- \texttt{isatool install}} |
112 \section{Installing standalone Isabelle executables -- \texttt{isatool install}} |
114 \label{sec:tool-install} |
113 \label{sec:tool-install} |
115 |
114 |