# HG changeset patch # User wenzelm # Date 1457646564 -3600 # Node ID adffc55a682d916cf32b7854d7fd928cca3f7b9e # Parent 8c7301325f9f26efaadf5c1ca002166ccfee0105# Parent 4832491d137619828b072f8938597285b2c3fe37 merged diff -r 8c7301325f9f -r adffc55a682d Admin/lib/Tools/build_doc --- 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 "$@" diff -r 8c7301325f9f -r adffc55a682d Admin/lib/Tools/check_sources --- 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 "$@" diff -r 8c7301325f9f -r adffc55a682d NEWS --- 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) ----------------------------------- diff -r 8c7301325f9f -r adffc55a682d bin/isabelle_process --- 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 "$@" diff -r 8c7301325f9f -r adffc55a682d lib/Tools/browser --- 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 diff -r 8c7301325f9f -r adffc55a682d lib/Tools/build --- 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 "$@" diff -r 8c7301325f9f -r adffc55a682d lib/Tools/console --- 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 diff -r 8c7301325f9f -r adffc55a682d lib/Tools/doc --- 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 "$@" diff -r 8c7301325f9f -r adffc55a682d lib/Tools/document --- 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 diff -r 8c7301325f9f -r adffc55a682d lib/Tools/install --- 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" diff -r 8c7301325f9f -r adffc55a682d lib/Tools/options --- 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 "$@" diff -r 8c7301325f9f -r adffc55a682d lib/Tools/process --- /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 "$@" diff -r 8c7301325f9f -r adffc55a682d lib/Tools/update_cartouches --- 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 "$@" diff -r 8c7301325f9f -r adffc55a682d lib/Tools/update_header --- 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 "$@" diff -r 8c7301325f9f -r adffc55a682d lib/Tools/update_then --- 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 "$@" diff -r 8c7301325f9f -r adffc55a682d lib/Tools/update_theorems --- 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 "$@" diff -r 8c7301325f9f -r adffc55a682d lib/scripts/getsettings --- 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" diff -r 8c7301325f9f -r adffc55a682d src/Doc/Classes/document/build --- 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" diff -r 8c7301325f9f -r adffc55a682d src/Doc/Codegen/document/build --- 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 diff -r 8c7301325f9f -r adffc55a682d src/Doc/Eisbach/document/build --- 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" diff -r 8c7301325f9f -r adffc55a682d src/Doc/Implementation/document/build --- 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" diff -r 8c7301325f9f -r adffc55a682d src/Doc/Intro/document/build --- 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" diff -r 8c7301325f9f -r adffc55a682d src/Doc/Isar_Ref/document/build --- 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" diff -r 8c7301325f9f -r adffc55a682d src/Doc/JEdit/document/build --- 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" diff -r 8c7301325f9f -r adffc55a682d src/Doc/Logics/document/build --- 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" diff -r 8c7301325f9f -r adffc55a682d src/Doc/Logics_ZF/document/build --- 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" diff -r 8c7301325f9f -r adffc55a682d src/Doc/Main/document/build --- 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" diff -r 8c7301325f9f -r adffc55a682d src/Doc/Nitpick/document/build --- 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" diff -r 8c7301325f9f -r adffc55a682d src/Doc/Prog_Prove/document/build --- 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" diff -r 8c7301325f9f -r adffc55a682d src/Doc/Sledgehammer/document/build --- 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" diff -r 8c7301325f9f -r adffc55a682d src/Doc/System/Basics.thy --- 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 \The Isabelle system environment\ text \ - This manual describes Isabelle together with related tools and user - interfaces as seen from a system oriented view. See also the \<^emph>\Isabelle/Isar - Reference Manual\ @{cite "isabelle-isar-ref"} for the actual Isabelle input - language and related concepts, and \<^emph>\The Isabelle/Isar Implementation - Manual\ @{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>\Isabelle settings\ mechanism provides process environment variables - to all Isabelle executables (including tools and user interfaces). - - \<^enum> The raw \<^emph>\Isabelle process\ (@{executable_ref "isabelle_process"}) runs - logic sessions in batch mode. This is rarely required for regular users. - - \<^enum> The main \<^emph>\Isabelle tool wrapper\ (@{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>\Isabelle/Isar Reference Manual\ @{cite + "isabelle-isar-ref"} for the actual Isabelle input language and related + concepts, and \<^emph>\The Isabelle/Isar Implementation Manual\ @{cite + "isabelle-implementation"} for the main concepts of the underlying + implementation in Isabelle/ML. \ section \Isabelle settings \label{sec:settings}\ text \ - The Isabelle system heavily depends on the \<^emph>\settings mechanism\. - Essentially, this is a statically scoped collection of environment + Isabelle executables may depend on the \<^emph>\Isabelle settings\ 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>\not\ intended to be set directly from the - shell, though. Isabelle employs a somewhat more sophisticated scheme of - \<^emph>\settings files\ --- 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>\components\ their \<^emph>\settings files\ as + explained below. \ @@ -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] \"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"\} - \<^descr>[@{setting_def ISABELLE_PROCESS}\\<^sup>*\, @{setting ISABELLE_TOOL}\\<^sup>*\] 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}\\<^sup>*\] 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}\\<^sup>*\] refers to the name of this Isabelle distribution, e.g.\ ``\<^verbatim>\Isabelle2012\''. @@ -228,8 +201,8 @@ \<^verbatim>\dvi\ files. \<^descr>[@{setting_def ISABELLE_TMP_PREFIX}\\<^sup>*\] 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. \ @@ -284,13 +257,52 @@ \ -section \The raw Isabelle process \label{sec:isabelle-process}\ +section \The Isabelle tool wrapper \label{sec:isabelle-tool}\ text \ - The @{executable_def "isabelle_process"} executable runs a bare-bone - Isabelle logic session in batch mode: + The main \<^emph>\Isabelle tool wrapper\ 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] -\Usage: isabelle_process [OPTIONS] [HEAP] +\Usage: isabelle TOOL [ARGS ...] + + Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help. + +Available tools: + ...\} + + 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! +\ + + +subsubsection \Examples\ + +text \ + Show the list of available documentation of the Isabelle distribution: + @{verbatim [display] \isabelle doc\} + + View a certain document as follows: + @{verbatim [display] \isabelle doc system\} + + Query the Isabelle settings environment: + @{verbatim [display] \isabelle getenv ISABELLE_HOME_USER\} +\ + + +section \The raw Isabelle ML process\ + +subsection \Batch mode \label{sec:tool-process}\ + +text \ + The @{tool_def process} tool runs the raw ML process in batch mode: + @{verbatim [display] +\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.\} Heap files without explicit directory specifications are looked up in the @@ -328,49 +342,60 @@ \ -subsubsection \Examples\ +subsubsection \Example\ text \ - In order to demonstrate batch execution of Isabelle, we retrieve the \<^verbatim>\Main\ - theory value from the theory loader within ML (observe the delicate quoting - rules for the Bash shell vs.\ ML): - @{verbatim [display] \isabelle_process -e 'Thy_Info.get_theory "Main"' HOL\} + The subsequent example retrieves the \<^verbatim>\Main\ theory value from the theory + loader within ML: + @{verbatim [display] \isabelle process -e 'Thy_Info.get_theory "Main"' HOL\} + + 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. \ -section \The Isabelle tool wrapper \label{sec:isabelle-tool}\ +subsection \Interactive mode\ text \ - 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] -\Usage: isabelle TOOL [ARGS ...] +\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: - ...\} + Build a logic session image and run the raw Isabelle ML process + in interactive mode, with line editor ISABELLE_LINE_EDITOR.\} - 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! -\ + Option \<^verbatim>\-l\ specifies the logic session name. By default, its heap image is + checked and built on demand, but the option \<^verbatim>\-n\ skips that. Option \<^verbatim>\-r\ + abbreviates \<^verbatim>\-l RAW_ML_SYSTEM\, which is relevant to bootstrap + Isabelle/Pure interactively. + Options \<^verbatim>\-d\ and \<^verbatim>\-s\ have the same meaning as for @{tool build} + (\secref{sec:tool-build}). + + Options \<^verbatim>\-m\ and \<^verbatim>\-o\ have the same meaning as for @{tool process} + (\secref{sec:tool-process}). -subsubsection \Examples\ - -text \ - Show the list of available documentation of the Isabelle distribution: - @{verbatim [display] \isabelle doc\} + \<^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] \isabelle doc system\} - - Query the Isabelle settings environment: - @{verbatim [display] \isabelle getenv ISABELLE_HOME_USER\} + 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}. \ diff -r 8c7301325f9f -r adffc55a682d src/Doc/System/Misc.thy --- 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 @@ \ -section \Raw ML console\ - -text \ - The @{tool_def console} tool runs the Isabelle process with raw ML console: - @{verbatim [display] -\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).\} - - Option \<^verbatim>\-l\ specifies the logic session name. By default, its heap image is - checked and built on demand, but the option \<^verbatim>\-n\ skips that. Option \<^verbatim>\-r\ - abbreviates \<^verbatim>\-l RAW_ML_SYSTEM\, which is relevant to bootstrap - Isabelle/Pure interactively. - - Options \<^verbatim>\-d\ and \<^verbatim>\-s\ have the same meaning as for @{tool build} - (\secref{sec:tool-build}). - - Options \<^verbatim>\-m\ and \<^verbatim>\-o\ 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}. -\ - - section \Displaying documents \label{sec:tool-display}\ text \ @@ -213,7 +170,7 @@ determined by @{setting ISABELLE_HOME}. The \BINDIR\ 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>\$HOME/bin\. diff -r 8c7301325f9f -r adffc55a682d src/Doc/System/Presentation.thy --- 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; \\ diff -r 8c7301325f9f -r adffc55a682d src/Doc/System/document/build --- 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" diff -r 8c7301325f9f -r adffc55a682d src/Doc/Tutorial/document/build --- 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" diff -r 8c7301325f9f -r adffc55a682d src/Doc/prepare_document --- 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" diff -r 8c7301325f9f -r adffc55a682d src/HOL/Mirabelle/ex/Ex.thy --- 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" diff -r 8c7301325f9f -r adffc55a682d src/HOL/Mirabelle/lib/scripts/mirabelle.pl --- 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) { diff -r 8c7301325f9f -r adffc55a682d src/HOL/Mutabelle/lib/Tools/mutabelle --- 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 diff -r 8c7301325f9f -r adffc55a682d src/HOL/TPTP/CASC/ReadMe --- 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. diff -r 8c7301325f9f -r adffc55a682d src/HOL/TPTP/lib/Tools/tptp_graph --- 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() diff -r 8c7301325f9f -r adffc55a682d src/HOL/TPTP/lib/Tools/tptp_isabelle --- 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 diff -r 8c7301325f9f -r adffc55a682d src/HOL/TPTP/lib/Tools/tptp_isabelle_hot --- 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 diff -r 8c7301325f9f -r adffc55a682d src/HOL/TPTP/lib/Tools/tptp_nitpick --- 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 diff -r 8c7301325f9f -r adffc55a682d src/HOL/TPTP/lib/Tools/tptp_refute --- 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 diff -r 8c7301325f9f -r adffc55a682d src/HOL/TPTP/lib/Tools/tptp_sledgehammer --- 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 diff -r 8c7301325f9f -r adffc55a682d src/HOL/TPTP/lib/Tools/tptp_translate --- 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.$" diff -r 8c7301325f9f -r adffc55a682d src/Pure/Concurrent/bash.ML --- 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; - diff -r 8c7301325f9f -r adffc55a682d src/Pure/Concurrent/bash.scala --- 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) - } - } -} diff -r 8c7301325f9f -r adffc55a682d src/Pure/Concurrent/bash_windows.ML --- 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; diff -r 8c7301325f9f -r adffc55a682d src/Pure/Concurrent/random.ML --- 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; - diff -r 8c7301325f9f -r adffc55a682d src/Pure/General/random.ML --- /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; + diff -r 8c7301325f9f -r adffc55a682d src/Pure/General/timing.scala --- 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 } diff -r 8c7301325f9f -r adffc55a682d src/Pure/ROOT --- 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" diff -r 8c7301325f9f -r adffc55a682d src/Pure/ROOT.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"; diff -r 8c7301325f9f -r adffc55a682d src/Pure/System/bash.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; + diff -r 8c7301325f9f -r adffc55a682d src/Pure/System/bash.scala --- /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) + } + } +} diff -r 8c7301325f9f -r adffc55a682d src/Pure/System/bash_windows.ML --- /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; diff -r 8c7301325f9f -r adffc55a682d src/Pure/System/isabelle_process.scala --- 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( diff -r 8c7301325f9f -r adffc55a682d src/Pure/System/ml_process.scala --- 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) - } -} diff -r 8c7301325f9f -r adffc55a682d src/Pure/Thy/present.ML --- 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 (); diff -r 8c7301325f9f -r adffc55a682d src/Pure/Tools/build.scala --- 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 } } diff -r 8c7301325f9f -r adffc55a682d src/Pure/Tools/ml_console.scala --- 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), diff -r 8c7301325f9f -r adffc55a682d src/Pure/Tools/ml_process.scala --- /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 + } + } +} diff -r 8c7301325f9f -r adffc55a682d src/Pure/build-jars --- 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 diff -r 8c7301325f9f -r adffc55a682d src/Pure/library.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) diff -r 8c7301325f9f -r adffc55a682d src/Tools/Code/code_ml.ML --- 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", diff -r 8c7301325f9f -r adffc55a682d src/Tools/jEdit/lib/Tools/jedit --- 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 diff -r 8c7301325f9f -r adffc55a682d src/Tools/jEdit/lib/Tools/jedit_client --- 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[@]}" diff -r 8c7301325f9f -r adffc55a682d src/Tools/jEdit/src/active.scala --- 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))) }