isabelle.Build uses ML_Process directly;
isabelle_process is for batch mode only;
removed unused feeder (already part of "isabelle console");
--- 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[@]}" </dev/null
- RC="$?"
-else
- "$ISABELLE_HOME/lib/scripts/feeder" -p | \
- {
- read FPID; "$ML_HOME/poly" -q -i $ML_OPTIONS "${FIRST_ML_OPTIONS[@]}" "${LAST_ML_OPTIONS[@]}"
- RC="$?"
- kill -TERM "$FPID"
- exit "$RC"
- }
- RC="$?"
-fi
-
-[ -n "$ISABELLE_PROCESS_OPTIONS" ] && rm -f "$ISABELLE_PROCESS_OPTIONS"
-rmdir "$ISABELLE_TMP"
-
-exit "$RC"
+"$ISABELLE_TOOL" java isabelle.Isabelle_Process "$@"
--- a/lib/scripts/feeder Wed Mar 09 16:53:14 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,77 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Markus Wenzel, TU Muenchen
-#
-# feeder - feed isabelle session
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-DIR="$(dirname "$0")"
-
-function usage()
-{
- echo
- echo "Usage: $PRG [OPTIONS]"
- echo
- echo " Options are:"
- echo " -h TEXT head text (encoded as utf8)"
- echo " -p emit my pid"
- echo " -q do not pipe stdin"
- echo " -t TEXT tail text"
- echo
- echo " Output texts (pid, head, stdin, tail), then wait to be terminated."
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&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"
--- 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 (<STDIN>) {
- print;
- }
-}
-
-emit("$tail");
-
-
-# wait forever
-
-close STDOUT;
-sleep;
--- 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>\<open>Isabelle process\<close> (@{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>\<open>Isabelle tool wrapper\<close> (@{executable_ref isabelle}) provides a
generic startup environment Isabelle related utilities, user interfaces etc.
@@ -289,35 +287,25 @@
section \<open>The raw Isabelle process \label{sec:isabelle-process}\<close>
text \<open>
- 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]
\<open>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.\<close>}
+ If HEAP is a plain name (default $ISABELLE_LOGIC), it is searched in
+ $ISABELLE_PATH; if it contains a slash, it is taken as literal file;
+ if it is RAW_ML_SYSTEM, the initial ML heap is used.\<close>}
- Heap files without 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>\<open>/\<close>) in the name (hint: use \<^verbatim>\<open>./\<close> 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.
\<close>
@@ -331,45 +319,22 @@
\<^medskip>
The \<^verbatim>\<open>-m\<close> 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>\<open>-e\<close> texts). The \<^verbatim>\<open>-q\<close> option inhibits interaction, thus providing a pure
- batch mode facility.
+ session. For example, \<^verbatim>\<open>-m ASCII\<close> prefers ASCII replacement syntax over
+ mathematical Isabelle symbols.
\<^medskip>
Option \<^verbatim>\<open>-o\<close> allows to override Isabelle system options for this process,
- see also \secref{sec:system-options}. Alternatively, option \<^verbatim>\<open>-O\<close> specifies
- the full environment of system options as a file in YXML format (according
- to the Isabelle/Scala function \<^verbatim>\<open>isabelle.Options.encode\<close>).
-
- \<^medskip>
- The \<^verbatim>\<open>-P\<close> 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>\<open>-S\<close> 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}.
\<close>
subsubsection \<open>Examples\<close>
text \<open>
- Run an interactive session of the default object-logic (as specified by the
- @{setting ISABELLE_LOGIC} setting) like this:
- @{verbatim [display] \<open>isabelle_process\<close>}
-
- \<^medskip>
- The next example demonstrates batch execution of Isabelle. We retrieve the
- \<^verbatim>\<open>Main\<close> theory value from the theory loader within ML (observe the delicate
- quoting rules for the Bash shell vs.\ ML):
- @{verbatim [display] \<open>isabelle_process -e 'Thy_Info.get_theory "Main"' -q HOL\<close>}
+ In order to demonstrate batch execution of Isabelle, we retrieve the \<^verbatim>\<open>Main\<close>
+ theory value from the theory loader within ML (observe the delicate quoting
+ rules for the Bash shell vs.\ ML):
+ @{verbatim [display] \<open>isabelle_process -e 'Thy_Info.get_theory "Main"' HOL\<close>}
Note that the output text will be interspersed with additional junk messages
by the ML runtime environment.
--- 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"
--- 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) {
--- 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"
--- 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()
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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.$"
--- 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](
--- 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 (" ^
--- 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,
--- 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)
}
}
--- 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 =
{
--- 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",