diff -r 9362fcd0318c -r 892061142ba6 src/Doc/System/Misc.thy --- a/src/Doc/System/Misc.thy Fri May 17 17:45:51 2013 +0200 +++ b/src/Doc/System/Misc.thy Fri May 17 18:19:42 2013 +0200 @@ -236,89 +236,6 @@ using this template. *} -section {* Isabelle wrapper for make \label{sec:tool-make} *} - -text {* The old @{tool_def make} tool is a very simple wrapper for - ordinary Unix @{executable make}: -\begin{ttbox} -Usage: isabelle make [ARGS ...] - - Compile the logic in current directory using IsaMakefile. - ARGS are directly passed to the system make program. -\end{ttbox} - - Note that the Isabelle settings environment is also active. Thus one - may refer to its values within the @{verbatim IsaMakefile}, e.g.\ - @{verbatim "$(ISABELLE_HOME)"}. Furthermore, programs started from - the make file also inherit this environment. -*} - - -section {* Creating Isabelle session directories - \label{sec:tool-mkdir} *} - -text {* The old @{tool_def mkdir} tool prepares Isabelle session - source directories, including a sensible default setup of @{verbatim - IsaMakefile}, @{verbatim ROOT.ML}, and a @{verbatim document} - directory with a minimal @{verbatim root.tex} that is sufficient to - print all theories of the session (in the order of appearance); see - \secref{sec:tool-document} for further information on Isabelle - document preparation. The usage of @{tool mkdir} is: - -\begin{ttbox} -Usage: isabelle mkdir [OPTIONS] [LOGIC] NAME - - Options are: - -I FILE alternative IsaMakefile output - -P include parent logic target - -b setup build mode (session outputs heap image) - -q quiet mode - - Prepare session directory, including IsaMakefile and document source, - with parent LOGIC (default ISABELLE_LOGIC=\$ISABELLE_LOGIC) -\end{ttbox} - - The @{tool mkdir} tool is conservative in the sense that any - existing @{verbatim IsaMakefile} etc.\ is left unchanged. Thus it - is safe to invoke it multiple times, although later runs may not - have the desired effect. - - Note that @{tool mkdir} is unable to change @{verbatim IsaMakefile} - incrementally --- manual changes are required for multiple - sub-sessions. On order to get an initial working session, the only - editing needed is to add appropriate @{ML use_thy} calls to the - generated @{verbatim ROOT.ML} file. -*} - - -subsubsection {* Options *} - -text {* - The @{verbatim "-I"} option specifies an alternative to @{verbatim - IsaMakefile} for dependencies. Note that ``@{verbatim "-"}'' refers - to \emph{stdout}, i.e.\ ``@{verbatim "-I-"}'' provides an easy way - to peek at @{tool mkdir}'s idea of @{tool make} setup required for - some particular of Isabelle session. - - \medskip The @{verbatim "-P"} option includes a target for the - parent @{verbatim LOGIC} session in the generated @{verbatim - IsaMakefile}. The corresponding sources are assumed to be located - within the Isabelle distribution. - - \medskip The @{verbatim "-b"} option sets up the current directory - as the base for a new session that provides an actual logic image, - as opposed to one that only runs several theories based on an - existing image. Note that in the latter case, everything except - @{verbatim IsaMakefile} would be placed into a separate directory - @{verbatim NAME}, rather than the current one. See - \secref{sec:tool-usedir} for further information on \emph{build - mode} vs.\ \emph{example mode} of @{tool usedir}. - - \medskip The @{verbatim "-q"} option enables quiet mode, suppressing - further notes on how to proceed. -*} - - section {* Printing documents *} text {* @@ -358,180 +275,6 @@ *} -section {* Running Isabelle sessions \label{sec:tool-usedir} *} - -text {* The old @{tool_def usedir} tool builds object-logic images, or - runs example sessions based on existing logics. Its usage is: -\begin{ttbox} -Usage: isabelle usedir [OPTIONS] LOGIC NAME - - Options are: - -C BOOL copy existing document directory to -D PATH (default true) - -D PATH dump generated document sources into PATH - -M MAX multithreading: maximum number of worker threads (default 1) - -P PATH set path for remote theory browsing information - -Q INT set threshold for sub-proof parallelization (default 50) - -T LEVEL multithreading: trace level (default 0) - -V VARIANT declare alternative document VARIANT - -b build mode (output heap image, using current dir) - -d FORMAT build document as FORMAT (default false) - -f NAME use ML file NAME (default ROOT.ML) - -g BOOL generate session graph image for document (default false) - -i BOOL generate theory browser information (default false) - -m MODE add print mode for output - -p LEVEL set level of detail for proof objects (default 0) - -q LEVEL set level of parallel proof checking (default 1) - -r reset session path - -s NAME override session NAME - -t BOOL internal session timing (default false) - -v BOOL be verbose (default false) - - Build object-logic or run examples. Also creates browsing - information (HTML etc.) according to settings. - - ISABELLE_USEDIR_OPTIONS=... - - ML_PLATFORM=... - ML_HOME=... - ML_SYSTEM=... - ML_OPTIONS=... -\end{ttbox} - - Note that the value of the @{setting_ref ISABELLE_USEDIR_OPTIONS} - setting is implicitly prefixed to \emph{any} @{tool usedir} - call. Since the @{verbatim IsaMakefile}s of all object-logics - distributed with Isabelle just invoke @{tool usedir} for the real - work, one may control compilation options globally via above - variable. In particular, generation of \rmindex{HTML} browsing - information and document preparation is controlled here. -*} - - -subsubsection {* Options *} - -text {* - Basically, there are two different modes of operation: \emph{build - mode} (enabled through the @{verbatim "-b"} option) and - \emph{example mode} (default). - - Calling @{tool usedir} with @{verbatim "-b"} runs @{executable - "isabelle-process"} with input image @{verbatim LOGIC} and output to - @{verbatim NAME}, as provided on the command line. This will be a - batch session, running @{verbatim ROOT.ML} from the current - directory and then quitting. It is assumed that @{verbatim ROOT.ML} - contains all ML commands required to build the logic. - - In example mode, @{tool usedir} runs a read-only session of - @{verbatim LOGIC} and automatically runs @{verbatim ROOT.ML} from - within directory @{verbatim NAME}. It assumes that this file - contains appropriate ML commands to run the desired examples. - - \medskip The @{verbatim "-i"} option controls theory browser data - generation. It may be explicitly turned on or off --- as usual, the - last occurrence of @{verbatim "-i"} on the command line wins. - - The @{verbatim "-P"} option specifies a path (or actual URL) to be - prefixed to any \emph{non-local} reference of existing theories. - Thus user sessions may easily link to existing Isabelle libraries - already present on the WWW. - - The @{verbatim "-m"} options specifies additional print modes to be - activated temporarily while the session is processed. - - \medskip The @{verbatim "-d"} option controls document preparation. - Valid arguments are @{verbatim false} (do not prepare any document; - this is default), or any of @{verbatim dvi}, @{verbatim dvi.gz}, - @{verbatim ps}, @{verbatim ps.gz}, @{verbatim pdf}. The logic - session has to provide a properly setup @{verbatim document} - directory. See \secref{sec:tool-document} and - \secref{sec:tool-latex} for more details. - - \medskip The @{verbatim "-V"} option declares alternative document - variants, consisting of name/tags pairs (cf.\ options @{verbatim - "-n"} and @{verbatim "-t"} of @{tool_ref document}). The standard - document is equivalent to ``@{verbatim - "document=theory,proof,ML"}'', which means that all theory begin/end - commands, proof body texts, and ML code will be presented - faithfully. - - An alternative variant ``@{verbatim "outline=/proof/ML"}'' would - fold proof and ML parts, replacing the original text by a short - place-holder. The form ``@{text name}@{verbatim "=-"},'' means to - remove document @{text name} from the list of variants to be - processed. Any number of @{verbatim "-V"} options may be given; - later declarations have precedence over earlier ones. - - Some document variant @{text name} may use an alternative {\LaTeX} - entry point called @{verbatim "document/root_"}@{text - "name"}@{verbatim ".tex"} if that file exists; otherwise the common - @{verbatim "document/root.tex"} is used. - - \medskip The @{verbatim "-g"} option produces images of the theory - dependency graph (cf.\ \secref{sec:browse}) for inclusion in the - generated document, both as @{verbatim session_graph.eps} and - @{verbatim session_graph.pdf} at the same time. To include this in - the final {\LaTeX} document one could say @{verbatim - "\\includegraphics{session_graph}"} in @{verbatim - "document/root.tex"} (omitting the file-name extension enables - {\LaTeX} to select to correct version, either for the DVI or PDF - output path). - - \medskip The @{verbatim "-D"} option causes the generated document - sources to be dumped at location @{verbatim PATH}; this path is - relative to the session's main directory. If the @{verbatim "-C"} - option is true, this will include a copy of an existing @{verbatim - document} directory as provided by the user. For example, @{tool - usedir}~@{verbatim "-D generated HOL Foo"} produces a complete set - of document sources at @{verbatim "Foo/generated"}. Subsequent - invocation of @{tool document}~@{verbatim "Foo/generated"} (see also - \secref{sec:tool-document}) will process the final result - independently of an Isabelle job. This decoupled mode of operation - facilitates debugging of serious {\LaTeX} errors, for example. - - \medskip The @{verbatim "-p"} option determines the level of detail - for internal proof objects, see also the \emph{Isabelle Reference - Manual}~\cite{isabelle-ref}. - - \medskip The @{verbatim "-q"} option specifies the level of parallel - proof checking: @{verbatim 0} no proofs, @{verbatim 1} toplevel - proofs (default), @{verbatim 2} toplevel and nested Isar proofs. - The option @{verbatim "-Q"} specifies a threshold for @{verbatim - "-q2"}: nested proofs are only parallelized when the current number - of forked proofs falls below the given value (default 50), - multiplied by the number of worker threads (see option @{verbatim - "-M"}). - - \medskip The @{verbatim "-t"} option produces a more detailed - internal timing report of the session. - - \medskip The @{verbatim "-v"} option causes additional information - to be printed while running the session, notably the location of - prepared documents. - - \medskip The @{verbatim "-M"} option specifies the maximum number of - parallel worker threads used for processing independent tasks when - checking theory sources (multithreading only works on suitable ML - platforms). The special value of @{verbatim 0} or @{verbatim max} - refers to the number of actual CPU cores of the underlying machine, - which is a good starting point for optimal performance tuning. The - @{verbatim "-T"} option determines the level of detail in tracing - output concerning the internal locking and scheduling in - multithreaded operation. This may be helpful in isolating - performance bottle-necks, e.g.\ due to excessive wait states when - locking critical code sections. - - \medskip Any @{tool usedir} session is named by some \emph{session - identifier}. These accumulate, documenting the way sessions depend - on others. For example, consider @{verbatim "Pure/FOL/ex"}, which - refers to the examples of FOL, which in turn is built upon Pure. - - The current session's identifier is by default just the base name of - the @{verbatim LOGIC} argument (in build mode), or of the @{verbatim - NAME} argument (in example mode). This may be overridden explicitly - via the @{verbatim "-s"} option. -*} - - section {* Output the version identifier of the Isabelle distribution *} text {*