--- a/Admin/lib/Tools/build_doc Thu Mar 10 19:15:06 2016 +0100
+++ b/Admin/lib/Tools/build_doc Thu Mar 10 22:49:24 2016 +0100
@@ -18,4 +18,4 @@
declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
-"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Build_Doc "$@"
+isabelle java "${JAVA_ARGS[@]}" isabelle.Build_Doc "$@"
--- a/Admin/lib/Tools/check_sources Thu Mar 10 19:15:06 2016 +0100
+++ b/Admin/lib/Tools/check_sources Thu Mar 10 22:49:24 2016 +0100
@@ -6,4 +6,4 @@
isabelle_admin_build jars || exit $?
-"$ISABELLE_TOOL" java isabelle.Check_Sources "$@"
+isabelle java isabelle.Check_Sources "$@"
--- a/NEWS Thu Mar 10 19:15:06 2016 +0100
+++ b/NEWS Thu Mar 10 22:49:24 2016 +0100
@@ -218,6 +218,35 @@
*** System ***
+* The Isabelle system environment always ensures that the main
+executables are found within the shell search $PATH: "isabelle" and
+"isabelle_scala_script".
+
+* The Isabelle ML process is now managed directly by Isabelle/Scala, and
+shell scripts merely provide optional command-line access. In
+particular:
+
+ . Scala module ML_Process to connect to the raw ML process,
+ with interaction via stdin/stdout/stderr or in batch mode;
+ . command-line tool "isabelle console" as interactive wrapper;
+ . command-line tool "isabelle process" as batch mode wrapper.
+
+* The executable "isabelle_process" has been discontinued. Tools and
+prover front-ends should use ML_Process or Isabelle_Process in
+Isabelle/Scala. INCOMPATIBILITY.
+
+* New command-line tool "isabelle process" supports ML evaluation of
+literal expressions (option -e) or files (option -f) in the context of a
+given heap image. Errors lead to premature exit of the ML process with
+return code 1.
+
+* Command-line tool "isabelle console" provides option -r to help to
+bootstrapping Isabelle/Pure interactively.
+
+* Command-line tool "isabelle yxml" has been discontinued.
+INCOMPATIBILITY, use operations from the modules "XML" and "YXML" in
+Isabelle/ML or Isabelle/Scala.
+
* File.bash_string, File.bash_path etc. represent Isabelle/ML and
Isabelle/Scala strings authentically within GNU bash. This is useful to
produce robust shell scripts under program control, without worrying
@@ -226,29 +255,10 @@
less versatile) operations File.shell_quote, File.shell_path etc. have
been discontinued.
-* The Isabelle system environment always ensures that the main
-executables are found within the PATH: isabelle, isabelle_process,
-isabelle_scala_script.
-
-* Command-line tool "isabelle_process" no longer supports writable heap
-images. INCOMPATIBILITY in exotic situations where "isabelle build"
-cannot be used: the structure ML_Heap provides operations to save the ML
-heap under program control.
-
-* Command-line tool "isabelle_process" supports ML evaluation of literal
-expressions (option -e) or files (option -f). Errors lead to premature
-exit of the ML process with return code 1.
-
-* Command-line tool "isabelle console -r" helps to bootstrap
-Isabelle/Pure interactively.
-
-* The somewhat pointless command-line tool "isabelle yxml" has been
-discontinued. INCOMPATIBILITY, use operations from the modules "XML" and
-"YXML" in Isabelle/ML or Isabelle/Scala.
-
* SML/NJ and old versions of Poly/ML are no longer supported.
+
New in Isabelle2016 (February 2016)
-----------------------------------
--- a/bin/isabelle_process Thu Mar 10 19:15:06 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# Isabelle process startup script.
-
-if [ -L "$0" ]; then
- TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
- exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
-fi
-
-ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
-source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
-
-
-isabelle_admin_build jars || exit $?
-
-"$ISABELLE_TOOL" java isabelle.Isabelle_Process "$@"
--- a/lib/Tools/browser Thu Mar 10 19:15:06 2016 +0100
+++ b/lib/Tools/browser Thu Mar 10 22:49:24 2016 +0100
@@ -86,9 +86,9 @@
esac
if [ -z "$OUTFILE" ]; then
- "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser "$(platform_path "$PRIVATE_FILE")"
+ isabelle java GraphBrowser.GraphBrowser "$(platform_path "$PRIVATE_FILE")"
else
- "$ISABELLE_TOOL" java GraphBrowser.Console "$(platform_path "$PRIVATE_FILE")" "$(platform_path "$OUTFILE")"
+ isabelle java GraphBrowser.Console "$(platform_path "$PRIVATE_FILE")" "$(platform_path "$OUTFILE")"
fi
RC="$?"
@@ -102,7 +102,7 @@
rm -f "$PRIVATE_FILE"
elif [ -z "$ADMIN_BUILD" ]; then
[ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO"
- exec "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser
+ exec isabelle java GraphBrowser.GraphBrowser
else
RC=0
fi
--- a/lib/Tools/build Thu Mar 10 19:15:06 2016 +0100
+++ b/lib/Tools/build Thu Mar 10 22:49:24 2016 +0100
@@ -4,7 +4,7 @@
#
# DESCRIPTION: build and manage Isabelle sessions
-## settings
+isabelle_admin_build jars || exit $?
case "$ISABELLE_JAVA_PLATFORM" in
x86-*)
@@ -15,174 +15,6 @@
;;
esac
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function show_settings()
-{
- local PREFIX="$1"
- echo "${PREFIX}ISABELLE_BUILD_OPTIONS=\"$ISABELLE_BUILD_OPTIONS\""
- echo
- echo "${PREFIX}ISABELLE_BUILD_JAVA_OPTIONS=\"$ISABELLE_BUILD_JAVA_OPTIONS\""
- echo
- echo "${PREFIX}ML_PLATFORM=\"$ML_PLATFORM\""
- echo "${PREFIX}ML_HOME=\"$ML_HOME\""
- echo "${PREFIX}ML_SYSTEM=\"$ML_SYSTEM\""
- echo "${PREFIX}ML_OPTIONS=\"$ML_OPTIONS\""
-}
-
-function usage()
-{
- echo
- echo "Usage: isabelle $PRG [OPTIONS] [SESSIONS ...]"
- echo
- echo " Options are:"
- echo " -D DIR include session directory and select its sessions"
- echo " -R operate on requirements of selected sessions"
- echo " -X NAME exclude sessions from group NAME and all descendants"
- echo " -a select all sessions"
- echo " -b build heap images"
- echo " -c clean build"
- echo " -d DIR include session directory"
- echo " -g NAME select session group NAME"
- echo " -j INT maximum number of parallel jobs (default 1)"
- echo " -k KEYWORD check theory sources for conflicts with proposed keywords"
- echo " -l list session source files"
- echo " -n no build -- test dependencies only"
- echo " -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)"
- echo " -s system build mode: produce output in ISABELLE_HOME"
- echo " -v verbose"
- echo " -x NAME exclude session NAME and all descendants"
- echo
- echo " Build and manage Isabelle sessions, depending on implicit"
- show_settings " "
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-function check_number()
-{
- [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
-}
-
-
-## process command line
-
-declare -a SELECT_DIRS=()
-REQUIREMENTS=false
-declare -a EXCLUDE_SESSION_GROUPS=()
-ALL_SESSIONS=false
-BUILD_HEAP=false
-CLEAN_BUILD=false
-declare -a INCLUDE_DIRS=()
-declare -a SESSION_GROUPS=()
-MAX_JOBS=1
-declare -a CHECK_KEYWORDS=()
-LIST_FILES=false
-NO_BUILD=false
-eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
-SYSTEM_MODE=false
-VERBOSE=false
-declare -a EXCLUDE_SESSIONS=()
+eval "declare -a JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
-while getopts "D:RX:abcd:g:j:k:lno:svx:" OPT
-do
- case "$OPT" in
- D)
- SELECT_DIRS["${#SELECT_DIRS[@]}"]="$OPTARG"
- ;;
- R)
- REQUIREMENTS="true"
- ;;
- X)
- EXCLUDE_SESSION_GROUPS["${#EXCLUDE_SESSION_GROUPS[@]}"]="$OPTARG"
- ;;
- a)
- ALL_SESSIONS="true"
- ;;
- b)
- BUILD_HEAP="true"
- ;;
- c)
- CLEAN_BUILD="true"
- ;;
- d)
- INCLUDE_DIRS["${#INCLUDE_DIRS[@]}"]="$OPTARG"
- ;;
- g)
- SESSION_GROUPS["${#SESSION_GROUPS[@]}"]="$OPTARG"
- ;;
- j)
- check_number "$OPTARG"
- MAX_JOBS="$OPTARG"
- ;;
- k)
- CHECK_KEYWORDS["${#CHECK_KEYWORDS[@]}"]="$OPTARG"
- ;;
- l)
- LIST_FILES="true"
- ;;
- n)
- NO_BUILD="true"
- ;;
- o)
- BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="$OPTARG"
- ;;
- s)
- SYSTEM_MODE="true"
- ;;
- v)
- VERBOSE="true"
- ;;
- x)
- EXCLUDE_SESSIONS["${#EXCLUDE_SESSIONS[@]}"]="$OPTARG"
- ;;
- \?)
- usage
- ;;
- esac
-done
-
-shift $(($OPTIND - 1))
-
-
-## main
-
-isabelle_admin_build jars || exit $?
-
-if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then
- echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
-
- show_settings ""
- echo
-fi
-
-declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
-
-. "$ISABELLE_HOME/lib/scripts/timestart.bash"
-
-"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Build \
- "$REQUIREMENTS" "$ALL_SESSIONS" "$BUILD_HEAP" "$CLEAN_BUILD" "$MAX_JOBS" \
- "$LIST_FILES" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
- "${INCLUDE_DIRS[@]}" $'\n' "${SELECT_DIRS[@]}" $'\n' \
- "${SESSION_GROUPS[@]}" $'\n' "${CHECK_KEYWORDS[@]}" $'\n' \
- "${BUILD_OPTIONS[@]}" $'\n' "${EXCLUDE_SESSION_GROUPS[@]}" $'\n' \
- "${EXCLUDE_SESSIONS[@]}" $'\n' "$@"
-RC="$?"
-
-if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then
- echo -n "Finished at "; date
-fi
-
-. "$ISABELLE_HOME/lib/scripts/timestop.bash"
-echo "$TIMES_REPORT"
-
-exit "$RC"
+exec isabelle java "${JAVA_ARGS[@]}" isabelle.Build "$@"
--- a/lib/Tools/console Thu Mar 10 19:15:06 2016 +0100
+++ b/lib/Tools/console Thu Mar 10 22:49:24 2016 +0100
@@ -2,7 +2,7 @@
#
# Author: Makarius
#
-# DESCRIPTION: run Isabelle process with raw ML console and line editor
+# DESCRIPTION: raw ML process (interactive mode)
isabelle_admin_build jars || exit $?
@@ -21,8 +21,8 @@
if type -p "$ISABELLE_LINE_EDITOR" > /dev/null
then
- exec "$ISABELLE_LINE_EDITOR" "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@"
+ exec "$ISABELLE_LINE_EDITOR" isabelle java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@"
else
echo "### No line editor: \"$ISABELLE_LINE_EDITOR\""
- exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@"
+ exec isabelle java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@"
fi
--- a/lib/Tools/doc Thu Mar 10 19:15:06 2016 +0100
+++ b/lib/Tools/doc Thu Mar 10 22:49:24 2016 +0100
@@ -6,4 +6,4 @@
isabelle_admin_build jars || exit $?
-"$ISABELLE_TOOL" java isabelle.Doc "$@"
+exec isabelle java isabelle.Doc "$@"
--- a/lib/Tools/document Thu Mar 10 19:15:06 2016 +0100
+++ b/lib/Tools/document Thu Mar 10 22:49:24 2016 +0100
@@ -128,12 +128,12 @@
./build "$OUTFORMAT" "$NAME"
RC="$?"
else
- "$ISABELLE_TOOL" latex -o sty "$ROOT_NAME.tex" && \
- "$ISABELLE_TOOL" latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \
- { [ ! -f "$ROOT_NAME.bib" ] || "$ISABELLE_TOOL" latex -o bbl "$ROOT_NAME.tex"; } && \
- { [ ! -f "$ROOT_NAME.idx" ] || "$ISABELLE_TOOL" latex -o idx "$ROOT_NAME.tex"; } && \
- "$ISABELLE_TOOL" latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \
- "$ISABELLE_TOOL" latex -o "$OUTFORMAT" "$ROOT_NAME.tex"
+ isabelle latex -o sty "$ROOT_NAME.tex" && \
+ isabelle latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \
+ { [ ! -f "$ROOT_NAME.bib" ] || isabelle latex -o bbl "$ROOT_NAME.tex"; } && \
+ { [ ! -f "$ROOT_NAME.idx" ] || isabelle latex -o idx "$ROOT_NAME.tex"; } && \
+ isabelle latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \
+ isabelle latex -o "$OUTFORMAT" "$ROOT_NAME.tex"
RC="$?"
fi
--- a/lib/Tools/install Thu Mar 10 19:15:06 2016 +0100
+++ b/lib/Tools/install Thu Mar 10 22:49:24 2016 +0100
@@ -63,7 +63,7 @@
mkdir -p "$BINDIR" || fail "Bad directory: \"$BINDIR\""
-for NAME in isabelle isabelle_process isabelle_scala_script
+for NAME in isabelle isabelle_scala_script
do
BIN="$BINDIR/$NAME"
DIST="$DISTDIR/bin/$NAME"
--- a/lib/Tools/options Thu Mar 10 19:15:06 2016 +0100
+++ b/lib/Tools/options Thu Mar 10 22:49:24 2016 +0100
@@ -6,4 +6,4 @@
isabelle_admin_build jars || exit $?
-exec "$ISABELLE_TOOL" java isabelle.Options "$@"
+exec isabelle java isabelle.Options "$@"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/process Thu Mar 10 22:49:24 2016 +0100
@@ -0,0 +1,22 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: raw ML process (batch mode)
+
+isabelle_admin_build jars || exit $?
+
+case "$ISABELLE_JAVA_PLATFORM" in
+ x86-*)
+ ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS32"
+ ;;
+ x86_64-*)
+ ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS64"
+ ;;
+esac
+
+declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
+
+mkdir -p "$ISABELLE_TMP_PREFIX" || exit $?
+
+exec isabelle java isabelle.ML_Process "$@"
--- a/lib/Tools/update_cartouches Thu Mar 10 19:15:06 2016 +0100
+++ b/lib/Tools/update_cartouches Thu Mar 10 22:49:24 2016 +0100
@@ -6,4 +6,4 @@
isabelle_admin_build jars || exit $?
-"$ISABELLE_TOOL" java isabelle.Update_Cartouches "$@"
+exec isabelle java isabelle.Update_Cartouches "$@"
--- a/lib/Tools/update_header Thu Mar 10 19:15:06 2016 +0100
+++ b/lib/Tools/update_header Thu Mar 10 22:49:24 2016 +0100
@@ -6,4 +6,4 @@
isabelle_admin_build jars || exit $?
-"$ISABELLE_TOOL" java isabelle.Update_Header "$@"
+exec isabelle java isabelle.Update_Header "$@"
--- a/lib/Tools/update_then Thu Mar 10 19:15:06 2016 +0100
+++ b/lib/Tools/update_then Thu Mar 10 22:49:24 2016 +0100
@@ -6,4 +6,4 @@
isabelle_admin_build jars || exit $?
-"$ISABELLE_TOOL" java isabelle.Update_Then "$@"
+exec isabelle java isabelle.Update_Then "$@"
--- a/lib/Tools/update_theorems Thu Mar 10 19:15:06 2016 +0100
+++ b/lib/Tools/update_theorems Thu Mar 10 22:49:24 2016 +0100
@@ -6,4 +6,4 @@
isabelle_admin_build jars || exit $?
-"$ISABELLE_TOOL" java isabelle.Update_Theorems "$@"
+exec isabelle java isabelle.Update_Theorems "$@"
--- a/lib/scripts/getsettings Thu Mar 10 19:15:06 2016 +0100
+++ b/lib/scripts/getsettings Thu Mar 10 22:49:24 2016 +0100
@@ -55,7 +55,6 @@
#main executables
ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
-ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle_process"
ISABELLE_SCALA_SCRIPT="$ISABELLE_HOME/bin/isabelle_scala_script"
PATH="$ISABELLE_HOME/bin:$PATH"
--- a/src/Doc/Classes/document/build Thu Mar 10 19:15:06 2016 +0100
+++ b/src/Doc/Classes/document/build Thu Mar 10 22:49:24 2016 +0100
@@ -5,6 +5,6 @@
FORMAT="$1"
VARIANT="$2"
-"$ISABELLE_TOOL" logo Isar
+isabelle logo Isar
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/Codegen/document/build Thu Mar 10 19:15:06 2016 +0100
+++ b/src/Doc/Codegen/document/build Thu Mar 10 22:49:24 2016 +0100
@@ -8,7 +8,7 @@
# ad-hoc patching of temporary path from sources
perl -i -pe 's/\{\\isachardollar\}ISABELLE\{\\isacharunderscore\}TMP\{\\isacharslash\}examples/examples/g' *.tex
-"$ISABELLE_TOOL" logo Isar
+isabelle logo Isar
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
# clean up afterwards
--- a/src/Doc/Eisbach/document/build Thu Mar 10 19:15:06 2016 +0100
+++ b/src/Doc/Eisbach/document/build Thu Mar 10 22:49:24 2016 +0100
@@ -5,6 +5,6 @@
FORMAT="$1"
VARIANT="$2"
-"$ISABELLE_TOOL" logo Eisbach
+isabelle logo Eisbach
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/Implementation/document/build Thu Mar 10 19:15:06 2016 +0100
+++ b/src/Doc/Implementation/document/build Thu Mar 10 22:49:24 2016 +0100
@@ -5,6 +5,6 @@
FORMAT="$1"
VARIANT="$2"
-"$ISABELLE_TOOL" logo Isar
+isabelle logo Isar
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/Intro/document/build Thu Mar 10 19:15:06 2016 +0100
+++ b/src/Doc/Intro/document/build Thu Mar 10 22:49:24 2016 +0100
@@ -5,6 +5,6 @@
FORMAT="$1"
VARIANT="$2"
-"$ISABELLE_TOOL" logo
+isabelle logo
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/Isar_Ref/document/build Thu Mar 10 19:15:06 2016 +0100
+++ b/src/Doc/Isar_Ref/document/build Thu Mar 10 22:49:24 2016 +0100
@@ -5,7 +5,7 @@
FORMAT="$1"
VARIANT="$2"
-"$ISABELLE_TOOL" logo Isar
+isabelle logo Isar
./showsymbols "$ISABELLE_HOME/lib/texinputs/isabellesym.sty" > syms.tex
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/JEdit/document/build Thu Mar 10 19:15:06 2016 +0100
+++ b/src/Doc/JEdit/document/build Thu Mar 10 22:49:24 2016 +0100
@@ -5,6 +5,6 @@
FORMAT="$1"
VARIANT="$2"
-"$ISABELLE_TOOL" logo jEdit
+isabelle logo jEdit
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/Logics/document/build Thu Mar 10 19:15:06 2016 +0100
+++ b/src/Doc/Logics/document/build Thu Mar 10 22:49:24 2016 +0100
@@ -5,6 +5,6 @@
FORMAT="$1"
VARIANT="$2"
-"$ISABELLE_TOOL" logo
+isabelle logo
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/Logics_ZF/document/build Thu Mar 10 19:15:06 2016 +0100
+++ b/src/Doc/Logics_ZF/document/build Thu Mar 10 22:49:24 2016 +0100
@@ -5,6 +5,6 @@
FORMAT="$1"
VARIANT="$2"
-"$ISABELLE_TOOL" logo ZF
+isabelle logo ZF
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/Main/document/build Thu Mar 10 19:15:06 2016 +0100
+++ b/src/Doc/Main/document/build Thu Mar 10 22:49:24 2016 +0100
@@ -5,6 +5,6 @@
FORMAT="$1"
VARIANT="$2"
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o "$FORMAT"
+isabelle latex -o "$FORMAT"
+isabelle latex -o "$FORMAT"
--- a/src/Doc/Nitpick/document/build Thu Mar 10 19:15:06 2016 +0100
+++ b/src/Doc/Nitpick/document/build Thu Mar 10 22:49:24 2016 +0100
@@ -5,6 +5,6 @@
FORMAT="$1"
VARIANT="$2"
-"$ISABELLE_TOOL" logo Nitpick
+isabelle logo Nitpick
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/Prog_Prove/document/build Thu Mar 10 19:15:06 2016 +0100
+++ b/src/Doc/Prog_Prove/document/build Thu Mar 10 22:49:24 2016 +0100
@@ -5,6 +5,6 @@
FORMAT="$1"
VARIANT="$2"
-"$ISABELLE_TOOL" logo HOL
+isabelle logo HOL
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/Sledgehammer/document/build Thu Mar 10 19:15:06 2016 +0100
+++ b/src/Doc/Sledgehammer/document/build Thu Mar 10 22:49:24 2016 +0100
@@ -5,6 +5,6 @@
FORMAT="$1"
VARIANT="$2"
-"$ISABELLE_TOOL" logo -n isabelle_sledgehammer "S/H"
+isabelle logo -n isabelle_sledgehammer "S/H"
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/System/Basics.thy Thu Mar 10 19:15:06 2016 +0100
+++ b/src/Doc/System/Basics.thy Thu Mar 10 22:49:24 2016 +0100
@@ -7,49 +7,24 @@
chapter \<open>The Isabelle system environment\<close>
text \<open>
- This manual describes Isabelle together with related tools and user
- interfaces as seen from a system oriented view. See also the \<^emph>\<open>Isabelle/Isar
- Reference Manual\<close> @{cite "isabelle-isar-ref"} for the actual Isabelle input
- language and related concepts, and \<^emph>\<open>The Isabelle/Isar Implementation
- Manual\<close> @{cite "isabelle-implementation"} for the main concepts of the
- underlying implementation in Isabelle/ML.
-
- \<^medskip>
- The Isabelle system environment provides the following basic infrastructure
- to integrate tools smoothly.
-
- \<^enum> The \<^emph>\<open>Isabelle settings\<close> mechanism provides process environment variables
- to all Isabelle executables (including tools and user interfaces).
-
- \<^enum> The raw \<^emph>\<open>Isabelle process\<close> (@{executable_ref "isabelle_process"}) runs
- logic sessions in batch mode. This is rarely required for regular users.
-
- \<^enum> The main \<^emph>\<open>Isabelle tool wrapper\<close> (@{executable_ref isabelle}) provides a
- generic startup environment Isabelle related utilities, user interfaces etc.
- Such tools automatically benefit from the settings mechanism.
+ This manual describes Isabelle together with related tools as seen from a
+ system oriented view. See also the \<^emph>\<open>Isabelle/Isar Reference Manual\<close> @{cite
+ "isabelle-isar-ref"} for the actual Isabelle input language and related
+ concepts, and \<^emph>\<open>The Isabelle/Isar Implementation Manual\<close> @{cite
+ "isabelle-implementation"} for the main concepts of the underlying
+ implementation in Isabelle/ML.
\<close>
section \<open>Isabelle settings \label{sec:settings}\<close>
text \<open>
- The Isabelle system heavily depends on the \<^emph>\<open>settings mechanism\<close>.
- Essentially, this is a statically scoped collection of environment
+ Isabelle executables may depend on the \<^emph>\<open>Isabelle settings\<close> within the
+ process environment. This is a statically scoped collection of environment
variables, such as @{setting ISABELLE_HOME}, @{setting ML_SYSTEM}, @{setting
ML_HOME}. These variables are \<^emph>\<open>not\<close> intended to be set directly from the
- shell, though. Isabelle employs a somewhat more sophisticated scheme of
- \<^emph>\<open>settings files\<close> --- one for site-wide defaults, another for additional
- user-specific modifications. With all configuration variables in clearly
- defined places, this scheme is more maintainable and user-friendly than
- global shell environment variables.
-
- In particular, we avoid the typical situation where prospective users of a
- software package are told to put several things into their shell startup
- scripts, before being able to actually run the program. Isabelle requires
- none such administrative chores of its end-users --- the executables can be
- invoked straight away. Occasionally, users would still want to put the
- @{file "$ISABELLE_HOME/bin"} directory into their shell's search path, but
- this is not required.
+ shell, but are provided by Isabelle \<^emph>\<open>components\<close> their \<^emph>\<open>settings files\<close> as
+ explained below.
\<close>
@@ -101,9 +76,8 @@
\<^medskip>
A few variables are somewhat special:
- \<^item> @{setting_def ISABELLE_PROCESS} and @{setting_def ISABELLE_TOOL} are set
- automatically to the absolute path names of the @{executable
- "isabelle_process"} and @{executable isabelle} executables, respectively.
+ \<^item> @{setting_def ISABELLE_TOOL} is set automatically to the absolute path
+ name of the @{executable isabelle} executables.
\<^item> @{setting_ref ISABELLE_OUTPUT} will have the identifiers of the Isabelle
distribution (cf.\ @{setting ISABELLE_IDENTIFIER}) and the ML system (cf.\
@@ -162,11 +136,10 @@
@{verbatim [display] \<open>"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"\<close>}
- \<^descr>[@{setting_def ISABELLE_PROCESS}\<open>\<^sup>*\<close>, @{setting ISABELLE_TOOL}\<open>\<^sup>*\<close>] are
- automatically set to the full path names of the @{executable
- "isabelle_process"} and @{executable isabelle} executables, respectively.
- Thus other tools and scripts need not assume that the @{file
- "$ISABELLE_HOME/bin"} directory is on the current search path of the shell.
+ \<^descr>[@{setting ISABELLE_TOOL}\<open>\<^sup>*\<close>] is automatically set to the full path name
+ of the @{executable isabelle} executable. Thus other tools and scripts need
+ not assume that the @{file "$ISABELLE_HOME/bin"} directory is on the current
+ search path of the shell.
\<^descr>[@{setting_def ISABELLE_IDENTIFIER}\<open>\<^sup>*\<close>] refers to the name of this
Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2012\<close>''.
@@ -228,8 +201,8 @@
\<^verbatim>\<open>dvi\<close> files.
\<^descr>[@{setting_def ISABELLE_TMP_PREFIX}\<open>\<^sup>*\<close>] is the prefix from which any
- running @{executable "isabelle_process"} derives an individual directory for
- temporary files.
+ running Isabelle ML process derives an individual directory for temporary
+ files.
\<close>
@@ -284,13 +257,52 @@
\<close>
-section \<open>The raw Isabelle process \label{sec:isabelle-process}\<close>
+section \<open>The Isabelle tool wrapper \label{sec:isabelle-tool}\<close>
text \<open>
- The @{executable_def "isabelle_process"} executable runs a bare-bone
- Isabelle logic session in batch mode:
+ The main \<^emph>\<open>Isabelle tool wrapper\<close> provides a generic startup environment for
+ Isabelle related utilities, user interfaces etc. Such tools automatically
+ benefit from the settings mechanism. All Isabelle command-line tools are
+ invoked via a common wrapper --- @{executable_ref isabelle}:
@{verbatim [display]
-\<open>Usage: isabelle_process [OPTIONS] [HEAP]
+\<open>Usage: isabelle TOOL [ARGS ...]
+
+ Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help.
+
+Available tools:
+ ...\<close>}
+
+ In principle, Isabelle tools are ordinary executable scripts that are run
+ within the Isabelle settings environment, see \secref{sec:settings}. The set
+ of available tools is collected by @{executable isabelle} from the
+ directories listed in the @{setting ISABELLE_TOOLS} setting. Do not try to
+ call the scripts directly from the shell. Neither should you add the tool
+ directories to your shell's search path!
+\<close>
+
+
+subsubsection \<open>Examples\<close>
+
+text \<open>
+ Show the list of available documentation of the Isabelle distribution:
+ @{verbatim [display] \<open>isabelle doc\<close>}
+
+ View a certain document as follows:
+ @{verbatim [display] \<open>isabelle doc system\<close>}
+
+ Query the Isabelle settings environment:
+ @{verbatim [display] \<open>isabelle getenv ISABELLE_HOME_USER\<close>}
+\<close>
+
+
+section \<open>The raw Isabelle ML process\<close>
+
+subsection \<open>Batch mode \label{sec:tool-process}\<close>
+
+text \<open>
+ The @{tool_def process} tool runs the raw ML process in batch mode:
+ @{verbatim [display]
+\<open>Usage: isabelle process [OPTIONS] [HEAP]
Options are:
-e ML_EXPR evaluate ML expression on startup
@@ -298,8 +310,10 @@
-m MODE add print mode for output
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- If HEAP is a plain name (default $ISABELLE_LOGIC), it is searched in
- $ISABELLE_PATH; if it contains a slash, it is taken as literal file;
+ Run the raw Isabelle ML process in batch mode, using a given heap image.
+
+ If HEAP is a plain name (default ISABELLE_LOGIC), it is searched in
+ ISABELLE_PATH; if it contains a slash, it is taken as literal file;
if it is RAW_ML_SYSTEM, the initial ML heap is used.\<close>}
Heap files without explicit directory specifications are looked up in the
@@ -328,49 +342,60 @@
\<close>
-subsubsection \<open>Examples\<close>
+subsubsection \<open>Example\<close>
text \<open>
- In order to demonstrate batch execution of Isabelle, we retrieve the \<^verbatim>\<open>Main\<close>
- theory value from the theory loader within ML (observe the delicate quoting
- rules for the Bash shell vs.\ ML):
- @{verbatim [display] \<open>isabelle_process -e 'Thy_Info.get_theory "Main"' HOL\<close>}
+ The subsequent example retrieves the \<^verbatim>\<open>Main\<close> theory value from the theory
+ loader within ML:
+ @{verbatim [display] \<open>isabelle process -e 'Thy_Info.get_theory "Main"' HOL\<close>}
+
+ Observe the delicate quoting rules for the Bash shell vs.\ ML. The
+ Isabelle/ML and Scala libraries provide functions for that, but here we need
+ to do it manually.
\<close>
-section \<open>The Isabelle tool wrapper \label{sec:isabelle-tool}\<close>
+subsection \<open>Interactive mode\<close>
text \<open>
- All Isabelle related tools and interfaces are called via a common wrapper
- --- @{executable isabelle}:
+ The @{tool_def console} tool runs the raw ML process with interactive
+ console and line editor:
@{verbatim [display]
-\<open>Usage: isabelle TOOL [ARGS ...]
+\<open>Usage: isabelle console [OPTIONS]
- Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help.
+ Options are:
+ -d DIR include session directory
+ -l NAME logic session name (default ISABELLE_LOGIC)
+ -m MODE add print mode for output
+ -n no build of session image on startup
+ -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
+ -r logic session is RAW_ML_SYSTEM
+ -s system build mode for session image
-Available tools:
- ...\<close>}
+ Build a logic session image and run the raw Isabelle ML process
+ in interactive mode, with line editor ISABELLE_LINE_EDITOR.\<close>}
- In principle, Isabelle tools are ordinary executable scripts that are run
- within the Isabelle settings environment, see \secref{sec:settings}. The set
- of available tools is collected by @{executable isabelle} from the
- directories listed in the @{setting ISABELLE_TOOLS} setting. Do not try to
- call the scripts directly from the shell. Neither should you add the tool
- directories to your shell's search path!
-\<close>
+ Option \<^verbatim>\<open>-l\<close> specifies the logic session name. By default, its heap image is
+ checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that. Option \<^verbatim>\<open>-r\<close>
+ abbreviates \<^verbatim>\<open>-l RAW_ML_SYSTEM\<close>, which is relevant to bootstrap
+ Isabelle/Pure interactively.
+ Options \<^verbatim>\<open>-d\<close> and \<^verbatim>\<open>-s\<close> have the same meaning as for @{tool build}
+ (\secref{sec:tool-build}).
+
+ Options \<^verbatim>\<open>-m\<close> and \<^verbatim>\<open>-o\<close> have the same meaning as for @{tool process}
+ (\secref{sec:tool-process}).
-subsubsection \<open>Examples\<close>
-
-text \<open>
- Show the list of available documentation of the Isabelle distribution:
- @{verbatim [display] \<open>isabelle doc\<close>}
+ \<^medskip>
+ The Isabelle/ML process is run through the line editor that is specified via
+ the settings variable @{setting ISABELLE_LINE_EDITOR} (e.g.\
+ @{executable_def rlwrap} for GNU readline); the fall-back is to use plain
+ standard input/output.
- View a certain document as follows:
- @{verbatim [display] \<open>isabelle doc system\<close>}
-
- Query the Isabelle settings environment:
- @{verbatim [display] \<open>isabelle getenv ISABELLE_HOME_USER\<close>}
+ The user is connected to the raw ML toplevel loop: this is neither
+ Isabelle/Isar nor Isabelle/ML within the usual formal context. The most
+ relevant ML commands at this stage are @{ML use}, @{ML use_thy}, @{ML
+ use_thys}.
\<close>
--- a/src/Doc/System/Misc.thy Thu Mar 10 19:15:06 2016 +0100
+++ b/src/Doc/System/Misc.thy Thu Mar 10 22:49:24 2016 +0100
@@ -56,49 +56,6 @@
\<close>
-section \<open>Raw ML console\<close>
-
-text \<open>
- The @{tool_def console} tool runs the Isabelle process with raw ML console:
- @{verbatim [display]
-\<open>Usage: isabelle console [OPTIONS]
-
- Options are:
- -d DIR include session directory
- -l NAME logic session name (default ISABELLE_LOGIC)
- -m MODE add print mode for output
- -n no build of session image on startup
- -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- -r logic session is RAW_ML_SYSTEM
- -s system build mode for session image
-
- Run Isabelle process with raw ML console and line editor
- (default ISABELLE_LINE_EDITOR).\<close>}
-
- Option \<^verbatim>\<open>-l\<close> specifies the logic session name. By default, its heap image is
- checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that. Option \<^verbatim>\<open>-r\<close>
- abbreviates \<^verbatim>\<open>-l RAW_ML_SYSTEM\<close>, which is relevant to bootstrap
- Isabelle/Pure interactively.
-
- Options \<^verbatim>\<open>-d\<close> and \<^verbatim>\<open>-s\<close> have the same meaning as for @{tool build}
- (\secref{sec:tool-build}).
-
- Options \<^verbatim>\<open>-m\<close> and \<^verbatim>\<open>-o\<close> have the same meaning as for the raw @{executable
- isabelle_process} (\secref{sec:isabelle-process}).
-
- \<^medskip>
- The Isabelle/ML process is run through the line editor that is specified via
- the settings variable @{setting ISABELLE_LINE_EDITOR} (e.g.\
- @{executable_def rlwrap} for GNU readline); the fall-back is to use plain
- standard input/output.
-
- The user is connected to the raw ML toplevel loop: this is neither
- Isabelle/Isar nor Isabelle/ML within the usual formal context. The most
- relevant ML commands at this stage are @{ML use}, @{ML use_thy}, @{ML
- use_thys}.
-\<close>
-
-
section \<open>Displaying documents \label{sec:tool-display}\<close>
text \<open>
@@ -213,7 +170,7 @@
determined by @{setting ISABELLE_HOME}.
The \<open>BINDIR\<close> argument tells where executable wrapper scripts for
- @{executable "isabelle_process"} and @{executable isabelle} should be
+ @{executable "isabelle"} and @{executable isabelle_scala_script} should be
placed, which is typically a directory in the shell's @{setting PATH}, such
as \<^verbatim>\<open>$HOME/bin\<close>.
--- a/src/Doc/System/Presentation.thy Thu Mar 10 19:15:06 2016 +0100
+++ b/src/Doc/System/Presentation.thy Thu Mar 10 22:49:24 2016 +0100
@@ -17,11 +17,10 @@
The tools @{tool_ref mkroot} and @{tool_ref build} provide the primary means
for managing Isabelle sessions, including proper setup for presentation;
- @{tool build} takes care to have @{executable_ref "isabelle_process"} run
- any additional stages required for document preparation, notably the
- @{tool_ref document} and @{tool_ref latex}. The complete tool chain for
- managing batch-mode Isabelle sessions is illustrated in
- \figref{fig:session-tools}.
+ @{tool build} tells the Isabelle process to run any additional stages
+ required for document preparation, notably the @{tool_ref document} and
+ @{tool_ref latex}. The complete tool chain for managing batch-mode Isabelle
+ sessions is illustrated in \figref{fig:session-tools}.
\begin{figure}[htbp]
\begin{center}
@@ -34,8 +33,7 @@
@{tool_ref build} & invoked repeatedly by the user to keep
session output up-to-date (HTML, documents etc.); \\
- @{executable "isabelle_process"} & run through @{tool_ref
- build}; \\
+ @{tool_ref process} & run through @{tool_ref build}; \\
@{tool_ref document} & run by the Isabelle process if document
preparation is enabled; \\
--- a/src/Doc/System/document/build Thu Mar 10 19:15:06 2016 +0100
+++ b/src/Doc/System/document/build Thu Mar 10 22:49:24 2016 +0100
@@ -5,6 +5,6 @@
FORMAT="$1"
VARIANT="$2"
-"$ISABELLE_TOOL" logo
+isabelle logo
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/Tutorial/document/build Thu Mar 10 19:15:06 2016 +0100
+++ b/src/Doc/Tutorial/document/build Thu Mar 10 22:49:24 2016 +0100
@@ -5,10 +5,10 @@
FORMAT="$1"
VARIANT="$2"
-"$ISABELLE_TOOL" logo HOL
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o bbl
+isabelle logo HOL
+isabelle latex -o "$FORMAT"
+isabelle latex -o bbl
./isa-index root
-"$ISABELLE_TOOL" latex -o "$FORMAT"
+isabelle latex -o "$FORMAT"
[ -f root.out ] && "$ISABELLE_HOME/src/Doc/fixbookmarks" root.out
-"$ISABELLE_TOOL" latex -o "$FORMAT"
+isabelle latex -o "$FORMAT"
--- a/src/Doc/prepare_document Thu Mar 10 19:15:06 2016 +0100
+++ b/src/Doc/prepare_document Thu Mar 10 22:49:24 2016 +0100
@@ -4,13 +4,13 @@
FORMAT="$1"
-"$ISABELLE_TOOL" latex -o sty
+isabelle latex -o sty
cp "$ISABELLE_HOME/src/Doc/pdfsetup.sty" .
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o bbl
+isabelle latex -o "$FORMAT"
+isabelle latex -o bbl
[ -f root.idx ] && "$ISABELLE_HOME/src/Doc/sedindex" root
-"$ISABELLE_TOOL" latex -o "$FORMAT"
+isabelle latex -o "$FORMAT"
[ -f root.out ] && "$ISABELLE_HOME/src/Doc/fixbookmarks" root.out
-"$ISABELLE_TOOL" latex -o "$FORMAT"
+isabelle latex -o "$FORMAT"
--- a/src/HOL/Mirabelle/ex/Ex.thy Thu Mar 10 19:15:06 2016 +0100
+++ b/src/HOL/Mirabelle/ex/Ex.thy Thu Mar 10 22:49:24 2016 +0100
@@ -3,7 +3,7 @@
ML {*
val rc = Isabelle_System.bash
- "cd \"$ISABELLE_HOME/src/HOL/Library\"; \"$ISABELLE_TOOL\" mirabelle arith Inner_Product.thy";
+ "cd \"$ISABELLE_HOME/src/HOL/Library\"; isabelle mirabelle arith Inner_Product.thy";
if rc <> 0 then error ("Mirabelle example failed: " ^ string_of_int rc)
else ();
*} -- "some arbitrary small test case"
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Thu Mar 10 19:15:06 2016 +0100
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Thu Mar 10 22:49:24 2016 +0100
@@ -158,8 +158,8 @@
if ($output_log) { print "Mirabelle: $thy_file\n"; }
my $cmd =
- "\"$ENV{'ISABELLE_PROCESS'}\" " .
- "-o quick_and_dirty -o threads=1 -e 'use_thy \"$path/$new_thy_name\"' $mirabelle_logic" . $quiet;
+ "isabelle process -o quick_and_dirty -o threads=1" .
+ " -e 'use_thy \"$path/$new_thy_name\"' $mirabelle_logic" . $quiet;
my $result = system "bash", "-c", $cmd;
if ($output_log) {
--- a/src/HOL/Mutabelle/lib/Tools/mutabelle Thu Mar 10 19:15:06 2016 +0100
+++ b/src/HOL/Mutabelle/lib/Tools/mutabelle Thu Mar 10 22:49:24 2016 +0100
@@ -133,7 +133,7 @@
# execution
-"$ISABELLE_PROCESS" -o auto_time_limit=10.0 \
+isabelle process -o auto_time_limit=10.0 \
-e 'use_thy "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test"' "$MUTABELLE_LOGIC" > "$MUTABELLE_OUTPUT_PATH/err" 2>&1
--- a/src/HOL/TPTP/CASC/ReadMe Thu Mar 10 19:15:06 2016 +0100
+++ b/src/HOL/TPTP/CASC/ReadMe Thu Mar 10 22:49:24 2016 +0100
@@ -67,7 +67,7 @@
year, because Isabelle now includes its own version of Java, but the solution
back then was to replace
- exec "$ISABELLE_TOOL" java
+ exec isabelle java
in the last line of the "contrib/kodkodi-1.5.2/bin/kodkodi" script with
@@ -180,7 +180,7 @@
Then I ran
- ./bin/isabelle_process -e 'use_thy "/tmp/T";'
+ ./bin/isabelle process -e 'use_thy "/tmp/T";'
I also performed the aforementioned sanity tests.
--- a/src/HOL/TPTP/lib/Tools/tptp_graph Thu Mar 10 19:15:06 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_graph Thu Mar 10 22:49:24 2016 +0100
@@ -118,7 +118,7 @@
begin ML_file \"$TPTP_HOME/TPTP_Parser/tptp_to_dot.ML\" \
ML {* TPTP_To_Dot.write_proof_dot \"$1\" \"$2\" *} end" \
> $WORKDIR/$LOADER.thy
- "$ISABELLE_PROCESS" -e "use_thy \"$WORKDIR/$LOADER\";" Pure
+ isabelle process -e "use_thy \"$WORKDIR/$LOADER\";" Pure
}
function cleanup_workdir()
--- a/src/HOL/TPTP/lib/Tools/tptp_isabelle Thu Mar 10 19:15:06 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle Thu Mar 10 22:49:24 2016 +0100
@@ -31,5 +31,5 @@
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
> /tmp/$SCRATCH.thy
- "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
+ isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
done
--- a/src/HOL/TPTP/lib/Tools/tptp_isabelle_hot Thu Mar 10 19:15:06 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle_hot Thu Mar 10 22:49:24 2016 +0100
@@ -31,5 +31,5 @@
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
ML {* ATP_Problem_Import.isabelle_hot_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
> /tmp/$SCRATCH.thy
- "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
+ isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
done
--- a/src/HOL/TPTP/lib/Tools/tptp_nitpick Thu Mar 10 19:15:06 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_nitpick Thu Mar 10 22:49:24 2016 +0100
@@ -31,5 +31,5 @@
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
ML {* ATP_Problem_Import.nitpick_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
> /tmp/$SCRATCH.thy
- "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
+ isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
done
--- a/src/HOL/TPTP/lib/Tools/tptp_refute Thu Mar 10 19:15:06 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_refute Thu Mar 10 22:49:24 2016 +0100
@@ -30,5 +30,5 @@
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
ML {* ATP_Problem_Import.refute_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
> /tmp/$SCRATCH.thy
- "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
+ isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
done
--- a/src/HOL/TPTP/lib/Tools/tptp_sledgehammer Thu Mar 10 19:15:06 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_sledgehammer Thu Mar 10 22:49:24 2016 +0100
@@ -31,5 +31,5 @@
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
ML {* ATP_Problem_Import.sledgehammer_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
> /tmp/$SCRATCH.thy
- "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
+ isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
done
--- a/src/HOL/TPTP/lib/Tools/tptp_translate Thu Mar 10 19:15:06 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_translate Thu Mar 10 22:49:24 2016 +0100
@@ -28,4 +28,4 @@
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
ML {* ATP_Problem_Import.translate_tptp_file @{theory} \"${args[0]}\" \"${args[1]}\" *} end" \
> /tmp/$SCRATCH.thy
-"$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
+isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
--- a/src/Pure/Concurrent/bash.ML Thu Mar 10 19:15:06 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,102 +0,0 @@
-(* Title: Pure/Concurrent/bash.ML
- Author: Makarius
-
-GNU bash processes, with propagation of interrupts -- POSIX version.
-*)
-
-signature BASH =
-sig
- val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
-end;
-
-structure Bash: BASH =
-struct
-
-val process = uninterruptible (fn restore_attributes => fn script =>
- let
- datatype result = Wait | Signal | Result of int;
- val result = Synchronized.var "bash_result" Wait;
-
- val id = serial_string ();
- val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
- val out_path = File.tmp_path (Path.basic ("bash_out" ^ id));
- val err_path = File.tmp_path (Path.basic ("bash_err" ^ id));
- val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id));
-
- fun cleanup_files () =
- (try File.rm script_path;
- try File.rm out_path;
- try File.rm err_path;
- try File.rm pid_path);
- val _ = cleanup_files ();
-
- val system_thread =
- Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
- Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
- let
- val _ = File.write script_path script;
- val _ = getenv_strict "ISABELLE_BASH_PROCESS";
- val status =
- OS.Process.system
- ("exec \"$ISABELLE_BASH_PROCESS\" " ^ File.bash_path pid_path ^ " \"\"" ^
- " bash " ^ File.bash_path script_path ^
- " > " ^ File.bash_path out_path ^
- " 2> " ^ File.bash_path err_path);
- val res =
- (case Posix.Process.fromStatus status of
- Posix.Process.W_EXITED => Result 0
- | Posix.Process.W_EXITSTATUS 0wx82 => Signal
- | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w)
- | Posix.Process.W_SIGNALED s =>
- if s = Posix.Signal.int then Signal
- else Result (256 + LargeWord.toInt (Posix.Signal.toWord s))
- | Posix.Process.W_STOPPED s =>
- Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
- in Synchronized.change result (K res) end
- handle exn =>
- (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn)));
-
- fun read_pid 0 = NONE
- | read_pid count =
- (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of
- NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1))
- | some => some);
-
- fun terminate NONE = ()
- | terminate (SOME pid) =
- let
- fun kill s =
- (Posix.Process.kill
- (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)), s); true)
- handle OS.SysErr _ => false;
-
- fun multi_kill count s =
- count = 0 orelse
- (kill s; kill (Posix.Signal.fromWord 0w0)) andalso
- (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s);
- val _ =
- multi_kill 10 Posix.Signal.int andalso
- multi_kill 10 Posix.Signal.term andalso
- multi_kill 10 Posix.Signal.kill;
- in () end;
-
- fun cleanup () =
- (Standard_Thread.interrupt_unsynchronized system_thread;
- cleanup_files ());
- in
- let
- val _ =
- restore_attributes (fn () =>
- Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) ();
-
- val out = the_default "" (try File.read out_path);
- val err = the_default "" (try File.read err_path);
- val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
- val pid = read_pid 1;
- val _ = cleanup ();
- in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end
- handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn)
- end);
-
-end;
-
--- a/src/Pure/Concurrent/bash.scala Thu Mar 10 19:15:06 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,168 +0,0 @@
-/* Title: Pure/Concurrent/bash.scala
- Author: Makarius
-
-GNU bash processes, with propagation of interrupts.
-*/
-
-package isabelle
-
-
-import java.io.{File => JFile, BufferedReader, InputStreamReader,
- BufferedWriter, OutputStreamWriter}
-
-
-object Bash
-{
- private class Limited_Progress(proc: Process, progress_limit: Option[Long])
- {
- private var count = 0L
- def apply(progress: String => Unit)(line: String): Unit = synchronized {
- progress(line)
- count = count + line.length + 1
- progress_limit match {
- case Some(limit) if count > limit => proc.terminate
- case _ =>
- }
- }
- }
-
- def process(script: String,
- cwd: JFile = null,
- env: Map[String, String] = Map.empty,
- redirect: Boolean = false): Process =
- new Process(script, cwd, env, redirect)
-
- class Process private [Bash](
- script: String, cwd: JFile, env: Map[String, String], redirect: Boolean)
- extends Prover.System_Process
- {
- private val timing_file = Isabelle_System.tmp_file("bash_script")
- private val timing = Synchronized[Option[Timing]](None)
-
- private val script_file = Isabelle_System.tmp_file("bash_script")
- File.write(script_file, script)
-
- private val proc =
- Isabelle_System.process(cwd, Isabelle_System.settings(env), redirect,
- File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-",
- File.standard_path(timing_file), "bash", File.standard_path(script_file))
-
-
- // channels
-
- val stdin: BufferedWriter =
- new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, UTF8.charset))
-
- val stdout: BufferedReader =
- new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset))
-
- val stderr: BufferedReader =
- new BufferedReader(new InputStreamReader(proc.getErrorStream, UTF8.charset))
-
-
- // signals
-
- private val pid = stdout.readLine
-
- def interrupt()
- { Exn.Interrupt.postpone { Isabelle_System.kill("INT", pid) } }
-
- private def kill(signal: String): Boolean =
- Exn.Interrupt.postpone {
- Isabelle_System.kill(signal, pid)
- Isabelle_System.kill("0", pid)._2 == 0 } getOrElse true
-
- private def multi_kill(signal: String): Boolean =
- {
- var running = true
- var count = 10
- while (running && count > 0) {
- if (kill(signal)) {
- Exn.Interrupt.postpone {
- Thread.sleep(100)
- count -= 1
- }
- }
- else running = false
- }
- running
- }
-
- def terminate()
- {
- multi_kill("INT") && multi_kill("TERM") && kill("KILL")
- proc.destroy
- cleanup()
- }
-
-
- // JVM shutdown hook
-
- private val shutdown_hook = new Thread { override def run = terminate() }
-
- try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
- catch { case _: IllegalStateException => }
-
-
- // cleanup
-
- private def cleanup()
- {
- try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
- catch { case _: IllegalStateException => }
-
- script_file.delete
-
- timing.change {
- case None =>
- if (timing_file.isFile) {
- val t =
- Word.explode(File.read(timing_file)) match {
- case List(Properties.Value.Long(elapsed), Properties.Value.Long(cpu)) =>
- Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero)
- case _ => Timing.zero
- }
- timing_file.delete
- Some(t)
- }
- else Some(Timing.zero)
- case some => some
- }
- }
-
-
- // join
-
- def join: Int =
- {
- val rc = proc.waitFor
- cleanup()
- rc
- }
-
-
- // result
-
- def result(
- progress_stdout: String => Unit = (_: String) => (),
- progress_stderr: String => Unit = (_: String) => (),
- progress_limit: Option[Long] = None,
- strict: Boolean = true): Process_Result =
- {
- stdin.close
-
- val limited = new Limited_Progress(this, progress_limit)
- val out_lines =
- Future.thread("bash_stdout") { File.read_lines(stdout, limited(progress_stdout)) }
- val err_lines =
- Future.thread("bash_stderr") { File.read_lines(stderr, limited(progress_stderr)) }
-
- val rc =
- try { join }
- catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code }
- if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
-
- Process_Result(rc, out_lines.join, err_lines.join, false, timing.value getOrElse Timing.zero)
- }
- }
-}
--- a/src/Pure/Concurrent/bash_windows.ML Thu Mar 10 19:15:06 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,99 +0,0 @@
-(* Title: Pure/Concurrent/bash_windows.ML
- Author: Makarius
-
-GNU bash processes, with propagation of interrupts -- Windows version.
-*)
-
-signature BASH =
-sig
- val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
-end;
-
-structure Bash: BASH =
-struct
-
-val process = uninterruptible (fn restore_attributes => fn script =>
- let
- datatype result = Wait | Signal | Result of int;
- val result = Synchronized.var "bash_result" Wait;
-
- val id = serial_string ();
- val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
- val out_path = File.tmp_path (Path.basic ("bash_out" ^ id));
- val err_path = File.tmp_path (Path.basic ("bash_err" ^ id));
- val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id));
-
- fun cleanup_files () =
- (try File.rm script_path;
- try File.rm out_path;
- try File.rm err_path;
- try File.rm pid_path);
- val _ = cleanup_files ();
-
- val system_thread =
- Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
- Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
- let
- val _ = File.write script_path script;
- val bash_script =
- "bash " ^ File.bash_path script_path ^
- " > " ^ File.bash_path out_path ^
- " 2> " ^ File.bash_path err_path;
- val bash_process = getenv_strict "ISABELLE_BASH_PROCESS";
- val rc =
- Windows.simpleExecute ("",
- quote (ML_System.platform_path bash_process) ^ " " ^
- quote (File.platform_path pid_path) ^ " \"\" bash -c " ^ quote bash_script)
- |> Windows.fromStatus |> SysWord.toInt;
- val res = if rc = 130 orelse rc = 512 then Signal else Result rc;
- in Synchronized.change result (K res) end
- handle exn =>
- (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn)));
-
- fun read_pid 0 = NONE
- | read_pid count =
- (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of
- NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1))
- | some => some);
-
- fun terminate NONE = ()
- | terminate (SOME pid) =
- let
- fun kill s =
- let
- val cmd = getenv_strict "CYGWIN_ROOT" ^ "\\bin\\bash.exe";
- val arg = "kill -" ^ s ^ " -" ^ string_of_int pid;
- in
- OS.Process.isSuccess (Windows.simpleExecute ("", quote cmd ^ " -c " ^ quote arg))
- handle OS.SysErr _ => false
- end;
-
- fun multi_kill count s =
- count = 0 orelse
- (kill s; kill "0") andalso
- (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s);
- val _ =
- multi_kill 10 "INT" andalso
- multi_kill 10 "TERM" andalso
- multi_kill 10 "KILL";
- in () end;
-
- fun cleanup () =
- (Standard_Thread.interrupt_unsynchronized system_thread;
- cleanup_files ());
- in
- let
- val _ =
- restore_attributes (fn () =>
- Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) ();
-
- val out = the_default "" (try File.read out_path);
- val err = the_default "" (try File.read err_path);
- val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
- val pid = read_pid 1;
- val _ = cleanup ();
- in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end
- handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn)
- end);
-
-end;
--- a/src/Pure/Concurrent/random.ML Thu Mar 10 19:15:06 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-(* Title: Pure/Concurrent/random.ML
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
-
-Pseudo random numbers.
-*)
-
-signature RANDOM =
-sig
- val random: unit -> real
- exception RANDOM
- val random_range: int -> int -> int
-end;
-
-structure Random: RANDOM =
-struct
-
-fun rmod x y = x - y * Real.realFloor (x / y);
-
-local
- val a = 16807.0;
- val m = 2147483647.0;
- val random_seed = Synchronized.var "random_seed" 1.0;
-in
-
-fun random () =
- Synchronized.change_result random_seed
- (fn r => let val r' = rmod (a * r) m in (r', r') end);
-
-end;
-
-exception RANDOM;
-
-fun random_range l h =
- if h < l orelse l < 0 then raise RANDOM
- else l + Real.floor (rmod (random ()) (real (h - l + 1)));
-
-end;
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/random.ML Thu Mar 10 22:49:24 2016 +0100
@@ -0,0 +1,38 @@
+(* Title: Pure/General/random.ML
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+
+Pseudo random numbers.
+*)
+
+signature RANDOM =
+sig
+ val random: unit -> real
+ exception RANDOM
+ val random_range: int -> int -> int
+end;
+
+structure Random: RANDOM =
+struct
+
+fun rmod x y = x - y * Real.realFloor (x / y);
+
+local
+ val a = 16807.0;
+ val m = 2147483647.0;
+ val random_seed = Synchronized.var "random_seed" 1.0;
+in
+
+fun random () =
+ Synchronized.change_result random_seed
+ (fn r => let val r' = rmod (a * r) m in (r', r') end);
+
+end;
+
+exception RANDOM;
+
+fun random_range l h =
+ if h < l orelse l < 0 then raise RANDOM
+ else l + Real.floor (rmod (random ()) (real (h - l + 1)));
+
+end;
+
--- a/src/Pure/General/timing.scala Thu Mar 10 19:15:06 2016 +0100
+++ b/src/Pure/General/timing.scala Thu Mar 10 22:49:24 2016 +0100
@@ -38,20 +38,24 @@
def + (t: Timing): Timing = Timing(elapsed + t.elapsed, cpu + t.cpu, gc + t.gc)
+ def message: String =
+ elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time"
+
+ def resources: Time = cpu + gc
def message_resources: String =
{
val resources = cpu + gc
val t1 = elapsed.seconds
val t2 = resources.seconds
val factor =
- if (t1 >= 5.0 && t2 >= 5.0)
+ if (t1 >= 3.0 && t2 >= 3.0)
String.format(Locale.ROOT, ", factor %.2f", new java.lang.Double(t2 / t1))
else ""
- elapsed.message_hms + " elapsed time, " + resources.message_hms + " cpu time" + factor
+ if (t2 >= 3.0)
+ elapsed.message_hms + " elapsed time, " + resources.message_hms + " cpu time" + factor
+ else
+ elapsed.message_hms + " elapsed time" + factor
}
- def message: String =
- elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time"
-
override def toString: String = message
}
--- a/src/Pure/ROOT Thu Mar 10 19:15:06 2016 +0100
+++ b/src/Pure/ROOT Thu Mar 10 22:49:24 2016 +0100
@@ -3,8 +3,6 @@
session Pure =
global_theories Pure
files
- "Concurrent/bash.ML"
- "Concurrent/bash_windows.ML"
"Concurrent/cache.ML"
"Concurrent/counter.ML"
"Concurrent/event_timer.ML"
@@ -14,7 +12,6 @@
"Concurrent/multithreading.ML"
"Concurrent/par_exn.ML"
"Concurrent/par_list.ML"
- "Concurrent/random.ML"
"Concurrent/single_assignment.ML"
"Concurrent/standard_thread.ML"
"Concurrent/synchronized.ML"
@@ -47,6 +44,7 @@
"General/print_mode.ML"
"General/properties.ML"
"General/queue.ML"
+ "General/random.ML"
"General/same.ML"
"General/scan.ML"
"General/secure.ML"
@@ -153,6 +151,8 @@
"Syntax/syntax_trans.ML"
"Syntax/term_position.ML"
"Syntax/type_annotation.ML"
+ "System/bash.ML"
+ "System/bash_windows.ML"
"System/command_line.ML"
"System/invoke_scala.ML"
"System/isabelle_process.ML"
--- a/src/Pure/ROOT.ML Thu Mar 10 19:15:06 2016 +0100
+++ b/src/Pure/ROOT.ML Thu Mar 10 22:49:24 2016 +0100
@@ -107,8 +107,8 @@
use "Concurrent/synchronized.ML";
use "Concurrent/counter.ML";
-use "Concurrent/random.ML";
+use "General/random.ML";
use "General/properties.ML";
use "General/output.ML";
use "PIDE/markup.ML";
@@ -193,10 +193,6 @@
use "Concurrent/standard_thread.ML";
use "Concurrent/single_assignment.ML";
-if ML_System.platform_is_windows
-then use "Concurrent/bash_windows.ML"
-else use "Concurrent/bash.ML";
-
use "Concurrent/par_exn.ML";
use "Concurrent/task_queue.ML";
use "Concurrent/future.ML";
@@ -371,8 +367,13 @@
use "Proof/proof_checker.ML";
use "Proof/extraction.ML";
+(*Isabelle system*)
+if ML_System.platform_is_windows
+then use "System/bash_windows.ML"
+else use "System/bash.ML";
+use "System/isabelle_system.ML";
+
(*theory documents*)
-use "System/isabelle_system.ML";
use "Thy/term_style.ML";
use "Isar/outer_syntax.ML";
use "Thy/thy_output.ML";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/bash.ML Thu Mar 10 22:49:24 2016 +0100
@@ -0,0 +1,102 @@
+(* Title: Pure/System/bash.ML
+ Author: Makarius
+
+GNU bash processes, with propagation of interrupts -- POSIX version.
+*)
+
+signature BASH =
+sig
+ val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
+end;
+
+structure Bash: BASH =
+struct
+
+val process = uninterruptible (fn restore_attributes => fn script =>
+ let
+ datatype result = Wait | Signal | Result of int;
+ val result = Synchronized.var "bash_result" Wait;
+
+ val id = serial_string ();
+ val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
+ val out_path = File.tmp_path (Path.basic ("bash_out" ^ id));
+ val err_path = File.tmp_path (Path.basic ("bash_err" ^ id));
+ val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id));
+
+ fun cleanup_files () =
+ (try File.rm script_path;
+ try File.rm out_path;
+ try File.rm err_path;
+ try File.rm pid_path);
+ val _ = cleanup_files ();
+
+ val system_thread =
+ Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
+ Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
+ let
+ val _ = File.write script_path script;
+ val _ = getenv_strict "ISABELLE_BASH_PROCESS";
+ val status =
+ OS.Process.system
+ ("exec \"$ISABELLE_BASH_PROCESS\" " ^ File.bash_path pid_path ^ " \"\"" ^
+ " bash " ^ File.bash_path script_path ^
+ " > " ^ File.bash_path out_path ^
+ " 2> " ^ File.bash_path err_path);
+ val res =
+ (case Posix.Process.fromStatus status of
+ Posix.Process.W_EXITED => Result 0
+ | Posix.Process.W_EXITSTATUS 0wx82 => Signal
+ | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w)
+ | Posix.Process.W_SIGNALED s =>
+ if s = Posix.Signal.int then Signal
+ else Result (256 + LargeWord.toInt (Posix.Signal.toWord s))
+ | Posix.Process.W_STOPPED s =>
+ Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
+ in Synchronized.change result (K res) end
+ handle exn =>
+ (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn)));
+
+ fun read_pid 0 = NONE
+ | read_pid count =
+ (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of
+ NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1))
+ | some => some);
+
+ fun terminate NONE = ()
+ | terminate (SOME pid) =
+ let
+ fun kill s =
+ (Posix.Process.kill
+ (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)), s); true)
+ handle OS.SysErr _ => false;
+
+ fun multi_kill count s =
+ count = 0 orelse
+ (kill s; kill (Posix.Signal.fromWord 0w0)) andalso
+ (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s);
+ val _ =
+ multi_kill 10 Posix.Signal.int andalso
+ multi_kill 10 Posix.Signal.term andalso
+ multi_kill 10 Posix.Signal.kill;
+ in () end;
+
+ fun cleanup () =
+ (Standard_Thread.interrupt_unsynchronized system_thread;
+ cleanup_files ());
+ in
+ let
+ val _ =
+ restore_attributes (fn () =>
+ Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) ();
+
+ val out = the_default "" (try File.read out_path);
+ val err = the_default "" (try File.read err_path);
+ val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
+ val pid = read_pid 1;
+ val _ = cleanup ();
+ in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end
+ handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn)
+ end);
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/bash.scala Thu Mar 10 22:49:24 2016 +0100
@@ -0,0 +1,168 @@
+/* Title: Pure/System/bash.scala
+ Author: Makarius
+
+GNU bash processes, with propagation of interrupts.
+*/
+
+package isabelle
+
+
+import java.io.{File => JFile, BufferedReader, InputStreamReader,
+ BufferedWriter, OutputStreamWriter}
+
+
+object Bash
+{
+ private class Limited_Progress(proc: Process, progress_limit: Option[Long])
+ {
+ private var count = 0L
+ def apply(progress: String => Unit)(line: String): Unit = synchronized {
+ progress(line)
+ count = count + line.length + 1
+ progress_limit match {
+ case Some(limit) if count > limit => proc.terminate
+ case _ =>
+ }
+ }
+ }
+
+ def process(script: String,
+ cwd: JFile = null,
+ env: Map[String, String] = Map.empty,
+ redirect: Boolean = false): Process =
+ new Process(script, cwd, env, redirect)
+
+ class Process private [Bash](
+ script: String, cwd: JFile, env: Map[String, String], redirect: Boolean)
+ extends Prover.System_Process
+ {
+ private val timing_file = Isabelle_System.tmp_file("bash_script")
+ private val timing = Synchronized[Option[Timing]](None)
+
+ private val script_file = Isabelle_System.tmp_file("bash_script")
+ File.write(script_file, script)
+
+ private val proc =
+ Isabelle_System.process(cwd, Isabelle_System.settings(env), redirect,
+ File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-",
+ File.standard_path(timing_file), "bash", File.standard_path(script_file))
+
+
+ // channels
+
+ val stdin: BufferedWriter =
+ new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, UTF8.charset))
+
+ val stdout: BufferedReader =
+ new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset))
+
+ val stderr: BufferedReader =
+ new BufferedReader(new InputStreamReader(proc.getErrorStream, UTF8.charset))
+
+
+ // signals
+
+ private val pid = stdout.readLine
+
+ def interrupt()
+ { Exn.Interrupt.postpone { Isabelle_System.kill("INT", pid) } }
+
+ private def kill(signal: String): Boolean =
+ Exn.Interrupt.postpone {
+ Isabelle_System.kill(signal, pid)
+ Isabelle_System.kill("0", pid)._2 == 0 } getOrElse true
+
+ private def multi_kill(signal: String): Boolean =
+ {
+ var running = true
+ var count = 10
+ while (running && count > 0) {
+ if (kill(signal)) {
+ Exn.Interrupt.postpone {
+ Thread.sleep(100)
+ count -= 1
+ }
+ }
+ else running = false
+ }
+ running
+ }
+
+ def terminate()
+ {
+ multi_kill("INT") && multi_kill("TERM") && kill("KILL")
+ proc.destroy
+ cleanup()
+ }
+
+
+ // JVM shutdown hook
+
+ private val shutdown_hook = new Thread { override def run = terminate() }
+
+ try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
+ catch { case _: IllegalStateException => }
+
+
+ // cleanup
+
+ private def cleanup()
+ {
+ try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
+ catch { case _: IllegalStateException => }
+
+ script_file.delete
+
+ timing.change {
+ case None =>
+ if (timing_file.isFile) {
+ val t =
+ Word.explode(File.read(timing_file)) match {
+ case List(Properties.Value.Long(elapsed), Properties.Value.Long(cpu)) =>
+ Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero)
+ case _ => Timing.zero
+ }
+ timing_file.delete
+ Some(t)
+ }
+ else Some(Timing.zero)
+ case some => some
+ }
+ }
+
+
+ // join
+
+ def join: Int =
+ {
+ val rc = proc.waitFor
+ cleanup()
+ rc
+ }
+
+
+ // result
+
+ def result(
+ progress_stdout: String => Unit = (_: String) => (),
+ progress_stderr: String => Unit = (_: String) => (),
+ progress_limit: Option[Long] = None,
+ strict: Boolean = true): Process_Result =
+ {
+ stdin.close
+
+ val limited = new Limited_Progress(this, progress_limit)
+ val out_lines =
+ Future.thread("bash_stdout") { File.read_lines(stdout, limited(progress_stdout)) }
+ val err_lines =
+ Future.thread("bash_stderr") { File.read_lines(stderr, limited(progress_stderr)) }
+
+ val rc =
+ try { join }
+ catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code }
+ if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
+
+ Process_Result(rc, out_lines.join, err_lines.join, false, timing.value getOrElse Timing.zero)
+ }
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/bash_windows.ML Thu Mar 10 22:49:24 2016 +0100
@@ -0,0 +1,99 @@
+(* Title: Pure/Concurrent/bash_windows.ML
+ Author: Makarius
+
+GNU bash processes, with propagation of interrupts -- Windows version.
+*)
+
+signature BASH =
+sig
+ val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
+end;
+
+structure Bash: BASH =
+struct
+
+val process = uninterruptible (fn restore_attributes => fn script =>
+ let
+ datatype result = Wait | Signal | Result of int;
+ val result = Synchronized.var "bash_result" Wait;
+
+ val id = serial_string ();
+ val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
+ val out_path = File.tmp_path (Path.basic ("bash_out" ^ id));
+ val err_path = File.tmp_path (Path.basic ("bash_err" ^ id));
+ val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id));
+
+ fun cleanup_files () =
+ (try File.rm script_path;
+ try File.rm out_path;
+ try File.rm err_path;
+ try File.rm pid_path);
+ val _ = cleanup_files ();
+
+ val system_thread =
+ Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
+ Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
+ let
+ val _ = File.write script_path script;
+ val bash_script =
+ "bash " ^ File.bash_path script_path ^
+ " > " ^ File.bash_path out_path ^
+ " 2> " ^ File.bash_path err_path;
+ val bash_process = getenv_strict "ISABELLE_BASH_PROCESS";
+ val rc =
+ Windows.simpleExecute ("",
+ quote (ML_System.platform_path bash_process) ^ " " ^
+ quote (File.platform_path pid_path) ^ " \"\" bash -c " ^ quote bash_script)
+ |> Windows.fromStatus |> SysWord.toInt;
+ val res = if rc = 130 orelse rc = 512 then Signal else Result rc;
+ in Synchronized.change result (K res) end
+ handle exn =>
+ (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn)));
+
+ fun read_pid 0 = NONE
+ | read_pid count =
+ (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of
+ NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1))
+ | some => some);
+
+ fun terminate NONE = ()
+ | terminate (SOME pid) =
+ let
+ fun kill s =
+ let
+ val cmd = getenv_strict "CYGWIN_ROOT" ^ "\\bin\\bash.exe";
+ val arg = "kill -" ^ s ^ " -" ^ string_of_int pid;
+ in
+ OS.Process.isSuccess (Windows.simpleExecute ("", quote cmd ^ " -c " ^ quote arg))
+ handle OS.SysErr _ => false
+ end;
+
+ fun multi_kill count s =
+ count = 0 orelse
+ (kill s; kill "0") andalso
+ (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s);
+ val _ =
+ multi_kill 10 "INT" andalso
+ multi_kill 10 "TERM" andalso
+ multi_kill 10 "KILL";
+ in () end;
+
+ fun cleanup () =
+ (Standard_Thread.interrupt_unsynchronized system_thread;
+ cleanup_files ());
+ in
+ let
+ val _ =
+ restore_attributes (fn () =>
+ Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) ();
+
+ val out = the_default "" (try File.read out_path);
+ val err = the_default "" (try File.read err_path);
+ val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
+ val pid = read_pid 1;
+ val _ = cleanup ();
+ in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end
+ handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn)
+ end);
+
+end;
--- a/src/Pure/System/isabelle_process.scala Thu Mar 10 19:15:06 2016 +0100
+++ b/src/Pure/System/isabelle_process.scala Thu Mar 10 22:49:24 2016 +0100
@@ -28,46 +28,6 @@
new Isabelle_Process(receiver, channel, process)
}
-
-
- /* command line entry point */
-
- def main(args: Array[String])
- {
- Command_Line.tool {
- var eval_args: List[String] = Nil
- var modes: List[String] = Nil
- var options = Options.init()
-
- val getopts = Getopts("""
-Usage: isabelle_process [OPTIONS] [HEAP]
-
- Options are:
- -e ML_EXPR evaluate ML expression on startup
- -f ML_FILE evaluate ML file on startup
- -m MODE add print mode for output
- -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-
- If HEAP is a plain name (default $ISABELLE_LOGIC), it is searched in
- $ISABELLE_PATH; if it contains a slash, it is taken as literal file;
- if it is RAW_ML_SYSTEM, the initial ML heap is used.
-""",
- "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
- "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
- "m:" -> (arg => modes = arg :: modes),
- "o:" -> (arg => options = options + arg))
-
- val heap =
- getopts(args) match {
- case Nil => ""
- case List(heap) => heap
- case _ => getopts.usage()
- }
-
- ML_Process(options, heap = heap, args = eval_args ::: args.toList, modes = modes).
- result().print_stdout.rc
- }
- }
}
class Isabelle_Process private(
--- a/src/Pure/System/ml_process.scala Thu Mar 10 19:15:06 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,115 +0,0 @@
-/* Title: Pure/System/ml_process.scala
- Author: Makarius
-
-The underlying ML process.
-*/
-
-package isabelle
-
-
-import java.io.{File => JFile}
-
-
-object ML_Process
-{
- def apply(options: Options,
- heap: String = "",
- args: List[String] = Nil,
- modes: List[String] = Nil,
- secure: Boolean = false,
- cwd: JFile = null,
- env: Map[String, String] = Map.empty,
- redirect: Boolean = false,
- channel: Option[System_Channel] = None): Bash.Process =
- {
- val load_heaps =
- {
- if (heap == "RAW_ML_SYSTEM") Nil
- else if (heap.iterator.contains('/')) {
- val heap_path = Path.explode(heap)
- if (!heap_path.is_file) error("Bad heap file: " + heap_path)
- List(heap_path)
- }
- else {
- val dirs = Isabelle_System.find_logics_dirs()
- val heap_name = if (heap == "") Isabelle_System.getenv_strict("ISABELLE_LOGIC") else heap
- dirs.map(_ + Path.basic(heap_name)).find(_.is_file) match {
- case Some(heap_path) => List(heap_path)
- case None =>
- error("Unknown logic " + quote(heap) + " -- no heap file found in:\n" +
- cat_lines(dirs.map(dir => " " + dir.implode)))
- }
- }
- }
-
- val eval_heaps =
- load_heaps.map(load_heap =>
- "(PolyML.SaveState.loadState " + ML_Syntax.print_string_raw(File.platform_path(load_heap)) +
- "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " +
- ML_Syntax.print_string_raw(": " + load_heap.toString + "\n") +
- "); OS.Process.exit OS.Process.failure)")
-
- val eval_initial =
- if (load_heaps.isEmpty) {
- List(
- if (Platform.is_windows)
- "fun exit 0 = OS.Process.exit OS.Process.success" +
- " | exit 1 = OS.Process.exit OS.Process.failure" +
- " | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))"
- else
- "fun exit rc = Posix.Process.exit (Word8.fromInt rc)",
- "PolyML.Compiler.prompt1 := \"ML> \"",
- "PolyML.Compiler.prompt2 := \"ML# \"")
- }
- else Nil
-
- val eval_modes =
- if (modes.isEmpty) Nil
- else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string_raw _)(modes))
-
- // options
- val isabelle_process_options = Isabelle_System.tmp_file("options")
- File.write(isabelle_process_options, YXML.string_of_body(options.encode))
- val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
- val eval_options = if (load_heaps.isEmpty) Nil else List("Options.load_default ()")
-
- val eval_secure = if (secure) List("Secure.set_secure ()") else Nil
-
- val eval_process =
- if (load_heaps.isEmpty)
- List("PolyML.print_depth 10")
- else
- channel match {
- case None =>
- List("(default_print_depth 10; Isabelle_Process.init_options ())")
- case Some(ch) =>
- List("(default_print_depth 10; Isabelle_Process.init_protocol " +
- ML_Syntax.print_string_raw(ch.server_name) + ")")
- }
-
- // bash
- val bash_args =
- Word.explode(Isabelle_System.getenv("ML_OPTIONS")) :::
- (eval_heaps ::: eval_initial ::: eval_modes ::: eval_options ::: eval_secure ::: eval_process).
- map(eval => List("--eval", eval)).flatten ::: args
-
- Bash.process(
- """
- [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
-
- export ISABELLE_PID="$$"
- export ISABELLE_TMP="$ISABELLE_TMP_PREFIX$ISABELLE_PID"
- mkdir -p "$ISABELLE_TMP"
- chmod $(umask -S) "$ISABELLE_TMP"
-
- librarypath "$ML_HOME"
- "$ML_HOME/poly" -q """ + File.bash_args(bash_args) + """
- RC="$?"
-
- rm -f "$ISABELLE_PROCESS_OPTIONS"
- rmdir "$ISABELLE_TMP"
-
- exit "$RC"
- """, cwd = cwd, env = env ++ env_options, redirect = redirect)
- }
-}
--- a/src/Pure/Thy/present.ML Thu Mar 10 19:15:06 2016 +0100
+++ b/src/Pure/Thy/present.ML Thu Mar 10 22:49:24 2016 +0100
@@ -215,7 +215,7 @@
fun isabelle_document {verbose, purge} format name tags dir =
let
- val s = "\"$ISABELLE_TOOL\" document" ^ (if purge then " -c" else "") ^ " -o '" ^ format ^ "' \
+ val s = "isabelle document" ^ (if purge then " -c" else "") ^ " -o '" ^ format ^ "' \
\-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.bash_path dir ^ " 2>&1";
val doc_path = Path.appends [dir, Path.parent, Path.basic name |> Path.ext format];
val _ = if verbose then writeln s else ();
--- a/src/Pure/Tools/build.scala Thu Mar 10 19:15:06 2016 +0100
+++ b/src/Pure/Tools/build.scala Thu Mar 10 22:49:24 2016 +0100
@@ -1027,29 +1027,113 @@
def main(args: Array[String])
{
Command_Line.tool {
- args.toList match {
- case
- Properties.Value.Boolean(requirements) ::
- Properties.Value.Boolean(all_sessions) ::
- Properties.Value.Boolean(build_heap) ::
- Properties.Value.Boolean(clean_build) ::
- Properties.Value.Int(max_jobs) ::
- Properties.Value.Boolean(list_files) ::
- Properties.Value.Boolean(no_build) ::
- Properties.Value.Boolean(system_mode) ::
- Properties.Value.Boolean(verbose) ::
- Command_Line.Chunks(dirs, select_dirs, session_groups, check_keywords,
- build_options, exclude_session_groups, exclude_sessions, sessions) =>
- val options = (Options.init() /: build_options)(_ + _)
- val progress = new Console_Progress(verbose)
- progress.interrupt_handler {
- build(options, progress, requirements, all_sessions, build_heap, clean_build,
- dirs.map(Path.explode(_)), select_dirs.map(Path.explode(_)), exclude_session_groups,
- session_groups, max_jobs, list_files, check_keywords.toSet, no_build, system_mode,
- verbose, exclude_sessions, sessions)
- }
- case _ => error("Bad arguments:\n" + cat_lines(args))
+ def show_settings(): String =
+ cat_lines(List(
+ "ISABELLE_BUILD_OPTIONS=" +
+ quote(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")),
+ "",
+ "ISABELLE_BUILD_JAVA_OPTIONS=" +
+ quote(Isabelle_System.getenv("ISABELLE_BUILD_JAVA_OPTIONS")) +
+ "",
+ "ML_PLATFORM=" + quote(Isabelle_System.getenv("ML_PLATFORM")),
+ "ML_HOME=" + quote(Isabelle_System.getenv("ML_HOME")),
+ "ML_SYSTEM=" + quote(Isabelle_System.getenv("ML_SYSTEM")),
+ "ML_OPTIONS=" + quote(Isabelle_System.getenv("ML_OPTIONS"))))
+
+ val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
+
+ var select_dirs: List[Path] = Nil
+ var requirements = false
+ var exclude_session_groups: List[String] = Nil
+ var all_sessions = false
+ var build_heap = false
+ var clean_build = false
+ var dirs: List[Path] = Nil
+ var session_groups: List[String] = Nil
+ var max_jobs = 1
+ var check_keywords: Set[String] = Set.empty
+ var list_files = false
+ var no_build = false
+ var options = (Options.init() /: build_options)(_ + _)
+ var system_mode = false
+ var verbose = false
+ var exclude_sessions: List[String] = Nil
+
+ val getopts = Getopts("""
+Usage: isabelle build [OPTIONS] [SESSIONS ...]
+
+ Options are:
+ -D DIR include session directory and select its sessions
+ -R operate on requirements of selected sessions
+ -X NAME exclude sessions from group NAME and all descendants
+ -a select all sessions
+ -b build heap images
+ -c clean build
+ -d DIR include session directory
+ -g NAME select session group NAME
+ -j INT maximum number of parallel jobs (default 1)
+ -k KEYWORD check theory sources for conflicts with proposed keywords
+ -l list session source files
+ -n no build -- test dependencies only
+ -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
+ -s system build mode: produce output in ISABELLE_HOME
+ -v verbose
+ -x NAME exclude session NAME and all descendants
+
+ Build and manage Isabelle sessions, depending on implicit
+""" + Library.prefix_lines(" ", show_settings()),
+ "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
+ "R" -> (_ => requirements = true),
+ "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
+ "a" -> (_ => all_sessions = true),
+ "b" -> (_ => build_heap = true),
+ "c" -> (_ => clean_build = true),
+ "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+ "g:" -> (arg => session_groups = session_groups ::: List(arg)),
+ "j:" -> (arg => max_jobs = Properties.Value.Int.parse(arg)),
+ "k:" -> (arg => check_keywords = check_keywords + arg),
+ "l" -> (_ => list_files = true),
+ "n" -> (_ => no_build = true),
+ "o:" -> (arg => options = options + arg),
+ "s" -> (_ => system_mode = true),
+ "v" -> (_ => verbose = true),
+ "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
+
+ val sessions = getopts(args)
+
+ val progress = new Console_Progress(verbose)
+ val start_time = Time.now()
+ val show_timing = !no_build && verbose
+
+ if (show_timing) {
+ progress.echo(
+ Library.trim_line(
+ Isabelle_System.bash(
+ """echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))" """).out))
+ progress.echo(show_settings())
}
+
+ val results =
+ progress.interrupt_handler {
+ build_results(options, progress, requirements, all_sessions, build_heap, clean_build,
+ dirs, select_dirs, exclude_session_groups, session_groups, max_jobs, list_files,
+ check_keywords, no_build, system_mode, verbose, exclude_sessions, sessions)
+ }
+
+ if (show_timing) {
+ val elapsed_time = Time.now() - start_time
+
+ progress.echo(
+ Library.trim_line(
+ Isabelle_System.bash("""echo "Finished at "; date""").out))
+
+ val total_timing =
+ (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _).
+ copy(elapsed = elapsed_time)
+ progress.echo(total_timing.message_resources)
+ }
+
+ results.rc
}
}
--- a/src/Pure/Tools/ml_console.scala Thu Mar 10 19:15:06 2016 +0100
+++ b/src/Pure/Tools/ml_console.scala Thu Mar 10 22:49:24 2016 +0100
@@ -1,7 +1,7 @@
/* Title: Pure/Tools/ml_console.scala
Author: Makarius
-Run Isabelle process with raw ML console and line editor.
+The raw ML process in interactive mode.
*/
package isabelle
@@ -33,11 +33,12 @@
-m MODE add print mode for output
-n no build of session image on startup
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- -r logic session is RAW_ML_SYSTEM
+ -r logic session is "RAW_ML_SYSTEM"
-s system build mode for session image
- Run Isabelle process with raw ML console and line editor
- (ISABELLE_LINE_EDITOR=""" + quote(Isabelle_System.getenv("ISABELLE_LINE_EDITOR")) + """.
+ Build a logic session image and run the raw Isabelle ML process
+ in interactive mode, with line editor ISABELLE_LINE_EDITOR=""" +
+ quote(Isabelle_System.getenv("ISABELLE_LINE_EDITOR")) + """.
""",
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
"l:" -> (arg => logic = arg),
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/ml_process.scala Thu Mar 10 22:49:24 2016 +0100
@@ -0,0 +1,159 @@
+/* Title: Pure/Tools/ml_process.scala
+ Author: Makarius
+
+The raw ML process.
+*/
+
+package isabelle
+
+
+import java.io.{File => JFile}
+
+
+object ML_Process
+{
+ def apply(options: Options,
+ heap: String = "",
+ args: List[String] = Nil,
+ modes: List[String] = Nil,
+ secure: Boolean = false,
+ cwd: JFile = null,
+ env: Map[String, String] = Map.empty,
+ redirect: Boolean = false,
+ channel: Option[System_Channel] = None): Bash.Process =
+ {
+ val load_heaps =
+ {
+ if (heap == "RAW_ML_SYSTEM") Nil
+ else if (heap.iterator.contains('/')) {
+ val heap_path = Path.explode(heap)
+ if (!heap_path.is_file) error("Bad heap file: " + heap_path)
+ List(heap_path)
+ }
+ else {
+ val dirs = Isabelle_System.find_logics_dirs()
+ val heap_name = if (heap == "") Isabelle_System.getenv_strict("ISABELLE_LOGIC") else heap
+ dirs.map(_ + Path.basic(heap_name)).find(_.is_file) match {
+ case Some(heap_path) => List(heap_path)
+ case None =>
+ error("Unknown logic " + quote(heap_name) + " -- no heap file found in:\n" +
+ cat_lines(dirs.map(dir => " " + dir.implode)))
+ }
+ }
+ }
+
+ val eval_heaps =
+ load_heaps.map(load_heap =>
+ "(PolyML.SaveState.loadState " + ML_Syntax.print_string_raw(File.platform_path(load_heap)) +
+ "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " +
+ ML_Syntax.print_string_raw(": " + load_heap.toString + "\n") +
+ "); OS.Process.exit OS.Process.failure)")
+
+ val eval_initial =
+ if (load_heaps.isEmpty) {
+ List(
+ if (Platform.is_windows)
+ "fun exit 0 = OS.Process.exit OS.Process.success" +
+ " | exit 1 = OS.Process.exit OS.Process.failure" +
+ " | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))"
+ else
+ "fun exit rc = Posix.Process.exit (Word8.fromInt rc)",
+ "PolyML.Compiler.prompt1 := \"ML> \"",
+ "PolyML.Compiler.prompt2 := \"ML# \"")
+ }
+ else Nil
+
+ val eval_modes =
+ if (modes.isEmpty) Nil
+ else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string_raw _)(modes))
+
+ // options
+ val isabelle_process_options = Isabelle_System.tmp_file("options")
+ File.write(isabelle_process_options, YXML.string_of_body(options.encode))
+ val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
+ val eval_options = if (load_heaps.isEmpty) Nil else List("Options.load_default ()")
+
+ val eval_secure = if (secure) List("Secure.set_secure ()") else Nil
+
+ val eval_process =
+ if (load_heaps.isEmpty)
+ List("PolyML.print_depth 10")
+ else
+ channel match {
+ case None =>
+ List("(default_print_depth 10; Isabelle_Process.init_options ())")
+ case Some(ch) =>
+ List("(default_print_depth 10; Isabelle_Process.init_protocol " +
+ ML_Syntax.print_string_raw(ch.server_name) + ")")
+ }
+
+ // bash
+ val bash_args =
+ Word.explode(Isabelle_System.getenv("ML_OPTIONS")) :::
+ (eval_heaps ::: eval_initial ::: eval_modes ::: eval_options ::: eval_secure ::: eval_process).
+ map(eval => List("--eval", eval)).flatten ::: args
+
+ Bash.process(
+ """
+ [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
+
+ export ISABELLE_PID="$$"
+ export ISABELLE_TMP="$ISABELLE_TMP_PREFIX$ISABELLE_PID"
+ mkdir -p "$ISABELLE_TMP"
+ chmod $(umask -S) "$ISABELLE_TMP"
+
+ librarypath "$ML_HOME"
+ "$ML_HOME/poly" -q """ + File.bash_args(bash_args) + """
+ RC="$?"
+
+ rm -f "$ISABELLE_PROCESS_OPTIONS"
+ rmdir "$ISABELLE_TMP"
+
+ exit "$RC"
+ """, cwd = cwd, env = env ++ env_options, redirect = redirect)
+ }
+
+
+ /* command line entry point */
+
+ def main(args: Array[String])
+ {
+ Command_Line.tool {
+ var eval_args: List[String] = Nil
+ var modes: List[String] = Nil
+ var options = Options.init()
+
+ val getopts = Getopts("""
+Usage: isabelle process [OPTIONS] [HEAP]
+
+ Options are:
+ -e ML_EXPR evaluate ML expression on startup
+ -f ML_FILE evaluate ML file on startup
+ -m MODE add print mode for output
+ -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
+
+ Run the raw Isabelle ML process in batch mode, using a given heap image.
+
+ If HEAP is a plain name (default ISABELLE_LOGIC=""" +
+ quote(Isabelle_System.getenv("ISABELLE_LOGIC")) + """), it is searched in
+ ISABELLE_PATH; if it contains a slash, it is taken as literal file;
+ if it is "RAW_ML_SYSTEM", the initial ML heap is used.
+""",
+ "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
+ "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
+ "m:" -> (arg => modes = arg :: modes),
+ "o:" -> (arg => options = options + arg))
+
+ if (args.isEmpty) getopts.usage()
+ val heap =
+ getopts(args) match {
+ case Nil => ""
+ case List(heap) => heap
+ case _ => getopts.usage()
+ }
+
+ ML_Process(options, heap = heap, args = eval_args ::: args.toList, modes = modes).
+ result().print_stdout.rc
+ }
+ }
+}
--- a/src/Pure/build-jars Thu Mar 10 19:15:06 2016 +0100
+++ b/src/Pure/build-jars Thu Mar 10 22:49:24 2016 +0100
@@ -9,7 +9,6 @@
## sources
declare -a SOURCES=(
- Concurrent/bash.scala
Concurrent/consumer_thread.scala
Concurrent/counter.scala
Concurrent/event_timer.scala
@@ -74,6 +73,7 @@
PIDE/xml.scala
PIDE/yxml.scala
ROOT.scala
+ System/bash.scala
System/command_line.scala
System/cygwin.scala
System/getopts.scala
@@ -81,7 +81,6 @@
System/isabelle_charset.scala
System/isabelle_process.scala
System/isabelle_system.scala
- System/ml_process.scala
System/options.scala
System/platform.scala
System/posix_interrupt.scala
@@ -103,6 +102,7 @@
Tools/doc.scala
Tools/main.scala
Tools/ml_console.scala
+ Tools/ml_process.scala
Tools/ml_statistics.scala
Tools/news.scala
Tools/print_operation.scala
--- a/src/Pure/library.scala Thu Mar 10 19:15:06 2016 +0100
+++ b/src/Pure/library.scala Thu Mar 10 22:49:24 2016 +0100
@@ -97,6 +97,10 @@
def split_lines(str: String): List[String] = space_explode('\n', str)
+ def prefix_lines(prfx: String, str: String): String =
+ if (str == "") str
+ else cat_lines(split_lines(str).map(s => prfx + s))
+
def first_line(source: CharSequence): String =
{
val lines = separated_chunks(_ == '\n', source)
--- a/src/Tools/Code/code_ml.ML Thu Mar 10 19:15:06 2016 +0100
+++ b/src/Tools/Code/code_ml.ML Thu Mar 10 22:49:24 2016 +0100
@@ -868,10 +868,10 @@
val _ = Theory.setup
(Code_Target.add_language
(target_SML, { serializer = serializer_sml, literals = literals_sml,
- check = { env_var = "ISABELLE_PROCESS",
+ check = { env_var = "ISABELLE_TOOL",
make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
make_command = fn _ =>
- "\"$ISABELLE_PROCESS\" -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' Pure" } })
+ "\"$ISABELLE_TOOL\" process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' Pure" } })
#> Code_Target.add_language
(target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
check = { env_var = "ISABELLE_OCAML",
--- a/src/Tools/jEdit/lib/Tools/jedit Thu Mar 10 19:15:06 2016 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Thu Mar 10 22:49:24 2016 +0100
@@ -209,7 +209,7 @@
## dependencies
if [ -e "$ISABELLE_HOME/Admin/build" ]; then
- "$ISABELLE_TOOL" browser -b || exit $?
+ isabelle browser -b || exit $?
"$ISABELLE_HOME/Admin/build" "$BUILD_JARS" || exit $?
fi
@@ -361,5 +361,5 @@
then
export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_PRINT_MODE JEDIT_BUILD_MODE
classpath "$JEDIT_HOME/dist/jedit.jar"
- exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}"
+ exec isabelle java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}"
fi
--- a/src/Tools/jEdit/lib/Tools/jedit_client Thu Mar 10 19:15:06 2016 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit_client Thu Mar 10 22:49:24 2016 +0100
@@ -104,11 +104,11 @@
exit
fi
-"$ISABELLE_TOOL" jedit -b || exit $?
+isabelle jedit -b || exit $?
if [ -f "$JEDIT_SETTINGS/$SERVER_NAME" ]
then
- exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" \
+ exec isabelle java "${JAVA_ARGS[@]}" \
-jar $(platform_path "$JEDIT_HOME/dist/jedit.jar") \
"-settings=$(platform_path "$JEDIT_SETTINGS")" \
-server="$SERVER_NAME" -reuseview "${ARGS[@]}"
--- a/src/Tools/jEdit/src/active.scala Thu Mar 10 19:15:06 2016 +0100
+++ b/src/Tools/jEdit/src/active.scala Thu Mar 10 22:49:24 2016 +0100
@@ -33,7 +33,7 @@
Standard_Thread.fork("browser") {
val graph_file = Isabelle_System.tmp_file("graph")
File.write(graph_file, XML.content(body))
- Isabelle_System.bash("\"$ISABELLE_TOOL\" browser -c \"$GRAPH_FILE\" &",
+ Isabelle_System.bash("isabelle browser -c \"$GRAPH_FILE\" &",
env = Map("GRAPH_FILE" -> File.standard_path(graph_file)))
}