doc-src/System/misc.tex
 changeset 3262 7115da553895 parent 3217 d30d62128fe5 child 3278 636322bfd057
equal inserted replaced
3261:8fe63a9cd0c7 3262:7115da553895
    29 \section{Tuning proof scripts --- \texttt{isatool expandshort}}
    29 \section{Tuning proof scripts --- \texttt{isatool expandshort}}
    30
    30
    31 The \tooldx{expandshort} utility tunes {\ML} proof scripts to enhance
    31 The \tooldx{expandshort} utility tunes {\ML} proof scripts to enhance
    32 readability a bit:
    32 readability a bit:
    33 \begin{ttbox}
    33 \begin{ttbox}
    34 Usage: expandshort [FILES ...]
    34 Usage: isatool expandshort [FILES ...]
    35
    35
    36   Expand shorthand goal commands in FILES.  Also contracts uses of
    36   Expand shorthand goal commands in FILES.  Also contracts uses of
    37   resolve_tac, dresolve_tac, eresolve_tac, rewrite_goals_tac on
    37   resolve_tac, dresolve_tac, eresolve_tac, rewrite_goals_tac on
    38   1-element lists; furthermore expands tabs, since they are now
    38   1-element lists; furthermore expands tabs, since they are now
    39   forbidden in ML string constants.
    39   forbidden in ML string constants.
    56
    56
    57   Collect heap file names from ISABELLE_PATH.
    57   Collect heap file names from ISABELLE_PATH.
    58 \end{ttbox}
    58 \end{ttbox}
    59 The base names of all files found on the path are printed --- sorted
    59 The base names of all files found on the path are printed --- sorted
    60 and with duplicates removed. Also note that \texttt{ISABELLE_PATH}
    60 and with duplicates removed. Also note that \texttt{ISABELLE_PATH}
    61 implicitely depends upon \texttt{ML_SYSTEM}. Thus switching to another
    61 implicitly depends upon \texttt{ML_SYSTEM}. Thus switching to another
    62 {\ML} compiler may change the set of logic images available.
    62 {\ML} compiler may change the set of logic images available.
    63
    63
    64
    64
    65 \section{Inspecting the settings environment -- \texttt{isatool getenv}}
    65 \section{Inspecting the settings environment -- \texttt{isatool getenv}}
    66 \label{sec:tool-getenv}
    66 \label{sec:tool-getenv}
   122
   122
   123   Compiles logic in current directory using IsaMakefile.
   123   Compiles logic in current directory using IsaMakefile.
   124   ARGS are directly passed to the system make program.
   124   ARGS are directly passed to the system make program.
   125 \end{ttbox}
   125 \end{ttbox}
   126 Note that the Isabelle settings environment is also active. Thus one
   126 Note that the Isabelle settings environment is also active. Thus one
   127 may refer to its values within the \texttt{IsaMakefile}, e.g.\
   127 may refer to its values within the \ttindex{IsaMakefile}, e.g.\
   128 \texttt{\$(ISABELLE_OUTPUT)}. Furthermore, programs started from the  128 \texttt{\$(ISABELLE_OUTPUT)}. Furthermore, programs started from the
   129 make file also inherit this environment.
   129 make file also inherit this environment.
   130
   130
   131 \medskip You may want to have a look at the \texttt{IsaMakefile}s of
   131 Typically, \texttt{IsaMakefile}s defer the real work to the
   132 the distributed object-logics as examples for your own developements.
   132 \texttt{usedir} utility, see \S\ref{sec:tool-usedir}.

   133
   133
   134
   134
   135
   135 \section{Running complete logics --- \texttt{isatool usedir}} \label{sec:tool-usedir}
   136 \section{Running complete logics --- \texttt{isatool usedir}} \label{sec:tool-usedir}
   136
   137
   137 FIXME
   138 The \tooldx{usedir} utility builds object-logic images, or runs
   138
   139 example sessions based on existing logics. Its usage is:
   139 %FIXME
   140 %FIXME
   140 %    -g BOOL      generate theory graph data (default false)
   141 %    -g BOOL      generate theory graph data (default false)
   141 \begin{ttbox}
   142 \begin{ttbox}
   142 Usage: isatool usedir LOGIC NAME
   143 Usage: isatool usedir LOGIC NAME
   143
   144
   148
   149
   149   Build object-logic or run examples. Also creates browsing
   150   Build object-logic or run examples. Also creates browsing
   150   information (HTML etc.) according to settings.
   151   information (HTML etc.) according to settings.
   151 \end{ttbox}
   152 \end{ttbox}
   152
   153
   153 FIXME
   154 The value of the \settdx{ISABELLE_USEDIR_OPTIONS} setting is

   155 implicitely prefixed to \emph{any} \texttt{usedir} call. Since the

   156 \ttindex{IsaMakefile}s of all object-logics distributed with Isabelle

   157 just invoke \texttt{usedir} for the real work, one may control

   158 compilation options globally via above variable. In particular,

   159 generation of \rmindex{HTML} browsing information is enabled or

   160 disabled this way.

   161

   162

   163 \subsection*{Options}

   164

   165 There are two slightly different modes of operation: \emph{build} mode

   166 (enabled through the \texttt{-b} option) and \emph{example} mode.

   167

   168 Calling \texttt{usedir} with \texttt{-b} runs \texttt{isabelle} with

   169 input image \texttt{LOGIC} and output to \texttt{NAME}, as provided as

   170 arguments. This will be a batch session, executing just

   171 \texttt{use_dir".";}\index{*use_dir}, and then quitting. It is assumed

   172 that there is a file \texttt{ROOT.ML} in the current directory

   173 containing all {\ML} commands required to build the logic.

   174

   175 In example mode, on the other hand, \texttt{usedir} runs a read-only

   176 session of \texttt{LOGIC} (typically just built before) and does an

   177 automatic \texttt{use_dir"NAME";}. I.e.\ it assumes that some file

   178 \texttt{ROOT.ML} in directory \texttt{NAME} contains appropriate {\ML}

   179 commands to run the desired examples.

   180

   181 \medskip The \texttt{-h} option controls HTML browsing data

   182 generation. It may be explicitely turned on or off --- the last

   183 occurrence of some \texttt{-h} on the command line wins.

   184

   185 \medskip Any \texttt{usedir} session is named by some \emph{session

   186   identifier}. These may accumulate, documenting the way sessions

   187 depend on others. For example, consider \texttt{Pure/FOL/ZF/ex}, which

   188 refers the examples of {\ZF} set theory, built upon {\FOL}, built upon

   189 {\Pure}.

   190

   191 The current session's identifier is by default just the base name of

   192 the \texttt{LOGIC} argument (in build mode), or the \texttt{NAME}

   193 argument (in example mode). This may be overridden explicitely via the

   194 \texttt{-s} option.

   195

   196

   197 \subsection*{Examples}

   198

   199 Refer to the \texttt{IsaMakefile}s of the Isabelle distribution's

   200 object-logics as a model for your own developements.