# HG changeset patch # User wenzelm # Date 1457548209 -3600 # Node ID 27f90319a499981eaa649ced73e7de58b999b390 # Parent acd17a6ce17d79434fd3a5f1ae933e8eb5b99d04 isabelle.Build uses ML_Process directly; isabelle_process is for batch mode only; removed unused feeder (already part of "isabelle console"); diff -r acd17a6ce17d -r 27f90319a499 bin/isabelle_process --- a/bin/isabelle_process Wed Mar 09 16:53:14 2016 +0100 +++ b/bin/isabelle_process Wed Mar 09 19:30:09 2016 +0100 @@ -9,248 +9,10 @@ exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@" fi - -## settings - -PRG="$(basename "$0")" - ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)" source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 -## diagnostics - -function usage() -{ - echo - echo "Usage: $PRG [OPTIONS] [HEAP]" - echo - echo " Options are:" - echo " -O system options from given YXML file" - echo " -P SOCKET startup process wrapper via TCP socket" - echo " -S secure mode -- disallow critical operations" - echo " -e ML_EXPR evaluate ML expression on startup" - echo " -f ML_FILE evaluate ML file on startup" - echo " -m MODE add print mode for output" - echo " -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)" - echo " -q non-interactive session" - echo - echo " If HEAP is a plain name (default \"$ISABELLE_LOGIC\"), it is searched in \$ISABELLE_PATH;" - echo " if it contains a slash, it is taken as literal file; if it is RAW_ML_SYSTEM," - echo " the initial ML heap is used." - echo - exit 1 -} - -function fail() -{ - echo "$1" >&2 - exit 2 -} - -function check_file() -{ - [ ! -f "$1" ] && fail "Bad file: \"$1\"" -} - - -## process command line - -# options - -OPTIONS_FILE="" -PROCESS_SOCKET="" -SECURE="" -declare -a LAST_ML_OPTIONS=() -MODES="" -declare -a SYSTEM_OPTIONS=() -TERMINATE="" - -while getopts "O:P:Se:f:m:o:q" OPT -do - case "$OPT" in - O) - OPTIONS_FILE="$OPTARG" - ;; - P) - PROCESS_SOCKET="$OPTARG" - ;; - S) - SECURE=true - ;; - e) - LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="--eval" - LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="$OPTARG" - ;; - f) - LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="--use" - LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="$OPTARG" - ;; - m) - if [ -z "$MODES" ]; then - MODES="\"$OPTARG\"" - else - MODES="\"$OPTARG\", $MODES" - fi - ;; - o) - SYSTEM_OPTIONS["${#SYSTEM_OPTIONS[@]}"]="$OPTARG" - ;; - q) - TERMINATE=true - ;; - \?) - usage - ;; - esac -done - -shift $(($OPTIND - 1)) - - -# args - -HEAP="" - -if [ "$#" -ge 1 ]; then - HEAP="$1" - shift -fi - -[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; } - - -## check ML system - -[ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle." - - -## heap file - -declare -a FIRST_ML_OPTIONS=() - -[ -z "$HEAP" ] && HEAP="$ISABELLE_LOGIC" +isabelle_admin_build jars || exit $? -case "$HEAP" in - RAW_ML_SYSTEM) - HEAP_FILE="" - ;; - */*) - HEAP_FILE="$HEAP" - [ ! -f "$HEAP_FILE" ] && fail "Bad heap file: \"$HEAP_FILE\"" - ;; - *) - HEAP_FILE="" - ISA_PATH="" - - splitarray ":" "$ISABELLE_PATH"; PATHS=("${SPLITARRAY[@]}") - for DIR in "${PATHS[@]}" - do - DIR="$DIR/$ML_IDENTIFIER" - ISA_PATH="$ISA_PATH $DIR\n" - [ -z "$HEAP_FILE" -a -f "$DIR/$HEAP" ] && HEAP_FILE="$DIR/$HEAP" - done - - if [ -z "$HEAP_FILE" ]; then - echo "Unknown logic \"$HEAP\" -- no heap file found in:" >&2 - echo -ne "$ISA_PATH" >&2 - exit 2 - fi - ;; -esac - -if [ -z "$HEAP_FILE" ]; then - case "$ML_PLATFORM" in - *-windows) - FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval" - FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="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))" - ;; - *) - FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval" - FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="fun exit rc = Posix.Process.exit (Word8.fromInt rc)" - ;; - esac -else - check_file "$HEAP_FILE" - case "$ML_PLATFORM" in - *-windows) - PLATFORM_HEAP_FILE="$(platform_path -m "$HEAP_FILE")" - ;; - *) - PLATFORM_HEAP_FILE="$HEAP_FILE" - ;; - esac - PLATFORM_HEAP_FILE="$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$PLATFORM_HEAP_FILE")" - FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval" - FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="PolyML.SaveState.loadState \"$PLATFORM_HEAP_FILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $HEAP_FILE\\n\"); OS.Process.exit OS.Process.failure)" -fi - - -## prepare tmp directory - -[ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle -ISABELLE_PID="$$" -ISABELLE_TMP="$ISABELLE_TMP_PREFIX$ISABELLE_PID" -mkdir -p "$ISABELLE_TMP" -chmod $(umask -S) "$ISABELLE_TMP" - - -## ML text - -if [ -n "$MODES" ]; then - FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval" - FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="Print_Mode.add_modes [$MODES]" -fi - -if [ -n "$SECURE" ]; then - LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="--eval" - LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="Secure.set_secure ()" -fi - -if [ -n "$PROCESS_SOCKET" ]; then - LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="--eval" - LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="Isabelle_Process.init \"$PROCESS_SOCKET\"" -else - ISABELLE_PROCESS_OPTIONS="$ISABELLE_TMP/options" - if [ -n "$OPTIONS_FILE" ]; then - [ "${#SYSTEM_OPTIONS[@]}" -gt 0 ] && \ - fail "Cannot provide options file and options on command-line" - mv "$OPTIONS_FILE" "$ISABELLE_PROCESS_OPTIONS" || - fail "Failed to move options file \"$OPTIONS_FILE\"" - else - "$ISABELLE_TOOL" options -x "$ISABELLE_PROCESS_OPTIONS" -- "${SYSTEM_OPTIONS[@]}" || \ - fail "Failed to retrieve Isabelle system options" - fi - if [ "$HEAP" != RAW_ML_SYSTEM -a "$HEAP" != RAW ]; then - FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval" - FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="Exn.capture_exit 2 Options.load_default ()" - fi -fi - - -## ML process - -check_file "$ML_HOME/poly" -librarypath "$ML_HOME" - -export ISABELLE_PID ISABELLE_TMP ISABELLE_PROCESS_OPTIONS - -if [ -n "$TERMINATE" ]; then - "$ML_HOME/poly" --error-exit -q -i $ML_OPTIONS \ - "${FIRST_ML_OPTIONS[@]}" "${LAST_ML_OPTIONS[@]}" &2 - exit 2 -} - - -## process command line - -# options - -HEAD="" -EMITPID="" -QUIT="" -TAIL="" - -while getopts "h:pqt:" OPT -do - case "$OPT" in - h) - HEAD="$OPTARG" - ;; - p) - EMITPID=true - ;; - q) - QUIT=true - ;; - t) - TAIL="$OPTARG" - ;; - \?) - usage - ;; - esac -done - -shift $(($OPTIND - 1)) - - -# args - -[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; } - - - -## main - -exec perl -w "$DIR"/feeder.pl "$HEAD" "$EMITPID" "$QUIT" "$TAIL" diff -r acd17a6ce17d -r 27f90319a499 lib/scripts/feeder.pl --- a/lib/scripts/feeder.pl Wed Mar 09 16:53:14 2016 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,47 +0,0 @@ -# -# Author: Markus Wenzel, TU Muenchen -# -# feeder.pl - feed isabelle session -# - -# args - -($head, $emitpid, $quit, $tail) = @ARGV; - - -# setup signal handlers - -$SIG{'INT'} = "IGNORE"; - - -# main - -#buffer lines -$| = 1; - -sub emit { - my ($text) = @_; - if ($text) { - utf8::upgrade($text); - $text =~ s/([\x80-\xff])/\\${\(ord($1))}/g; - print $text, "\n"; - } -} - -$emitpid && (print $$, "\n"); - -emit("$head"); - -if (!$quit) { - while () { - print; - } -} - -emit("$tail"); - - -# wait forever - -close STDOUT; -sleep; diff -r acd17a6ce17d -r 27f90319a499 src/Doc/System/Basics.thy --- a/src/Doc/System/Basics.thy Wed Mar 09 16:53:14 2016 +0100 +++ b/src/Doc/System/Basics.thy Wed Mar 09 19:30:09 2016 +0100 @@ -22,9 +22,7 @@ to all Isabelle executables (including tools and user interfaces). \<^enum> The raw \<^emph>\Isabelle process\ (@{executable_ref "isabelle_process"}) runs - logic sessions either interactively or in batch mode. In particular, this - view abstracts over the invocation of the actual ML system to be used. - Regular users rarely need to care about the low-level process. + 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. @@ -289,35 +287,25 @@ section \The raw Isabelle process \label{sec:isabelle-process}\ text \ - The @{executable_def "isabelle_process"} executable runs bare-bones Isabelle - logic sessions --- either interactively or in batch mode. It provides an - abstraction over the underlying ML system and its saved heap files. Its - usage is: + The @{executable_def "isabelle_process"} executable runs a bare-bone + Isabelle logic session in batch mode: @{verbatim [display] \Usage: isabelle_process [OPTIONS] [HEAP] Options are: - -O system options from given YXML file - -P SOCKET startup process wrapper via TCP socket - -S secure mode -- disallow critical operations -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) - -q non-interactive session - If HEAP is a plain name (default "HOL"), 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.\} + 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 path specifications are looked up in the @{setting - ISABELLE_PATH} setting, which may consist of multiple components separated - by colons --- these are tried in the given order with the value of @{setting - ML_IDENTIFIER} appended internally. In a similar way, base names are - relative to the directory specified by @{setting ISABELLE_OUTPUT}. In any - case, actual file locations may also be given by including at least one - slash (\<^verbatim>\/\) in the name (hint: use \<^verbatim>\./\ to refer to the current - directory). + Heap files without explicit directory specifications are looked up in the + @{setting ISABELLE_PATH} setting, which may consist of multiple components + separated by colons --- these are tried in the given order with the value of + @{setting ML_IDENTIFIER} appended internally. \ @@ -331,45 +319,22 @@ \<^medskip> The \<^verbatim>\-m\ option adds identifiers of print modes to be made active for this - session. Typically, this is used by some user interface, e.g.\ to enable - output of proper mathematical symbols. - - \<^medskip> - Isabelle normally enters an interactive top-level loop (after processing the - \<^verbatim>\-e\ texts). The \<^verbatim>\-q\ option inhibits interaction, thus providing a pure - batch mode facility. + session. For example, \<^verbatim>\-m ASCII\ prefers ASCII replacement syntax over + mathematical Isabelle symbols. \<^medskip> Option \<^verbatim>\-o\ allows to override Isabelle system options for this process, - see also \secref{sec:system-options}. Alternatively, option \<^verbatim>\-O\ specifies - the full environment of system options as a file in YXML format (according - to the Isabelle/Scala function \<^verbatim>\isabelle.Options.encode\). - - \<^medskip> - The \<^verbatim>\-P\ option starts the Isabelle process wrapper for Isabelle/Scala, - with a private protocol running over the specified TCP socket. Isabelle/ML - and Isabelle/Scala provide various programming interfaces to invoke protocol - functions over untyped strings and XML trees. - - \<^medskip> - The \<^verbatim>\-S\ option makes the Isabelle process more secure by disabling some - critical operations, notably runtime compilation and evaluation of ML source - code. + see also \secref{sec:system-options}. \ subsubsection \Examples\ text \ - Run an interactive session of the default object-logic (as specified by the - @{setting ISABELLE_LOGIC} setting) like this: - @{verbatim [display] \isabelle_process\} - - \<^medskip> - The next example demonstrates 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"' -q HOL\} + 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\} Note that the output text will be interspersed with additional junk messages by the ML runtime environment. diff -r acd17a6ce17d -r 27f90319a499 src/HOL/Mirabelle/ex/Ex.thy --- a/src/HOL/Mirabelle/ex/Ex.thy Wed Mar 09 16:53:14 2016 +0100 +++ b/src/HOL/Mirabelle/ex/Ex.thy Wed Mar 09 19:30:09 2016 +0100 @@ -3,7 +3,7 @@ ML {* val rc = Isabelle_System.bash - "cd \"$ISABELLE_HOME/src/HOL/Library\"; \"$ISABELLE_TOOL\" mirabelle -q arith Inner_Product.thy"; + "cd \"$ISABELLE_HOME/src/HOL/Library\"; \"$ISABELLE_TOOL\" 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 acd17a6ce17d -r 27f90319a499 src/HOL/Mirabelle/lib/scripts/mirabelle.pl --- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Wed Mar 09 16:53:14 2016 +0100 +++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Wed Mar 09 19:30:09 2016 +0100 @@ -159,8 +159,7 @@ my $cmd = "\"$ENV{'ISABELLE_PROCESS'}\" " . - "-o quick_and_dirty -e 'Multithreading.max_threads_setmp 1 use_thy \"$path/$new_thy_name\"' -q $mirabelle_logic" . - $quiet; + "-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 acd17a6ce17d -r 27f90319a499 src/HOL/Mutabelle/lib/Tools/mutabelle --- a/src/HOL/Mutabelle/lib/Tools/mutabelle Wed Mar 09 16:53:14 2016 +0100 +++ b/src/HOL/Mutabelle/lib/Tools/mutabelle Wed Mar 09 19:30:09 2016 +0100 @@ -134,7 +134,7 @@ # execution "$ISABELLE_PROCESS" -o auto_time_limit=10.0 \ - -e 'use_thy "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test"' -q "$MUTABELLE_LOGIC" > "$MUTABELLE_OUTPUT_PATH/err" 2>&1 + -e 'use_thy "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test"' "$MUTABELLE_LOGIC" > "$MUTABELLE_OUTPUT_PATH/err" 2>&1 [ $? -ne 0 ] && echo "isabelle processing of mutabelle failed" diff -r acd17a6ce17d -r 27f90319a499 src/HOL/TPTP/lib/Tools/tptp_graph --- a/src/HOL/TPTP/lib/Tools/tptp_graph Wed Mar 09 16:53:14 2016 +0100 +++ b/src/HOL/TPTP/lib/Tools/tptp_graph Wed Mar 09 19:30:09 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\";" -q Pure + "$ISABELLE_PROCESS" -e "use_thy \"$WORKDIR/$LOADER\";" Pure } function cleanup_workdir() diff -r acd17a6ce17d -r 27f90319a499 src/HOL/TPTP/lib/Tools/tptp_isabelle --- a/src/HOL/TPTP/lib/Tools/tptp_isabelle Wed Mar 09 16:53:14 2016 +0100 +++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle Wed Mar 09 19:30:09 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" -q -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 acd17a6ce17d -r 27f90319a499 src/HOL/TPTP/lib/Tools/tptp_isabelle_hot --- a/src/HOL/TPTP/lib/Tools/tptp_isabelle_hot Wed Mar 09 16:53:14 2016 +0100 +++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle_hot Wed Mar 09 19:30:09 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" -q -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 acd17a6ce17d -r 27f90319a499 src/HOL/TPTP/lib/Tools/tptp_nitpick --- a/src/HOL/TPTP/lib/Tools/tptp_nitpick Wed Mar 09 16:53:14 2016 +0100 +++ b/src/HOL/TPTP/lib/Tools/tptp_nitpick Wed Mar 09 19:30:09 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" -q -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 acd17a6ce17d -r 27f90319a499 src/HOL/TPTP/lib/Tools/tptp_refute --- a/src/HOL/TPTP/lib/Tools/tptp_refute Wed Mar 09 16:53:14 2016 +0100 +++ b/src/HOL/TPTP/lib/Tools/tptp_refute Wed Mar 09 19:30:09 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" -q -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 acd17a6ce17d -r 27f90319a499 src/HOL/TPTP/lib/Tools/tptp_sledgehammer --- a/src/HOL/TPTP/lib/Tools/tptp_sledgehammer Wed Mar 09 16:53:14 2016 +0100 +++ b/src/HOL/TPTP/lib/Tools/tptp_sledgehammer Wed Mar 09 19:30:09 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" -q -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 acd17a6ce17d -r 27f90319a499 src/HOL/TPTP/lib/Tools/tptp_translate --- a/src/HOL/TPTP/lib/Tools/tptp_translate Wed Mar 09 16:53:14 2016 +0100 +++ b/src/HOL/TPTP/lib/Tools/tptp_translate Wed Mar 09 19:30:09 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" -q -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 acd17a6ce17d -r 27f90319a499 src/Pure/Concurrent/bash.scala --- a/src/Pure/Concurrent/bash.scala Wed Mar 09 16:53:14 2016 +0100 +++ b/src/Pure/Concurrent/bash.scala Wed Mar 09 19:30:09 2016 +0100 @@ -27,7 +27,9 @@ } def process(script: String, - cwd: JFile = null, env: Map[String, String] = null, redirect: Boolean = false): Process = + cwd: JFile = null, + env: Map[String, String] = Map.empty, + redirect: Boolean = false): Process = new Process(script, cwd, env, redirect) class Process private [Bash]( diff -r acd17a6ce17d -r 27f90319a499 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Wed Mar 09 16:53:14 2016 +0100 +++ b/src/Pure/ROOT.ML Wed Mar 09 19:30:09 2016 +0100 @@ -83,8 +83,6 @@ PolyML.Compiler.reportExhaustiveHandlers := true; PolyML.Compiler.printInAlphabeticalOrder := false; PolyML.Compiler.maxInlineSize := 80; -PolyML.Compiler.prompt1 := "ML> "; -PolyML.Compiler.prompt2 := "ML# "; fun ml_make_string struct_name = "(fn x => Pretty.string_of (Pretty.from_ML (ML_Pretty.from_polyml (PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^ diff -r acd17a6ce17d -r 27f90319a499 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Wed Mar 09 16:53:14 2016 +0100 +++ b/src/Pure/System/isabelle_system.scala Wed Mar 09 19:30:09 2016 +0100 @@ -51,7 +51,7 @@ @volatile private var _settings: Option[Map[String, String]] = None - def settings(env: Map[String, String] = null): Map[String, String] = + def settings(env: Map[String, String] = Map.empty): Map[String, String] = { if (_settings.isEmpty) init() // unsynchronized check if (env == null) _settings.get else _settings.get ++ env @@ -302,7 +302,7 @@ /* bash */ - def bash(script: String, cwd: JFile = null, env: Map[String, String] = null, + def bash(script: String, cwd: JFile = null, env: Map[String, String] = Map.empty, progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), progress_limit: Option[Long] = None, diff -r acd17a6ce17d -r 27f90319a499 src/Pure/System/ml_process.scala --- a/src/Pure/System/ml_process.scala Wed Mar 09 16:53:14 2016 +0100 +++ b/src/Pure/System/ml_process.scala Wed Mar 09 19:30:09 2016 +0100 @@ -7,6 +7,9 @@ package isabelle +import java.io.{File => JFile} + + object ML_Process { def apply(options: Options, @@ -14,6 +17,8 @@ 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 = { @@ -66,7 +71,7 @@ // options val isabelle_process_options = Isabelle_System.tmp_file("options") File.write(isabelle_process_options, YXML.string_of_body(options.encode)) - val env = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options)) + 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 @@ -87,7 +92,7 @@ (eval_heaps ::: eval_initial ::: eval_modes ::: eval_options ::: eval_secure ::: eval_process). map(eval => List("--eval", eval)).flatten ::: args - Bash.process(env = env, redirect = redirect, script = + Bash.process( """ [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle @@ -104,6 +109,6 @@ rmdir "$ISABELLE_TMP" exit "$RC" - """) + """, cwd = cwd, env = env ++ env_options, redirect = redirect) } } diff -r acd17a6ce17d -r 27f90319a499 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Wed Mar 09 16:53:14 2016 +0100 +++ b/src/Pure/Tools/build.scala Wed Mar 09 19:30:09 2016 +0100 @@ -550,6 +550,7 @@ catch { case ERROR(_) => /*error should be exposed in ML*/ } private val args_file = Isabelle_System.tmp_file("args") + private val args_standard_path = File.standard_path(args_file) File.write(args_file, YXML.string_of_body( if (is_pure(name)) Options.encode(info.options) else @@ -566,48 +567,28 @@ theories)))))))))))) })) - private val env = - { - val env0 = - Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> output_standard_path, - (if (is_pure(name)) "ISABELLE_PROCESS_OPTIONS" else "ARGS_FILE") -> - File.standard_path(args_file)) - if (is_pure(name)) - env0 + ("ISABELLE_ML_DEBUGGER" -> info.options.bool("ML_debugger").toString) - else env0 - } + output.file.delete + + private val env = Map("ISABELLE_ML_DEBUGGER" -> info.options.bool("ML_debugger").toString) - private val script = - """ - . "$ISABELLE_HOME/lib/scripts/timestart.bash" - """ + - (if (is_pure(name)) - """ - rm -f "$OUTPUT" - "$ISABELLE_PROCESS" -f "ROOT.ML" \ - -e "Command_Line.tool0 (fn () => (Session.finish (); Options.reset_default (); Session.shutdown (); ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\"));" \ - -q RAW_ML_SYSTEM - """ - else - """ - rm -f "$OUTPUT" - "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q "$INPUT" - """) + - """ - RC="$?" - - . "$ISABELLE_HOME/lib/scripts/timestop.bash" - - if [ "$RC" -eq 0 ]; then - echo "Finished $TARGET ($TIMES_REPORT)" >&2 - fi - - exit "$RC" - """ - - private val future_result = + private val future_result: Future[Process_Result] = Future.thread("build") { - Isabelle_System.bash(script, info.dir.file, env, + val process = + if (is_pure(name)) { + val eval = + "Command_Line.tool0 (fn () => (Session.finish (); Options.reset_default ();" + + " Session.shutdown (); ML_Heap.share_common_data ();" + + " ML_Heap.save_state " + ML_Syntax.print_string_raw(output_standard_path) + "));" + val env1 = env + ("ISABELLE_PROCESS_OPTIONS" -> args_standard_path) + ML_Process(info.options, "RAW_ML_SYSTEM", List("--use", "ROOT.ML", "--eval", eval), + cwd = info.dir.file, env = env1) + } + else { + ML_Process(info.options, parent, + List("--eval", "Build.build " + ML_Syntax.print_string_raw(args_standard_path)), + cwd = info.dir.file, env = env) + } + process.result( progress_stdout = (line: String) => Library.try_unprefix("\floading_theory = ", line) match { case Some(theory) => progress.theory(name, theory) @@ -876,7 +857,9 @@ //{{{ finish job val process_result = job.join - progress.echo(process_result.err) + process_result.err_lines.foreach(progress.echo(_)) + if (process_result.ok) + progress.echo("Finished " + name + " (" + process_result.timing.message_resources + ")") val process_result_tail = { diff -r acd17a6ce17d -r 27f90319a499 src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML Wed Mar 09 16:53:14 2016 +0100 +++ b/src/Tools/Code/code_ml.ML Wed Mar 09 19:30:09 2016 +0100 @@ -869,7 +869,7 @@ check = { env_var = "ISABELLE_PROCESS", make_destination = fn p => Path.append p (Path.explode "ROOT.ML"), make_command = fn _ => - "\"$ISABELLE_PROCESS\" -q -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' Pure" } }) + "\"$ISABELLE_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",