--- 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.
--- 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"
--- 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 "$@"
--- 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 <<EOF
-(*
- no_document use_thys ["This_Theory1", "This_Theory2"];
- use_thys ["That_Theory1", "That_Theory2", "That_Theory3"];
-*)
-EOF
-fi
-
-
-# document directory
-
-if [ -e document ]; then
- echo "keeping $PREFIX/document" >&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 <<EOF
-\documentclass[11pt,a4paper]{article}
-\usepackage{isabelle,isabellesym}
-
-% further packages required for unusual symbols (see also
-% isabellesym.sty), use only when needed
-
-%\usepackage{amssymb}
- %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
- %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
- %\<triangleq>, \<yen>, \<lozenge>
-
-%\usepackage{eurosym}
- %for \<euro>
-
-%\usepackage[only,bigsqcap]{stmaryrd}
- %for \<Sqinter>
-
-%\usepackage{eufrak}
- %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
-
-%\usepackage{textcomp}
- %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
- %\<currency>
-
-% 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 <<EOF
-
-Notes:
-
- * 'isabelle make' processes the session (including document preparation)
-
- * $DIR/IsaMakefile contains compilation options and file dependencies
-
- * $PREFIX/document/root.tex contains the LaTeX master document setup
-
- * $PREFIX/ROOT.ML needs to contain ML code to load all theories
-
-EOF
-fi
--- a/lib/Tools/usedir Fri May 17 17:45:51 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,273 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Markus Wenzel, TU Muenchen
-#
-# DESCRIPTION: build object-logic or run examples
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: isabelle $PRG [OPTIONS] LOGIC NAME"
- echo
- echo " Options are:"
- echo " -C BOOL copy existing document directory to -D PATH (default true)"
- echo " -D PATH dump generated document sources into PATH"
- echo " -M MAX multithreading: maximum number of worker threads (default 1)"
- echo " -P PATH set path for remote theory browsing information"
- echo " -Q INT set threshold for sub-proof parallelization (default 100)"
- echo " -T LEVEL multithreading: trace level (default 0)"
- echo " -V VARIANT declare alternative document VARIANT"
- echo " -b build mode (output heap image, using current dir)"
- echo " -d FORMAT build document as FORMAT (default false)"
- echo " -f NAME use ML file NAME (default ROOT.ML)"
- echo " -g BOOL generate session graph image for document (default false)"
- echo " -i BOOL generate HTML and graph browser information (default false)"
- echo " -m MODE add print mode for output"
- echo " -p LEVEL set level of detail for proof objects (default 0)"
- echo " -q LEVEL set level of parallel proof checking (default 1)"
- echo " -r reset session path"
- echo " -s NAME override session NAME"
- echo " -t BOOL internal session timing (default false)"
- echo " -v BOOL be verbose (default false)"
- echo
- echo " Build object-logic or run examples. Also creates browsing"
- echo " information (HTML etc.) according to settings."
- echo
- echo " ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
- echo
- echo " ML_PLATFORM=$ML_PLATFORM"
- echo " ML_HOME=$ML_HOME"
- echo " ML_SYSTEM=$ML_SYSTEM"
- echo " ML_OPTIONS=$ML_OPTIONS"
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&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"
--- 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
--- 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 {*
--- 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;
--- 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);