# HG changeset patch # User wenzelm # Date 1368807582 -7200 # Node ID 892061142ba601ac6478c6f7d3bb247d11b3e933 # Parent 9362fcd0318c664361a33ca058017d04770df230 discontinued obsolete isabelle usedir, mkdir, make; diff -r 9362fcd0318c -r 892061142ba6 NEWS --- a/NEWS Fri May 17 17:45:51 2013 +0200 +++ b/NEWS Fri May 17 18:19:42 2013 +0200 @@ -232,9 +232,8 @@ *** System *** -* Discontinued "isabelle usedir" option -P (remote path) and -r (reset -session path). Note that usedir is legacy and superseded by "isabelle -build" since Isabelle2013. +* Discontinued obsolete isabelle usedir, mkdir, make -- superseded by +"isabelle build" in Isabelle2013. INCOMPATIBILITY. diff -r 9362fcd0318c -r 892061142ba6 etc/settings --- a/etc/settings Fri May 17 17:45:51 2013 +0200 +++ b/etc/settings Fri May 17 18:19:42 2013 +0200 @@ -24,13 +24,9 @@ ### -### Batch sessions +### Batch sessions (cf. isabelle build) ### -#cf. isabelle usedir -ISABELLE_USEDIR_OPTIONS="-M max -p 1 -q 2 -v true -V outline=/proof,/ML" - -#cf. isabelle build ISABELLE_BUILD_OPTIONS="" ISABELLE_BUILD_JAVA_OPTIONS="-Xmx1024m -Xss1m" diff -r 9362fcd0318c -r 892061142ba6 lib/Tools/make --- a/lib/Tools/make Fri May 17 17:45:51 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,26 +0,0 @@ -#!/usr/bin/env bash -# -# Author: Markus Wenzel, TU Muenchen -# -# DESCRIPTION: Isabelle make utility - - -PRG="$(basename "$0")" - -function usage() -{ - echo - echo "Usage: isabelle $PRG [ARGS ...]" - echo - echo " Compile the logic in current directory using IsaMakefile." - echo " ARGS are directly passed to the system make program." - echo - exit 1 -} - - -## main - -[ "$1" = "-?" ] && usage - -exec make -f IsaMakefile "$@" diff -r 9362fcd0318c -r 892061142ba6 lib/Tools/mkdir --- a/lib/Tools/mkdir Fri May 17 17:45:51 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,288 +0,0 @@ -#!/usr/bin/env bash -# -# Author: Markus Wenzel, TU Muenchen -# -# DESCRIPTION: prepare logic session directory - - -## diagnostics - -PRG="$(basename "$0")" - -function usage() -{ - echo - echo "Usage: isabelle $PRG [OPTIONS] [LOGIC] NAME" - echo - echo " Options are:" - echo " -I FILE alternative IsaMakefile output" - echo " -P include parent logic target" - echo " -b setup build mode (session outputs heap image)" - echo " -q quiet mode" - echo - echo " Prepare session directory, including IsaMakefile and document source" - echo " with parent LOGIC (default ISABELLE_LOGIC=$ISABELLE_LOGIC)" - echo - exit 1 -} - -function fail() -{ - echo "$1" >&2 - exit 2 -} - - -## process command line - -# options - -ISAMAKEFILE="IsaMakefile" -PARENT="" -BUILD="" -QUIET="" - -while getopts "I:Pbq" OPT -do - case "$OPT" in - I) - ISAMAKEFILE="$OPTARG" - ;; - P) - PARENT=true - ;; - b) - BUILD=true - ;; - q) - QUIET=true - ;; - \?) - usage - ;; - esac -done - -shift $(($OPTIND - 1)) - - -# args - - -if [ "$#" -eq 1 ]; then - LOGIC="$ISABELLE_LOGIC" - DIR_NAME="$1"; shift -elif [ "$#" -eq 2 ]; then - LOGIC="$1"; shift - DIR_NAME="$1"; shift -else - usage -fi - -DIR=$(dirname "$DIR_NAME") -NAME=$(basename "$DIR_NAME") - - -## main - -[ -z "$QUIET" ] && echo "Preparing session \"$NAME\" ..." - - -# IsaMakefile - -mkdir -p "$DIR" || fail "Bad directory: $DIR" -cd "$DIR" - -DOCUMENT_ROOT="" -VERBOSE="" -[ -z "$QUIET" ] && VERBOSE="-v true " - -if [ -n "$BUILD" ]; then - IMAGES="$NAME" - TEST="" - TARGET="\$(OUT)/$NAME" - ROOT_ML="ROOT.ML" - SOURCES="*.thy" - DOCUMENT_ROOT="document/root.tex" - USEDIR="\$(USEDIR) -b -P http://isabelle.in.tum.de/library" -else - IMAGES="" - TEST="$NAME" - TARGET="\$(LOG)/$LOGIC-$NAME.gz" - ROOT_ML="$NAME/ROOT.ML" - SOURCES="$NAME/*.thy" - DOCUMENT_ROOT="$NAME/document/root.tex" - USEDIR="\$(USEDIR)" -fi - -if [ "$ISAMAKEFILE" != - -a -f "$ISAMAKEFILE" ]; then - echo "keeping $DIR/$ISAMAKEFILE" >&2 -else - [ -z "$QUIET" -a -n "$ISAMAKEFILE" -a "$ISAMAKEFILE" != - ] && \ - echo "creating $DIR/$ISAMAKEFILE" >&2 - { echo - echo "## targets" - echo - echo "default: $NAME" - echo "images: $IMAGES" - echo "test: $TEST" - echo - echo "all: images test" - echo - echo - echo "## global settings" - echo - echo "SRC = \$(ISABELLE_HOME)/src" - echo "OUT = \$(ISABELLE_OUTPUT)" - echo "LOG = \$(OUT)/log" - echo - echo "USEDIR = \$(ISABELLE_TOOL) usedir ${VERBOSE}-i true -d $ISABELLE_DOC_FORMAT ## -D generated" - echo - echo - echo "## $NAME" - echo "" - if [ -n "$PARENT" ]; then - echo "$NAME: $LOGIC $TARGET" - echo - echo "$LOGIC:" - echo -e "\t@cd \$(SRC)/$LOGIC; \$(ISABELLE_TOOL) make $LOGIC" - echo - echo "$TARGET: \$(OUT)/$LOGIC $ROOT_ML $DOCUMENT_ROOT ## $SOURCES" - echo -e "\t@$USEDIR \$(OUT)/$LOGIC $NAME" - else - echo "$NAME: $TARGET" - echo - echo "$TARGET: ## $ROOT_ML $DOCUMENT_ROOT $SOURCES" - echo -e "\t@$USEDIR $LOGIC $NAME" - fi - echo - echo - echo "## clean" - echo - echo "clean:" - echo -e "\t@rm -f $TARGET" - } | { - if [ -z "$ISAMAKEFILE" -o "$ISAMAKEFILE" = - ]; then - cat - else - cat > "$ISAMAKEFILE" - fi - } -fi - - -# base directory - -if [ -z "$BUILD" ]; then - mkdir -p "$NAME" || fail "Bad directory: $DIR/$NAME" - cd "$NAME" - PREFIX="$DIR/$NAME" -else - PREFIX="$DIR" -fi - -if [ -f ROOT.ML ]; then - echo "keeping $PREFIX/ROOT.ML" >&2 -else - [ -z "$QUIET" ] && echo "creating $PREFIX/ROOT.ML" >&2 - cat >ROOT.ML <&2 -else - [ -z "$QUIET" ] && echo "creating $PREFIX/document" >&2 - mkdir document || fail "Bad directory: $PREFIX/document" - - [ -z "$QUIET" ] && echo "creating $PREFIX/document/root.tex" >&2 - TITLE=$(echo "$NAME" | tr _ - | tr -d '\\') - AUTHOR=$(echo "By $USER" | tr _ - | tr -d '\\') - cat >document/root.tex <, \, \, \, \, \, - %\, \, \, \, \, - %\, \, \ - -%\usepackage{eurosym} - %for \ - -%\usepackage[only,bigsqcap]{stmaryrd} - %for \ - -%\usepackage{eufrak} - %for \ ... \, \ ... \ (also included in amssymb) - -%\usepackage{textcomp} - %for \, \, \, \, \, - %\ - -% this should be the last package used -\usepackage{pdfsetup} - -% urls in roman style, theory text in math-similar italics -\urlstyle{rm} -\isabellestyle{it} - -% for uniform font size -%\renewcommand{\isastyle}{\isastyleminor} - - -\begin{document} - -\title{$TITLE} -\author{$AUTHOR} -\maketitle - -\tableofcontents - -% sane default for proof documents -\parindent 0pt\parskip 0.5ex - -% generated text of all theories -\input{session} - -% optional bibliography -%\bibliographystyle{abbrv} -%\bibliography{root} - -\end{document} - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: t -%%% End: -EOF -fi - - -# notes - -if [ -z "$QUIET" ]; then - cat >&2 <&2 - exit 2 -} - -function check_bool() -{ - [ "$1" = true -o "$1" = false ] || fail "Bad boolean: \"$1\"" -} - -function check_number() -{ - [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\"" -} - - -## process command line - -# options - -COPY_DUMP=true -DUMP="" -MAXTHREADS="1" -RPATH="" -TRACETHREADS="0" -DOCUMENT_VARIANTS="" -BUILD="" -DOCUMENT=false -ROOT_FILE="ROOT.ML" -DOCUMENT_GRAPH=false -INFO=false -MODES="" -RESET=false -SESSION="" -PROOFS="0" -PARALLEL_PROOFS="1" -PARALLEL_PROOFS_THRESHOLD="100" -TIMING=false -VERBOSE=false - -function getoptions() -{ - OPTIND=1 - while getopts "C:D:M:P:Q:T:V:bd:f:g:i:m:p:q:rs:t:v:" OPT - do - case "$OPT" in - C) - check_bool "$OPTARG" - COPY_DUMP="$OPTARG" - ;; - D) - DUMP="$OPTARG" - ;; - M) - if [ "$OPTARG" = max ]; then - MAXTHREADS=0 - else - check_number "$OPTARG" - MAXTHREADS="$OPTARG" - fi - ;; - P) - RPATH="$OPTARG" - ;; - Q) - check_number "$OPTARG" - PARALLEL_PROOFS_THRESHOLD="$OPTARG" - ;; - T) - check_number "$OPTARG" - TRACETHREADS="$OPTARG" - ;; - V) - if [ -z "$DOCUMENT_VARIANTS" ]; then - DOCUMENT_VARIANTS="\"$OPTARG\"" - else - DOCUMENT_VARIANTS="$DOCUMENT_VARIANTS, \"$OPTARG\"" - fi - ;; - b) - BUILD=true - ;; - d) - DOCUMENT="$OPTARG" - ;; - f) - ROOT_FILE="$OPTARG" - ;; - g) - check_bool "$OPTARG" - DOCUMENT_GRAPH="$OPTARG" - ;; - i) - check_bool "$OPTARG" - INFO="$OPTARG" - ;; - m) - if [ -z "$MODES" ]; then - MODES="\"$OPTARG\"" - else - MODES="\"$OPTARG\", $MODES" - fi - ;; - p) - check_number "$OPTARG" - PROOFS="$OPTARG" - ;; - q) - check_number "$OPTARG" - PARALLEL_PROOFS="$OPTARG" - ;; - r) - RESET=true - ;; - s) - SESSION="$OPTARG" - ;; - t) - check_bool "$OPTARG" - TIMING="$OPTARG" - ;; - v) - check_bool "$OPTARG" - VERBOSE="$OPTARG" - ;; - \?) - usage - ;; - esac - done -} - -eval "OPTIONS=($ISABELLE_USEDIR_OPTIONS)" -getoptions "${OPTIONS[@]}" - -getoptions "$@" -shift $(($OPTIND - 1)) - - -# args - -[ "$#" -ne 2 ] && usage - -LOGIC="$1"; shift -NAME="$1"; shift - -[ -z "$SESSION" ] && SESSION=$(basename "$NAME") - - - -## main - -# prepare browser info dir - -if [ "$INFO" = "true" -a ! -f "$ISABELLE_BROWSER_INFO/index.html" ]; then - mkdir -p "$ISABELLE_BROWSER_INFO" - cp "$ISABELLE_HOME/lib/logo/isabelle.gif" "$ISABELLE_BROWSER_INFO/isabelle.gif" - cat "$ISABELLE_HOME/lib/html/library_index_header.template" \ - "$ISABELLE_HOME/lib/html/library_index_content.template" \ - "$ISABELLE_HOME/lib/html/library_index_footer.template"> "$ISABELLE_BROWSER_INFO/index.html" -fi - - -# prepare log dir - -LOGDIR="$ISABELLE_OUTPUT/log" -mkdir -p "$LOGDIR" - - -# run isabelle - -PARENT=$(basename "$LOGIC") - -if [ -z "$BUILD" ]; then - cd "$NAME" || fail "Bad session directory '$NAME'" -fi - -if [ "$DOCUMENT" != false ]; then - DOC="$DOCUMENT" -else - DOC="" -fi - - -. "$ISABELLE_HOME/lib/scripts/timestart.bash" - -if [ -n "$BUILD" ]; then - ITEM="$SESSION" - echo "Building $ITEM ..." >&2 - LOG="$LOGDIR/$ITEM" - - "$ISABELLE_PROCESS" \ - -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$ISABELLE_BROWSER_INFO\" \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD;" \ - -q -w $LOGIC $NAME > "$LOG" - RC="$?" -else - ITEM=$(basename "$LOGIC")-"$SESSION" - echo "Running $ITEM ..." >&2 - LOG="$LOGDIR/$ITEM" - - "$ISABELLE_PROCESS" \ - -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$ISABELLE_BROWSER_INFO\" \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD; quit();" \ - -r -q "$LOGIC" > "$LOG" - RC="$?" - cd .. -fi - -. "$ISABELLE_HOME/lib/scripts/timestop.bash" - - -# exit status - -if [ "$RC" -eq 0 ]; then - echo "Finished $ITEM ($TIMES_REPORT)" >&2 - gzip --force "$LOG" -else - { echo "$ITEM FAILED"; - echo "(see also $LOG)"; - echo; tail -20 "$LOG"; echo; } >&2 -fi - -exit "$RC" diff -r 9362fcd0318c -r 892061142ba6 src/Doc/System/Basics.thy --- a/src/Doc/System/Basics.thy Fri May 17 17:45:51 2013 +0200 +++ b/src/Doc/System/Basics.thy Fri May 17 18:19:42 2013 +0200 @@ -256,12 +256,6 @@ \item[@{setting_def ISABELLE_LINE_EDITOR}] specifies the default line editor for the @{tool_ref tty} interface. - \item[@{setting_def ISABELLE_USEDIR_OPTIONS}] is implicitly prefixed - to the command line of any @{tool_ref usedir} invocation. This - typically contains compilation options for object-logics --- @{tool - usedir} is the basic tool for managing logic sessions (cf.\ the - @{verbatim IsaMakefile}s in the distribution). - \item[@{setting_def ISABELLE_LATEX}, @{setting_def ISABELLE_PDFLATEX}, @{setting_def ISABELLE_BIBTEX}, @{setting_def ISABELLE_DVIPS}] refer to {\LaTeX} related tools for Isabelle 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 {* diff -r 9362fcd0318c -r 892061142ba6 src/Pure/System/session.ML --- a/src/Pure/System/session.ML Fri May 17 17:45:51 2013 +0200 +++ b/src/Pure/System/session.ML Fri May 17 18:19:42 2013 +0200 @@ -1,7 +1,7 @@ (* Title: Pure/System/session.ML - Author: Markus Wenzel, TU Muenchen + Author: Makarius -Session management -- internal state of logic images. +Session management -- internal state of logic images (not thread-safe). *) signature SESSION = @@ -11,10 +11,6 @@ val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list -> string -> string * string -> bool * string -> bool -> unit val finish: unit -> unit - val with_timing: string -> bool -> ('a -> 'b) -> 'a -> 'b - val use_dir: string -> string -> bool -> string list -> bool -> bool -> string -> - string -> bool -> string list -> string -> string -> bool * string -> - string -> int -> bool -> bool -> int -> int -> int -> int -> unit end; structure Session: SESSION = @@ -63,67 +59,4 @@ Event_Timer.shutdown (); session_finished := true); - -(* timing within ML *) - -fun with_timing name verbose f x = - let - val start = Timing.start (); - val y = f x; - val timing = Timing.result start; - - val threads = string_of_int (Multithreading.max_threads_value ()); - val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing) - |> Real.fmt (StringCvt.FIX (SOME 2)); - - val timing_props = - [("threads", threads)] @ Markup.timing_properties timing @ [("factor", factor)]; - val _ = writeln ("\fTiming = " ^ YXML.string_of_body (XML.Encode.properties timing_props)); - val _ = - if verbose then - Output.physical_stderr ("Timing " ^ name ^ " (" ^ - threads ^ " threads, " ^ Timing.message timing ^ ", factor " ^ factor ^ ")\n") - else (); - in y end; - - -(* use_dir *) - -fun read_variants strs = - rev (distinct (eq_fst (op =)) (rev (("document", "") :: map Present.read_variant strs))) - |> filter_out (fn (_, s) => s = "-"); - -fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent - name doc_dump rpath level timing verbose max_threads trace_threads - parallel_proofs parallel_subproofs_saturation = - ((fn () => - let - val _ = - Output.physical_stderr - "### Legacy feature: old \"isabelle usedir\" -- use \"isabelle build\" instead!\n"; - val _ = - if not reset then () - else Output.physical_stderr "### Ignoring reset (historic usedir option -r)\n"; - val _ = - if rpath = "" then () - else Output.physical_stderr "### Ignoring remote path (historic usedir option -P)\n"; - - val _ = - init build info (Path.explode info_path) doc doc_graph "" (read_variants doc_variants) - parent ("Unsorted", name) doc_dump verbose; - val res1 = (use |> with_timing item timing |> Exn.capture) root; - val res2 = Exn.capture finish (); - val _ = ignore (Par_Exn.release_all [res1, res2]); - val _ = Options.reset_default (); - in () end) - |> Unsynchronized.setmp Proofterm.proofs level - |> Unsynchronized.setmp print_mode (modes @ print_mode_value ()) - |> Unsynchronized.setmp Goal.parallel_proofs parallel_proofs - |> Unsynchronized.setmp Goal.parallel_subproofs_saturation parallel_subproofs_saturation - |> Unsynchronized.setmp Multithreading.trace trace_threads - |> Unsynchronized.setmp Multithreading.max_threads - (if Multithreading.available then max_threads - else (if max_threads = 1 then () else warning "Multithreading support unavailable"; 1))) () - handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1); - end; diff -r 9362fcd0318c -r 892061142ba6 src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML Fri May 17 17:45:51 2013 +0200 +++ b/src/Pure/Tools/build.ML Fri May 17 18:19:42 2013 +0200 @@ -43,6 +43,29 @@ | NONE => NONE); +(* session timing *) + +fun session_timing name verbose f x = + let + val start = Timing.start (); + val y = f x; + val timing = Timing.result start; + + val threads = string_of_int (Multithreading.max_threads_value ()); + val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing) + |> Real.fmt (StringCvt.FIX (SOME 2)); + + val timing_props = + [("threads", threads)] @ Markup.timing_properties timing @ [("factor", factor)]; + val _ = writeln ("\fTiming = " ^ YXML.string_of_body (XML.Encode.properties timing_props)); + val _ = + if verbose then + Output.physical_stderr ("Timing " ^ name ^ " (" ^ + threads ^ " threads, " ^ Timing.message timing ^ ", factor " ^ factor ^ ")\n") + else (); + in y end; + + (* protocol messages *) fun inline_message a args = @@ -147,7 +170,7 @@ val res1 = theories |> (List.app (use_theories_condition last_timing) - |> Session.with_timing name verbose + |> session_timing name verbose |> Unsynchronized.setmp Output.Private_Hooks.protocol_message_fn protocol_message |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads") |> Exn.capture);