--- a/Admin/bash_process/bash_process.c Wed Mar 09 17:22:43 2016 +0000
+++ b/Admin/bash_process/bash_process.c Wed Mar 09 21:01:22 2016 +0100
@@ -3,11 +3,15 @@
Bash process with separate process group id.
*/
-#include <stdlib.h>
+#include <signal.h>
#include <stdio.h>
+#include <stdlib.h>
#include <string.h>
+#include <sys/resource.h>
+#include <sys/time.h>
#include <sys/types.h>
#include <sys/wait.h>
+#include <time.h>
#include <unistd.h>
static void fail(const char *msg)
@@ -17,31 +21,70 @@
exit(2);
}
+static time_t now()
+{
+ struct timeval tv;
+ if (gettimeofday(&tv, NULL) == 0) {
+ return tv.tv_sec * 1000 + tv.tv_usec / 1000;
+ }
+ else {
+ return time(NULL) * 1000;
+ }
+}
+
int main(int argc, char *argv[])
{
/* args */
- if (argc < 2) {
- fprintf(stderr, "Bad arguments: missing pid file\n");
+ if (argc < 3) {
+ fprintf(stderr, "Bad arguments: PID_FILE and TIMING_FILE required\n");
fflush(stderr);
exit(1);
}
char *pid_name = argv[1];
+ char *timing_name = argv[2];
- /* setsid */
+ /* potential fork */
- if (setsid() == -1) {
+ time_t time_start = now();
+
+ if (strlen(timing_name) > 0 || setsid() == -1) {
pid_t pid = fork();
- int status;
if (pid == -1) fail("Cannot set session id (failed to fork)");
else if (pid != 0) {
+ int status;
+
+ // ingore SIGINT
+ struct sigaction sa;
+ memset(&sa, 0, sizeof(sa));
+ sa.sa_handler = SIG_IGN;
+ sigaction(SIGINT, &sa, 0);
+
if (waitpid(pid, &status, 0) == -1) {
fail("Cannot join forked process");
}
+ /* report timing */
+
+ if (strlen(timing_name) > 0) {
+ long long timing_elapsed = now() - time_start;
+
+ struct rusage ru;
+ getrusage(RUSAGE_CHILDREN, &ru);
+
+ long long timing_cpu =
+ ru.ru_utime.tv_sec * 1000 + ru.ru_utime.tv_usec / 1000 +
+ ru.ru_stime.tv_sec * 1000 + ru.ru_stime.tv_usec / 1000;
+
+ FILE *timing_file = fopen(timing_name, "w");
+ if (timing_file == NULL) fail("Cannot open timing file");
+ fprintf(timing_file, "%lld %lld", timing_elapsed, timing_cpu);
+ fclose(timing_file);
+ }
+
if (WIFEXITED(status)) {
exit(WEXITSTATUS(status));
}
@@ -74,9 +117,10 @@
/* shift command line */
int i;
- for (i = 2; i < argc; i++) {
- argv[i - 2] = argv[i];
+ for (i = 3; i < argc; i++) {
+ argv[i - 3] = argv[i];
}
+ argv[argc - 3] = NULL;
argv[argc - 2] = NULL;
argv[argc - 1] = NULL;
--- a/Admin/bash_process/build Wed Mar 09 17:22:43 2016 +0000
+++ b/Admin/bash_process/build Wed Mar 09 21:01:22 2016 +0100
@@ -37,15 +37,15 @@
case "$TARGET" in
x86_64-linux | x86_64-darwin)
- cc -m64 bash_process.c -o "$TARGET/bash_process"
+ cc -Wall -m64 bash_process.c -o "$TARGET/bash_process"
;;
x86-linux | x86-darwin)
- cc -m32 bash_process.c -o "$TARGET/bash_process"
+ cc -Wall -m32 bash_process.c -o "$TARGET/bash_process"
;;
x86-cygwin)
- cc bash_process.c -o "$TARGET/bash_process.exe"
+ cc -Wall bash_process.c -o "$TARGET/bash_process.exe"
;;
*)
- cc bash_process.c -o "$TARGET/bash_process"
+ cc -Wall bash_process.c -o "$TARGET/bash_process"
;;
esac
--- a/Admin/components/components.sha1 Wed Mar 09 17:22:43 2016 +0000
+++ b/Admin/components/components.sha1 Wed Mar 09 21:01:22 2016 +0100
@@ -1,5 +1,7 @@
fbe83b522cb37748ac1b3c943ad71704fdde2f82 bash_process-1.1.1.tar.gz
bb9ef498cd594b4289221b96146d529c899da209 bash_process-1.1.tar.gz
+81250148f8b89ac3587908fb20645081d7f53207 bash_process-1.2.1.tar.gz
+9e21f447bfa0431ae5097301d553dd6df3c58218 bash_process-1.2.tar.gz
70105fd6fbfd1a868383fc510772b95234325d31 csdp-6.x.tar.gz
2f6417b8e96a0e4e8354fe0f1a253c18fb55d9a7 cvc3-2.4.1.tar.gz
a5e02b5e990da4275dc5d4480c3b72fc73160c28 cvc4-1.5pre-1.tar.gz
--- a/Admin/components/main Wed Mar 09 17:22:43 2016 +0000
+++ b/Admin/components/main Wed Mar 09 21:01:22 2016 +0100
@@ -1,5 +1,5 @@
#main components for everyday use, without big impact on overall build time
-bash_process-1.1.1
+bash_process-1.2.1
csdp-6.x
cvc4-1.5pre-3
e-1.8
--- a/NEWS Wed Mar 09 17:22:43 2016 +0000
+++ b/NEWS Wed Mar 09 21:01:22 2016 +0100
@@ -210,9 +210,22 @@
replaced by structure Timeout, with slightly different signature.
INCOMPATIBILITY.
+* Discontinued cd and pwd operations, which are not well-defined in a
+multi-threaded environment. Note that files are usually located
+relatively to the master directory of a theory (see also
+File.full_path). Potential INCOMPATIBILITY.
+
*** System ***
+* 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
+about spaces or special characters. Note that user output works via
+Path.print (ML) or Path.toString (Scala). INCOMPATIBILITY, the old (and
+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.
--- a/bin/isabelle_process Wed Mar 09 17:22:43 2016 +0000
+++ b/bin/isabelle_process Wed Mar 09 21:01:22 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[@]}"]="Unsynchronized.change print_mode (append [$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/Tools/console Wed Mar 09 17:22:43 2016 +0000
+++ b/lib/Tools/console Wed Mar 09 21:01:22 2016 +0100
@@ -4,7 +4,7 @@
#
# DESCRIPTION: run Isabelle process with raw ML console and line editor
-## settings
+isabelle_admin_build jars || exit $?
case "$ISABELLE_JAVA_PLATFORM" in
x86-*)
@@ -15,112 +15,14 @@
;;
esac
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: isabelle $PRG [OPTIONS]"
- echo
- echo " Options are:"
- echo " -d DIR include session directory"
- echo " -l NAME logic session name (default ISABELLE_LOGIC=\"$ISABELLE_LOGIC\")"
- echo " -m MODE add print mode for output"
- echo " -n no build of session image on startup"
- echo " -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)"
- echo " -r logic session is RAW_ML_SYSTEM"
- echo " -s system build mode for session image"
- echo
- echo " Run Isabelle process with raw ML console and line editor"
- echo " (ISABELLE_LINE_EDITOR=\"$ISABELLE_LINE_EDITOR\")."
- echo
- exit 1
-}
-
-
-## process command line
-
-# options
-
-declare -a ISABELLE_OPTIONS=()
-
-declare -a INCLUDE_DIRS=()
-LOGIC="$ISABELLE_LOGIC"
-NO_BUILD="false"
-declare -a SYSTEM_OPTIONS=()
-SYSTEM_MODE="false"
-
-while getopts "d:l:m:no:rs" OPT
-do
- case "$OPT" in
- d)
- INCLUDE_DIRS["${#INCLUDE_DIRS[@]}"]="$OPTARG"
- ;;
- l)
- LOGIC="$OPTARG"
- ;;
- m)
- ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-m"
- ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="$OPTARG"
- ;;
- n)
- NO_BUILD="true"
- ;;
- o)
- SYSTEM_OPTIONS["${#SYSTEM_OPTIONS[@]}"]="$OPTARG"
- ;;
- r)
- LOGIC="RAW_ML_SYSTEM"
- ;;
- s)
- SYSTEM_MODE="true"
- ;;
- \?)
- usage
- ;;
- esac
-done
-
-shift $(($OPTIND - 1))
-
-
-# args
-
-[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
-
-
-## main
-
-isabelle_admin_build jars || exit $?
-
declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
mkdir -p "$ISABELLE_TMP_PREFIX" || exit $?
-OPTIONS_FILE="$ISABELLE_TMP_PREFIX/options$$"
-
-if [ "$LOGIC" = "RAW_ML_SYSTEM" ]; then
- "$ISABELLE_TOOL" options -x "$OPTIONS_FILE"
-else
- "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Build_Console \
- "$LOGIC" "$NO_BUILD" "$SYSTEM_MODE" "$OPTIONS_FILE" \
- "${INCLUDE_DIRS[@]}" $'\n' "${SYSTEM_OPTIONS[@]}" || {
- rm -f "$OPTIONS_FILE"
- exit "$?"
- }
- ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-m"
- ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="ASCII"
-fi
-
-ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-O"
-ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="$OPTIONS_FILE"
if type -p "$ISABELLE_LINE_EDITOR" > /dev/null
then
- exec "$ISABELLE_LINE_EDITOR" "$ISABELLE_PROCESS" "${ISABELLE_OPTIONS[@]}" -- "$LOGIC"
+ exec "$ISABELLE_LINE_EDITOR" "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@"
else
echo "### No line editor: \"$ISABELLE_LINE_EDITOR\""
- exec "$ISABELLE_PROCESS" "${ISABELLE_OPTIONS[@]}" -- "$LOGIC"
+ exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@"
fi
--- a/lib/scripts/feeder Wed Mar 09 17:22:43 2016 +0000
+++ /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 17:22:43 2016 +0000
+++ /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/lib/scripts/recode.pl Wed Mar 09 17:22:43 2016 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-#
-# Author: Makarius
-#
-# recode.pl - recode utf8 for ML
-#
-
-for (@ARGV) {
- utf8::upgrade($_);
- s/([\x80-\xff])/\\${\(ord($1))}/g;
- print $_;
-}
--- a/src/Doc/System/Basics.thy Wed Mar 09 17:22:43 2016 +0000
+++ b/src/Doc/System/Basics.thy Wed Mar 09 21:01:22 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,48 +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>}
-
- Note that the output text will be interspersed with additional junk messages
- by the ML runtime environment.
+ 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>}
\<close>
--- a/src/Doc/System/Misc.thy Wed Mar 09 17:22:43 2016 +0000
+++ b/src/Doc/System/Misc.thy Wed Mar 09 21:01:22 2016 +0100
@@ -65,7 +65,7 @@
Options are:
-d DIR include session directory
- -l NAME logic session name (default ISABELLE_LOGIC="HOL")
+ -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)
@@ -75,27 +75,27 @@
Run Isabelle process with raw ML console and line editor
(default ISABELLE_LINE_EDITOR).\<close>}
- The \<^verbatim>\<open>-l\<close> option specifies the logic session name. By default, its heap
- image is checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that.
-
- Option \<^verbatim>\<open>-r\<close> abbreviates \<^verbatim>\<open>-l RAW_ML_SYSTEM\<close>, which is relevant to bootstrap
+ Option \<^verbatim>\<open>-l\<close> specifies the logic session name. By default, its heap image is
+ checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that. Option \<^verbatim>\<open>-r\<close>
+ abbreviates \<^verbatim>\<open>-l RAW_ML_SYSTEM\<close>, which is relevant to bootstrap
Isabelle/Pure interactively.
- Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-o\<close>, \<^verbatim>\<open>-s\<close> are passed directly to @{tool build}
+ Options \<^verbatim>\<open>-d\<close> and \<^verbatim>\<open>-s\<close> have the same meaning as for @{tool build}
(\secref{sec:tool-build}).
- Options \<^verbatim>\<open>-m\<close>, \<^verbatim>\<open>-o\<close> are passed directly to the underlying Isabelle process
- (\secref{sec:isabelle-process}).
+ Options \<^verbatim>\<open>-m\<close> and \<^verbatim>\<open>-o\<close> have the same meaning as for the raw @{executable
+ isabelle_process} (\secref{sec:isabelle-process}).
- The Isabelle process is run through the line editor that is specified via
+ \<^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.
- Interaction works via the raw ML toplevel loop: this is neither
- Isabelle/Isar nor Isabelle/ML within the usual formal context. Some useful
- ML commands at this stage are @{ML cd}, @{ML pwd}, @{ML use}, @{ML use_thy},
- @{ML use_thys}.
+ The user is connected to the raw ML toplevel loop: this is neither
+ Isabelle/Isar nor Isabelle/ML within the usual formal context. The most
+ relevant ML commands at this stage are @{ML use}, @{ML use_thy}, @{ML
+ use_thys}.
\<close>
--- a/src/HOL/Library/Old_SMT/old_smt_solver.ML Wed Mar 09 17:22:43 2016 +0000
+++ b/src/HOL/Library/Old_SMT/old_smt_solver.ML Wed Mar 09 21:01:22 2016 +0100
@@ -51,9 +51,10 @@
local
-fun make_cmd command options problem_path proof_path = space_implode " " (
- "(exec 2>&1;" :: map File.shell_quote (command () @ options) @
- [File.shell_path problem_path, ")", ">", File.shell_path proof_path])
+fun make_cmd command options problem_path proof_path =
+ space_implode " "
+ ("(exec 2>&1;" :: map File.bash_string (command () @ options) @
+ [File.bash_path problem_path, ")", ">", File.bash_path proof_path])
fun trace_and ctxt msg f x =
let val _ = Old_SMT_Config.trace_msg ctxt (fn () => msg) ()
@@ -82,7 +83,7 @@
Cache_IO.run_and_cache certs key mk_cmd input
| (SOME output, _) =>
trace_and ctxt ("Using cached certificate from " ^
- File.shell_path (Cache_IO.cache_path_of certs) ^ " ...")
+ Path.print (Cache_IO.cache_path_of certs) ^ " ...")
I output))
fun run_solver ctxt name mk_cmd input =
--- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Wed Mar 09 17:22:43 2016 +0000
+++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Wed Mar 09 21:01:22 2016 +0100
@@ -40,7 +40,7 @@
val (output, rc) =
Isabelle_System.bash_output
- ("\"$ISABELLE_CSDP\" " ^ File.shell_path in_path ^ " " ^ File.shell_path out_path)
+ ("\"$ISABELLE_CSDP\" " ^ File.bash_path in_path ^ " " ^ File.bash_path out_path)
val _ = Sum_of_Squares.debug_message ctxt (fn () => "Solver output:\n" ^ output)
val result = if File.exists out_path then File.read out_path else ""
--- a/src/HOL/Library/code_test.ML Wed Mar 09 17:22:43 2016 +0000
+++ b/src/HOL/Library/code_test.ML Wed Mar 09 21:01:22 2016 +0100
@@ -382,9 +382,9 @@
driverN
val compile_cmd =
- File.shell_path (Path.variable ISABELLE_MLTON) ^
- " -default-type intinf " ^ File.shell_path ml_basis_path
- val run_cmd = File.shell_path (Path.append path (Path.basic projectN))
+ File.bash_path (Path.variable ISABELLE_MLTON) ^
+ " -default-type intinf " ^ File.bash_path ml_basis_path
+ val run_cmd = File.bash_path (Path.append path (Path.basic projectN))
in
{files = [(driver_path, driver), (ml_basis_path, ml_basis)],
compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
@@ -464,7 +464,7 @@
" -I " ^ Path.implode path ^
" nums.cma " ^ Path.implode code_path ^ " " ^ Path.implode driver_path
- val run_cmd = File.shell_path compiled_path
+ val run_cmd = File.bash_path compiled_path
in
{files = [(driver_path, driver)],
compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
@@ -509,7 +509,7 @@
Config.get ctxt ghc_options ^ " -o " ^ Path.implode compiled_path ^ " " ^
Path.implode driver_path ^ " -i" ^ Path.implode path
- val run_cmd = File.shell_path compiled_path
+ val run_cmd = File.bash_path compiled_path
in
{files = [(driver_path, driver)],
compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = mk_code_file}
@@ -551,12 +551,12 @@
val compile_cmd =
Path.implode (Path.append (Path.variable ISABELLE_SCALA) (Path.basic "scalac")) ^
- " -d " ^ File.shell_path path ^ " -classpath " ^ File.shell_path path ^ " " ^
- File.shell_path code_path ^ " " ^ File.shell_path driver_path
+ " -d " ^ File.bash_path path ^ " -classpath " ^ File.bash_path path ^ " " ^
+ File.bash_path code_path ^ " " ^ File.bash_path driver_path
val run_cmd =
Path.implode (Path.append (Path.variable ISABELLE_SCALA) (Path.basic "scala")) ^
- " -cp " ^ File.shell_path path ^ " Test"
+ " -cp " ^ File.bash_path path ^ " Test"
in
{files = [(driver_path, driver)],
compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
--- a/src/HOL/Mirabelle/ex/Ex.thy Wed Mar 09 17:22:43 2016 +0000
+++ b/src/HOL/Mirabelle/ex/Ex.thy Wed Mar 09 21:01:22 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 17:22:43 2016 +0000
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Wed Mar 09 21:01:22 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 17:22:43 2016 +0000
+++ b/src/HOL/Mutabelle/lib/Tools/mutabelle Wed Mar 09 21:01:22 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/TPTP_Parser/tptp_interpret.ML Wed Mar 09 17:22:43 2016 +0000
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Wed Mar 09 21:01:22 2016 +0100
@@ -756,8 +756,7 @@
case find_first (fn prefix => File.exists (Path.append prefix path_suffix))
path_prefixes of
SOME prefix => Path.append prefix path_suffix
- | NONE =>
- error ("Cannot find include file " ^ quote (Path.implode path_suffix))
+ | NONE => error ("Cannot find include file " ^ Path.print path_suffix)
(* Ideally, to be in sync with TFF1, we should perform full type skolemization here.
But the problems originating from HOL systems are restricted to top-level
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML Wed Mar 09 17:22:43 2016 +0000
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML Wed Mar 09 21:01:22 2016 +0100
@@ -1797,7 +1797,7 @@
val fms = get_fmlas_of_prob thy1 prob_name
in
if List.null fms then
- (warning ("File " ^ Path.implode file_name ^ " appears empty!");
+ (warning ("File " ^ Path.print file_name ^ " appears empty!");
TPTP_Reconstruction_Data.map (cons ((prob_name, empty_pannot prob_name))) thy1)
else
let
--- a/src/HOL/TPTP/atp_theory_export.ML Wed Mar 09 17:22:43 2016 +0000
+++ b/src/HOL/TPTP/atp_theory_export.ML Wed Mar 09 21:01:22 2016 +0100
@@ -59,8 +59,8 @@
val exec = exec false
val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec)
val command =
- File.shell_path (Path.explode path) ^ " " ^
- arguments ctxt false "" atp_timeout (File.shell_path prob_file)
+ File.bash_path (Path.explode path) ^ " " ^
+ arguments ctxt false "" atp_timeout (File.bash_path prob_file)
(ord, K [], K [])
val outcome =
Timeout.apply atp_timeout Isabelle_System.bash_output command
--- a/src/HOL/TPTP/lib/Tools/tptp_graph Wed Mar 09 17:22:43 2016 +0000
+++ b/src/HOL/TPTP/lib/Tools/tptp_graph Wed Mar 09 21:01:22 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 17:22:43 2016 +0000
+++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle Wed Mar 09 21:01:22 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 17:22:43 2016 +0000
+++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle_hot Wed Mar 09 21:01:22 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 17:22:43 2016 +0000
+++ b/src/HOL/TPTP/lib/Tools/tptp_nitpick Wed Mar 09 21:01:22 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 17:22:43 2016 +0000
+++ b/src/HOL/TPTP/lib/Tools/tptp_refute Wed Mar 09 21:01:22 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 17:22:43 2016 +0000
+++ b/src/HOL/TPTP/lib/Tools/tptp_sledgehammer Wed Mar 09 21:01:22 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 17:22:43 2016 +0000
+++ b/src/HOL/TPTP/lib/Tools/tptp_translate Wed Mar 09 21:01:22 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/HOL/Tools/Nitpick/kodkod.ML Wed Mar 09 17:22:43 2016 +0000
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Wed Mar 09 21:01:22 2016 +0100
@@ -1028,8 +1028,8 @@
val outcome =
let
val code =
- Isabelle_System.bash ("cd " ^ File.shell_quote temp_dir ^ ";\n\
- \\"$KODKODI\"/bin/kodkodi" ^
+ Isabelle_System.bash ("cd " ^ File.bash_string temp_dir ^ ";\n\
+ \\"$KODKODI/bin/kodkodi\"" ^
(if ms >= 0 then " -max-msecs " ^ string_of_int ms
else "") ^
(if max_solutions > 1 then " -solve-all" else "") ^
@@ -1038,9 +1038,9 @@
" -max-threads " ^ string_of_int max_threads
else
"") ^
- " < " ^ File.shell_path in_path ^
- " > " ^ File.shell_path out_path ^
- " 2> " ^ File.shell_path err_path)
+ " < " ^ File.bash_path in_path ^
+ " > " ^ File.bash_path out_path ^
+ " 2> " ^ File.bash_path err_path)
val (io_error, (ps, nontriv_js)) =
read_output_file out_path
||> apfst (map (apfst reindex)) ||> apsnd (map reindex)
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Wed Mar 09 17:22:43 2016 +0000
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Wed Mar 09 21:01:22 2016 +0100
@@ -818,7 +818,7 @@
if getenv env_var = "" then
(warning (env_var ^ " not set; could not execute code for " ^ string_of_system system); "")
else
- (case Isabelle_System.bash_output (cmd ^ File.shell_path file) of
+ (case Isabelle_System.bash_output (cmd ^ File.bash_path file) of
(out, 0) => out
| (_, rc) =>
error ("Error caused by prolog system " ^ env_var ^
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Mar 09 17:22:43 2016 +0000
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Mar 09 21:01:22 2016 +0100
@@ -251,10 +251,10 @@
val _ = map (uncurry File.write) (includes @
[(narrowing_engine_file, if contains_existentials then pnf_narrowing_engine else narrowing_engine),
(code_file, code), (main_file, main)])
- val executable = File.shell_path (Path.append in_path (Path.basic "isabelle_quickcheck_narrowing"))
+ val executable = File.bash_path (Path.append in_path (Path.basic "isabelle_quickcheck_narrowing"))
val cmd = "exec \"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^
ghc_options ^ " " ^
- (space_implode " " (map File.shell_path (map fst includes @ [code_file, narrowing_engine_file, main_file]))) ^
+ (space_implode " " (map File.bash_path (map fst includes @ [code_file, narrowing_engine_file, main_file]))) ^
" -o " ^ executable ^ ";"
val (_, compilation_time) =
elapsed_time "Haskell compilation" (fn () => Isabelle_System.bash cmd)
--- a/src/HOL/Tools/SMT/smt_solver.ML Wed Mar 09 17:22:43 2016 +0000
+++ b/src/HOL/Tools/SMT/smt_solver.ML Wed Mar 09 21:01:22 2016 +0100
@@ -49,8 +49,8 @@
local
fun make_command command options problem_path proof_path =
- "(exec 2>&1;" :: map File.shell_quote (command () @ options) @
- [File.shell_path problem_path, ")", ">", File.shell_path proof_path]
+ "(exec 2>&1;" :: map File.bash_string (command () @ options) @
+ [File.bash_path problem_path, ")", ">", File.bash_path proof_path]
|> space_implode " "
fun with_trace ctxt msg f x =
@@ -79,7 +79,7 @@
Cache_IO.run_and_cache certs key mk_cmd input
| (SOME output, _) =>
with_trace ctxt ("Using cached certificate from " ^
- File.shell_path (Cache_IO.cache_path_of certs) ^ " ...") I output))
+ Path.print (Cache_IO.cache_path_of certs) ^ " ...") I output))
(* Z3 returns 1 if "get-model" or "get-model" fails *)
val normal_return_codes = [0, 1]
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Wed Mar 09 17:22:43 2016 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Wed Mar 09 21:01:22 2016 +0100
@@ -283,10 +283,10 @@
val ord = effective_term_order ctxt name
val args =
- arguments ctxt full_proofs extra slice_timeout (File.shell_path prob_path)
+ arguments ctxt full_proofs extra slice_timeout (File.bash_path prob_path)
(ord, ord_info, sel_weights)
val command =
- "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^ ")"
+ "(exec 2>&1; " ^ File.bash_path command0 ^ " " ^ args ^ " " ^ ")"
|> enclose "TIMEFORMAT='%3R'; { time " " ; }"
val _ =
--- a/src/HOL/Tools/sat_solver.ML Wed Mar 09 17:22:43 2016 +0000
+++ b/src/HOL/Tools/sat_solver.ML Wed Mar 09 21:01:22 2016 +0100
@@ -633,7 +633,7 @@
val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
val outpath = File.tmp_path (Path.explode ("result" ^ serial_str))
val proofpath = File.tmp_path (Path.explode ("result" ^ serial_str ^ ".prf"))
- val cmd = getenv "MINISAT_HOME" ^ "/minisat " ^ File.shell_path inpath ^ " -r " ^ File.shell_path outpath ^ " -t " ^ File.shell_path proofpath ^ "> /dev/null"
+ val cmd = "\"$MINISAT_HOME/minisat\" " ^ File.bash_path inpath ^ " -r " ^ File.bash_path outpath ^ " -t " ^ File.bash_path proofpath ^ "> /dev/null"
fun writefn fm = SAT_Solver.write_dimacs_cnf_file inpath fm
fun readfn () = SAT_Solver.read_std_result_file outpath ("SAT", "", "UNSAT")
val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else ()
@@ -809,7 +809,7 @@
val serial_str = serial_string ()
val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
val outpath = File.tmp_path (Path.explode ("result" ^ serial_str))
- val cmd = getenv "MINISAT_HOME" ^ "/minisat " ^ File.shell_path inpath ^ " -r " ^ File.shell_path outpath ^ " > /dev/null"
+ val cmd = "\"$MINISAT_HOME/minisat\" " ^ File.bash_path inpath ^ " -r " ^ File.bash_path outpath ^ " > /dev/null"
fun writefn fm = SAT_Solver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm)
fun readfn () = SAT_Solver.read_std_result_file outpath ("SAT", "", "UNSAT")
val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else ()
@@ -965,7 +965,7 @@
val serial_str = serial_string ()
val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
val outpath = File.tmp_path (Path.explode ("result" ^ serial_str))
- val cmd = getenv "ZCHAFF_HOME" ^ "/zchaff " ^ File.shell_path inpath ^ " > " ^ File.shell_path outpath
+ val cmd = "\"$ZCHAFF_HOME/zchaff\" " ^ File.bash_path inpath ^ " > " ^ File.bash_path outpath
fun writefn fm = SAT_Solver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm)
fun readfn () = SAT_Solver.read_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable")
val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else ()
@@ -991,8 +991,7 @@
val serial_str = serial_string ()
val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
val outpath = File.tmp_path (Path.explode ("result" ^ serial_str))
- val exec = getenv "BERKMIN_EXE"
- val cmd = getenv "BERKMIN_HOME" ^ "/" ^ (if exec = "" then "BerkMin561" else exec) ^ " " ^ File.shell_path inpath ^ " > " ^ File.shell_path outpath
+ val cmd = "\"$BERKMIN_HOME/${BERKMIN_EXE:-BerkMin561}\" " ^ File.bash_path inpath ^ " > " ^ File.bash_path outpath
fun writefn fm = SAT_Solver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm)
fun readfn () = SAT_Solver.read_std_result_file outpath ("Satisfiable !!", "solution =", "UNSATISFIABLE !!")
val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else ()
@@ -1018,7 +1017,7 @@
val serial_str = serial_string ()
val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
val outpath = File.tmp_path (Path.explode ("result" ^ serial_str))
- val cmd = getenv "JERUSAT_HOME" ^ "/Jerusat1.3 " ^ File.shell_path inpath ^ " > " ^ File.shell_path outpath
+ val cmd = "\"$JERUSAT_HOME/Jerusat1.3\" " ^ File.bash_path inpath ^ " > " ^ File.bash_path outpath
fun writefn fm = SAT_Solver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm)
fun readfn () = SAT_Solver.read_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE")
val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else ()
--- a/src/Pure/Concurrent/bash.ML Wed Mar 09 17:22:43 2016 +0000
+++ b/src/Pure/Concurrent/bash.ML Wed Mar 09 21:01:22 2016 +0100
@@ -38,10 +38,10 @@
val _ = getenv_strict "ISABELLE_BASH_PROCESS";
val status =
OS.Process.system
- ("exec \"$ISABELLE_BASH_PROCESS\" " ^ File.shell_path pid_path ^
- " bash " ^ File.shell_path script_path ^
- " > " ^ File.shell_path out_path ^
- " 2> " ^ File.shell_path err_path);
+ ("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
--- a/src/Pure/Concurrent/bash.scala Wed Mar 09 17:22:43 2016 +0000
+++ b/src/Pure/Concurrent/bash.scala Wed Mar 09 21:01:22 2016 +0100
@@ -13,20 +13,39 @@
object Bash
{
- def process(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
- new Process(cwd, env, redirect, args:_*)
+ 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](
- cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*)
+ 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 =
- {
- val params =
- List(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-", "bash")
- Isabelle_System.process(
- cwd, Isabelle_System.settings(env), redirect, (params ::: args.toList):_*)
- }
+ 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
@@ -45,6 +64,9 @@
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)
@@ -66,8 +88,12 @@
running
}
- def interrupt() { multi_kill("INT") }
- def terminate() { multi_kill("INT") && multi_kill("TERM") && kill("KILL"); proc.destroy }
+ def terminate()
+ {
+ multi_kill("INT") && multi_kill("TERM") && kill("KILL")
+ proc.destroy
+ cleanup()
+ }
// JVM shutdown hook
@@ -77,13 +103,66 @@
try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
catch { case _: IllegalStateException => }
- private def cleanup() =
+
+ // cleanup
+
+ private def cleanup()
+ {
try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
catch { case _: IllegalStateException => }
+ script_file.delete
- /* result */
+ 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 }
+ def join: Int =
+ {
+ val rc = proc.waitFor
+ cleanup()
+ rc
+ }
+
+
+ // result
+
+ def result(
+ progress_stdout: String => Unit = (_: String) => (),
+ progress_stderr: String => Unit = (_: String) => (),
+ progress_limit: Option[Long] = None,
+ strict: Boolean = true): Process_Result =
+ {
+ stdin.close
+
+ val limited = new Limited_Progress(this, progress_limit)
+ val out_lines =
+ Future.thread("bash_stdout") { File.read_lines(stdout, limited(progress_stdout)) }
+ val err_lines =
+ Future.thread("bash_stderr") { File.read_lines(stderr, limited(progress_stderr)) }
+
+ val rc =
+ try { join }
+ catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code }
+ if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
+
+ Process_Result(rc, out_lines.join, err_lines.join, false, timing.value getOrElse Timing.zero)
+ }
}
}
--- a/src/Pure/Concurrent/bash_windows.ML Wed Mar 09 17:22:43 2016 +0000
+++ b/src/Pure/Concurrent/bash_windows.ML Wed Mar 09 21:01:22 2016 +0100
@@ -36,14 +36,14 @@
let
val _ = File.write script_path script;
val bash_script =
- "bash " ^ File.shell_path script_path ^
- " > " ^ File.shell_path out_path ^
- " 2> " ^ File.shell_path err_path;
+ "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)
+ 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
--- a/src/Pure/GUI/color_value.scala Wed Mar 09 17:22:43 2016 +0000
+++ b/src/Pure/GUI/color_value.scala Wed Mar 09 21:01:22 2016 +0100
@@ -9,6 +9,7 @@
import java.awt.Color
+import java.util.Locale
object Color_Value
@@ -31,7 +32,7 @@
val g = new java.lang.Integer(c.getGreen)
val b = new java.lang.Integer(c.getBlue)
val a = new java.lang.Integer(c.getAlpha)
- Word.uppercase(String.format("%02x%02x%02x%02x", r, g, b, a))
+ Word.uppercase(String.format(Locale.ROOT, "%02x%02x%02x%02x", r, g, b, a))
}
def apply(s: String): Color =
--- a/src/Pure/General/file.ML Wed Mar 09 17:22:43 2016 +0000
+++ b/src/Pure/General/file.ML Wed Mar 09 21:01:22 2016 +0100
@@ -8,10 +8,9 @@
sig
val standard_path: Path.T -> string
val platform_path: Path.T -> string
- val shell_quote: string -> string
- val shell_path: Path.T -> string
- val cd: Path.T -> unit
- val pwd: unit -> Path.T
+ val bash_string: string -> string
+ val bash_args: string list -> string
+ val bash_path: Path.T -> string
val full_path: Path.T -> Path.T -> Path.T
val tmp_path: Path.T -> Path.T
val exists: Path.T -> bool
@@ -47,14 +46,25 @@
val standard_path = Path.implode o Path.expand;
val platform_path = ML_System.platform_path o standard_path;
-val shell_quote = enclose "'" "'";
-val shell_path = shell_quote o standard_path;
-
+val bash_string =
+ translate_string (fn ch =>
+ let val c = ord ch in
+ (case ch of
+ "\t" => "$'\\t'"
+ | "\n" => "$'\\n'"
+ | "\f" => "$'\\f'"
+ | "\r" => "$'\\r'"
+ | _ =>
+ if Symbol.is_ascii_letter ch orelse Symbol.is_ascii_digit ch orelse
+ exists_string (fn c => c = ch) "-./:_" then ch
+ else if c < 16 then "$'\\x0" ^ Int.fmt StringCvt.HEX c ^ "'"
+ else if c < 32 orelse c >= 127 then "$'\\x" ^ Int.fmt StringCvt.HEX c ^ "'"
+ else "\\" ^ ch)
+ end);
-(* current working directory *)
+val bash_args = space_implode " " o map bash_string;
-val cd = cd o standard_path;
-val pwd = Path.explode o pwd;
+val bash_path = bash_string o standard_path;
(* full_path *)
@@ -66,7 +76,7 @@
val path'' = Path.append dir path';
in
if Path.is_absolute path'' then path''
- else Path.append (pwd ()) path''
+ else Path.append (Path.explode (ML_System.standard_path (OS.FileSys.getDir ()))) path''
end;
--- a/src/Pure/General/file.scala Wed Mar 09 17:22:43 2016 +0000
+++ b/src/Pure/General/file.scala Wed Mar 09 21:01:22 2016 +0100
@@ -101,11 +101,43 @@
}
- /* shell path (bash) */
+ /* bash path */
- def shell_quote(s: String): String = "'" + s + "'"
- def shell_path(path: Path): String = shell_quote(standard_path(path))
- def shell_path(file: JFile): String = shell_quote(standard_path(file))
+ private def bash_chr(c: Byte): String =
+ {
+ val ch = c.toChar
+ ch match {
+ case '\t' => "$'\\t'"
+ case '\n' => "$'\\n'"
+ case '\f' => "$'\\f'"
+ case '\r' => "$'\\r'"
+ case _ =>
+ if (Symbol.is_ascii_letter(ch) || Symbol.is_ascii_digit(ch) || "-./:_".contains(ch))
+ Symbol.ascii(ch)
+ else if (c < 0) "$'\\x" + Integer.toHexString(256 + c) + "'"
+ else if (c < 16) "$'\\x0" + Integer.toHexString(c) + "'"
+ else if (c < 32 || c >= 127) "$'\\x" + Integer.toHexString(c) + "'"
+ else "\\" + ch
+ }
+ }
+
+ def bash_string(s: String): String =
+ UTF8.bytes(s).iterator.map(bash_chr(_)).mkString
+
+ def bash_args(args: List[String]): String =
+ args.iterator.map(bash_string(_)).mkString(" ")
+
+ def bash_path(path: Path): String = bash_string(standard_path(path))
+ def bash_path(file: JFile): String = bash_string(standard_path(file))
+
+
+ /* directory entries */
+
+ def check_dir(path: Path): Path =
+ if (path.is_dir) path else error("No such directory: " + path)
+
+ def check_file(path: Path): Path =
+ if (path.is_file) path else error("No such file: " + path)
/* find files */
--- a/src/Pure/General/output.scala Wed Mar 09 17:22:43 2016 +0000
+++ b/src/Pure/General/output.scala Wed Mar 09 21:01:22 2016 +0100
@@ -18,7 +18,27 @@
def warning_text(msg: String): String = cat_lines(split_lines(clean_yxml(msg)).map("### " + _))
def error_text(msg: String): String = cat_lines(split_lines(clean_yxml(msg)).map("*** " + _))
- def writeln(msg: String) { if (msg != "") Console.err.println(writeln_text(msg)) }
- def warning(msg: String) { if (msg != "") Console.err.println(warning_text(msg)) }
- def error_message(msg: String) { if (msg != "") Console.err.println(error_text(msg)) }
+ def writeln(msg: String, stdout: Boolean = false)
+ {
+ if (msg != "") {
+ if (stdout) Console.println(writeln_text(msg))
+ else Console.err.println(writeln_text(msg))
+ }
+ }
+
+ def warning(msg: String, stdout: Boolean = false)
+ {
+ if (msg != "") {
+ if (stdout) Console.println(warning_text(msg))
+ else Console.err.println(warning_text(msg))
+ }
+ }
+
+ def error_message(msg: String, stdout: Boolean = false)
+ {
+ if (msg != "") {
+ if (stdout) Console.println(error_text(msg))
+ else Console.err.println(error_text(msg))
+ }
+ }
}
--- a/src/Pure/General/print_mode.ML Wed Mar 09 17:22:43 2016 +0000
+++ b/src/Pure/General/print_mode.ML Wed Mar 09 21:01:22 2016 +0100
@@ -23,6 +23,7 @@
val setmp: string list -> ('a -> 'b) -> 'a -> 'b
val with_modes: string list -> ('a -> 'b) -> 'a -> 'b
val closure: ('a -> 'b) -> 'a -> 'b
+ val add_modes: string list -> unit
end;
structure Print_Mode: PRINT_MODE =
@@ -51,6 +52,8 @@
fun with_modes modes f x = setmp (modes @ print_mode_value ()) f x;
fun closure f = with_modes [] f;
+fun add_modes modes = Unsynchronized.change print_mode (append modes);
+
end;
structure Basic_Print_Mode: BASIC_PRINT_MODE = Print_Mode;
--- a/src/Pure/General/time.scala Wed Mar 09 17:22:43 2016 +0000
+++ b/src/Pure/General/time.scala Wed Mar 09 21:01:22 2016 +0100
@@ -46,5 +46,11 @@
override def toString: String = Time.print_seconds(seconds)
def message: String = toString + "s"
+
+ def message_hms: String =
+ {
+ val s = ms / 1000
+ String.format(Locale.ROOT, "%d:%02d:%02d",
+ new java.lang.Long(s / 3600), new java.lang.Long((s / 60) % 60), new java.lang.Long(s % 60))
+ }
}
-
--- a/src/Pure/General/timing.scala Wed Mar 09 17:22:43 2016 +0000
+++ b/src/Pure/General/timing.scala Wed Mar 09 21:01:22 2016 +0100
@@ -8,6 +8,9 @@
package isabelle
+import java.util.Locale
+
+
object Timing
{
val zero = Timing(Time.zero, Time.zero, Time.zero)
@@ -35,9 +38,20 @@
def + (t: Timing): Timing = Timing(elapsed + t.elapsed, cpu + t.cpu, gc + t.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)
+ String.format(Locale.ROOT, ", factor %.2f", new java.lang.Double(t2 / t1))
+ else ""
+ elapsed.message_hms + " elapsed time, " + resources.message_hms + " cpu time" + factor
+ }
+
def message: String =
elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time"
override def toString: String = message
}
-
--- a/src/Pure/ML/ml_syntax.scala Wed Mar 09 17:22:43 2016 +0000
+++ b/src/Pure/ML/ml_syntax.scala Wed Mar 09 21:01:22 2016 +0100
@@ -33,4 +33,7 @@
def print_string_raw(str: String): String =
quote(UTF8.bytes(str).iterator.map(print_chr(_)).mkString)
+
+ def print_list[A](f: A => String)(list: List[A]): String =
+ "[" + commas(list.map(f)) + "]"
}
--- a/src/Pure/PIDE/batch_session.scala Wed Mar 09 17:22:43 2016 +0000
+++ b/src/Pure/PIDE/batch_session.scala Wed Mar 09 21:01:22 2016 +0100
@@ -58,7 +58,8 @@
case _ =>
}
- prover_session.start("Isabelle", "-q " + quote(parent_session))
+ prover_session.start(receiver =>
+ Isabelle_Process(options, heap = parent_session, receiver = receiver))
batch_session
}
--- a/src/Pure/PIDE/protocol.ML Wed Mar 09 17:22:43 2016 +0000
+++ b/src/Pure/PIDE/protocol.ML Wed Mar 09 21:01:22 2016 +0100
@@ -16,9 +16,7 @@
(fn [options_yxml] =>
let val options = Options.decode (YXML.parse_body options_yxml) in
Options.set_default options;
- Future.ML_statistics := Options.bool options "ML_statistics";
- Multithreading.trace := Options.int options "threads_trace";
- Multithreading.max_threads_update (Options.int options "threads");
+ Isabelle_Process.init_options ();
Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0)
end);
--- a/src/Pure/PIDE/prover.scala Wed Mar 09 17:22:43 2016 +0000
+++ b/src/Pure/PIDE/prover.scala Wed Mar 09 21:01:22 2016 +0100
@@ -39,6 +39,7 @@
/* messages */
sealed abstract class Message
+ type Receiver = Message => Unit
class Input(val name: String, val args: List[String]) extends Message
{
@@ -85,7 +86,7 @@
abstract class Prover(
- receiver: Prover.Message => Unit,
+ receiver: Prover.Receiver,
system_channel: System_Channel,
system_process: Prover.System_Process) extends Protocol
{
--- a/src/Pure/PIDE/resources.scala Wed Mar 09 17:22:43 2016 +0000
+++ b/src/Pure/PIDE/resources.scala Wed Mar 09 21:01:22 2016 +0100
@@ -132,11 +132,5 @@
Thy_Syntax.parse_change(this, reparse_limit, previous, doc_blobs, edits)
def commit(change: Session.Change) { }
-
-
- /* prover process */
-
- def start_prover(receiver: Prover.Message => Unit, name: String, args: String): Prover =
- Isabelle_Process(receiver, args)
}
--- a/src/Pure/PIDE/session.scala Wed Mar 09 17:22:43 2016 +0000
+++ b/src/Pure/PIDE/session.scala Wed Mar 09 21:01:22 2016 +0100
@@ -212,7 +212,7 @@
/* internal messages */
- private case class Start(name: String, args: String)
+ private case class Start(start_prover: Prover.Receiver => Prover)
private case object Stop
private case class Cancel_Exec(exec_id: Document_ID.Exec)
private case class Protocol_Command(name: String, args: List[String])
@@ -532,10 +532,10 @@
case input: Prover.Input =>
all_messages.post(input)
- case Start(name, args) if !prover.defined =>
+ case Start(start_prover) if !prover.defined =>
if (phase == Session.Inactive || phase == Session.Failed) {
phase = Session.Startup
- prover.set(resources.start_prover(manager.send(_), name, args))
+ prover.set(start_prover(manager.send(_)))
}
case Stop =>
@@ -601,8 +601,8 @@
pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
global_state.value.snapshot(name, pending_edits)
- def start(name: String, args: String)
- { manager.send(Start(name, args)) }
+ def start(start_prover: Prover.Receiver => Prover)
+ { manager.send(Start(start_prover)) }
def stop()
{
--- a/src/Pure/ROOT.ML Wed Mar 09 17:22:43 2016 +0000
+++ b/src/Pure/ROOT.ML Wed Mar 09 21:01:22 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 (" ^
@@ -429,6 +427,4 @@
Runtime.toplevel_program (fn () => Thy_Info.use_thys (map (rpair Position.none) args));
val use_thy = use_thys o single;
-val cd = File.cd o Path.explode;
-
Proofterm.proofs := 0;
--- a/src/Pure/System/isabelle_process.ML Wed Mar 09 17:22:43 2016 +0000
+++ b/src/Pure/System/isabelle_process.ML Wed Mar 09 21:01:22 2016 +0100
@@ -10,7 +10,8 @@
val protocol_command: string -> (string list -> unit) -> unit
val reset_tracing: Document_ID.exec -> unit
val crashes: exn list Synchronized.var
- val init: string -> unit
+ val init_protocol: string -> unit
+ val init_options: unit -> unit
end;
structure Isabelle_Process: ISABELLE_PROCESS =
@@ -180,12 +181,12 @@
end;
-(* init *)
+(* init protocol *)
val default_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN];
val default_modes2 = [Symbol.xsymbolsN, isabelle_processN, Pretty.symbolicN];
-val init = uninterruptible (fn _ => fn socket =>
+val init_protocol = uninterruptible (fn _ => fn socket =>
let
val _ = SHA1_Samples.test ()
handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); Exn.reraise exn);
@@ -203,5 +204,13 @@
val _ = loop channel;
in Message_Channel.shutdown msg_channel end);
+
+(* init options *)
+
+fun init_options () =
+ (Future.ML_statistics := Options.default_bool "ML_statistics";
+ Multithreading.trace := Options.default_int "threads_trace";
+ Multithreading.max_threads_update (Options.default_int "threads");
+ Goal.parallel_proofs := Options.default_int "parallel_proofs");
+
end;
-
--- a/src/Pure/System/isabelle_process.scala Wed Mar 09 17:22:43 2016 +0000
+++ b/src/Pure/System/isabelle_process.scala Wed Mar 09 21:01:22 2016 +0100
@@ -10,31 +10,69 @@
object Isabelle_Process
{
def apply(
- receiver: Prover.Message => Unit = Console.println(_),
- prover_args: String = ""): Isabelle_Process =
+ options: Options,
+ heap: String = "",
+ args: List[String] = Nil,
+ modes: List[String] = Nil,
+ secure: Boolean = false,
+ receiver: Prover.Receiver = Console.println(_)): Isabelle_Process =
{
- val system_channel = System_Channel()
- val system_process =
+ val channel = System_Channel()
+ val process =
try {
- val script =
- File.shell_quote(Isabelle_System.getenv_strict("ISABELLE_PROCESS")) +
- " -P " + system_channel.server_name +
- (if (prover_args == "") "" else " " + prover_args)
- val process = Bash.process(null, null, false, "-c", script)
- process.stdin.close
- process
+ ML_Process(options, heap = heap, args = args, modes = modes, secure = secure,
+ channel = Some(channel))
}
- catch { case exn @ ERROR(_) => system_channel.accepted(); throw exn }
+ catch { case exn @ ERROR(_) => channel.accepted(); throw exn }
+ process.stdin.close
+
+ 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]
- new Isabelle_Process(receiver, system_channel, system_process)
+ 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(
- receiver: Prover.Message => Unit,
- system_channel: System_Channel,
- system_process: Prover.System_Process)
- extends Prover(receiver, system_channel, system_process)
+ receiver: Prover.Receiver, channel: System_Channel, process: Prover.System_Process)
+ extends Prover(receiver, channel, process)
{
def encode(s: String): String = Symbol.encode(s)
def decode(s: String): String = Symbol.decode(s)
--- a/src/Pure/System/isabelle_system.ML Wed Mar 09 17:22:43 2016 +0000
+++ b/src/Pure/System/isabelle_system.ML Wed Mar 09 21:01:22 2016 +0100
@@ -51,7 +51,7 @@
then SOME path
else NONE
end handle OS.SysErr _ => NONE) of
- SOME path => bash (File.shell_path path ^ " " ^ args)
+ SOME path => bash (File.bash_path path ^ " " ^ args)
| NONE => (warning ("Unknown Isabelle tool: " ^ name); 2));
fun system_command cmd =
@@ -64,7 +64,7 @@
fun mkdirs path =
if File.is_dir path then ()
else
- (bash ("perl -e \"use File::Path make_path; make_path(" ^ File.shell_path path ^ ");\"");
+ (bash ("perl -e \"use File::Path make_path; make_path('" ^ File.standard_path path ^ "');\"");
if File.is_dir path then () else error ("Failed to create directory: " ^ Path.print path));
fun mkdir path =
@@ -72,7 +72,7 @@
fun copy_dir src dst =
if File.eq (src, dst) then ()
- else (system_command ("cp -p -R -f " ^ File.shell_path src ^ "/. " ^ File.shell_path dst); ());
+ else (system_command ("cp -p -R -f " ^ File.bash_path src ^ "/. " ^ File.bash_path dst); ());
fun copy_file src0 dst0 =
let
@@ -82,7 +82,7 @@
in
if File.eq (src, target) then ()
else
- ignore (system_command ("cp -p -f " ^ File.shell_path src ^ " " ^ File.shell_path target))
+ ignore (system_command ("cp -p -f " ^ File.bash_path src ^ " " ^ File.bash_path target))
end;
fun copy_file_base (base_dir, src0) target_dir =
@@ -112,7 +112,7 @@
(* tmp dirs *)
-fun rm_tree path = system_command ("rm -r -f " ^ File.shell_path path);
+fun rm_tree path = system_command ("rm -r -f " ^ File.bash_path path);
fun with_tmp_dir name f =
let
--- a/src/Pure/System/isabelle_system.scala Wed Mar 09 17:22:43 2016 +0000
+++ b/src/Pure/System/isabelle_system.scala Wed Mar 09 21:01:22 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
@@ -167,7 +167,7 @@
def mkdirs(path: Path): Unit =
if (!path.is_dir) {
- bash("perl -e \"use File::Path make_path; make_path(" + File.shell_path(path) + ");\"")
+ bash("perl -e \"use File::Path make_path; make_path('" + File.standard_path(path) + "');\"")
if (!path.is_dir) error("Failed to create directory: " + quote(File.platform_path(path)))
}
@@ -302,43 +302,13 @@
/* bash */
- private class Limited_Progress(proc: Bash.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 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,
strict: Boolean = true): Process_Result =
{
- with_tmp_file("isabelle_script") { script_file =>
- File.write(script_file, script)
- val proc = Bash.process(cwd, env, false, File.standard_path(script_file))
- proc.stdin.close
-
- val limited = new Limited_Progress(proc, progress_limit)
- val stdout =
- Future.thread("bash_stdout") { File.read_lines(proc.stdout, limited(progress_stdout)) }
- val stderr =
- Future.thread("bash_stderr") { File.read_lines(proc.stderr, limited(progress_stderr)) }
-
- val rc =
- try { proc.join }
- catch { case Exn.Interrupt() => proc.terminate; Exn.Interrupt.return_code }
- if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
-
- Process_Result(rc, out_lines = stdout.join, err_lines = stderr.join)
- }
+ Bash.process(script, cwd, env).result(progress_stdout, progress_stderr, progress_limit, strict)
}
@@ -368,7 +338,7 @@
bash("exec \"$PDF_VIEWER\" '" + File.standard_path(arg) + "' >/dev/null 2>/dev/null &")
def hg(cmd_line: String, cwd: Path = Path.current): Process_Result =
- bash("cd " + File.shell_path(cwd) + " && \"${HG:-hg}\" " + cmd_line)
+ bash("cd " + File.bash_path(cwd) + " && \"${HG:-hg}\" " + cmd_line)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/ml_process.scala Wed Mar 09 21:01:22 2016 +0100
@@ -0,0 +1,115 @@
+/* Title: Pure/System/ml_process.scala
+ Author: Makarius
+
+The underlying ML process.
+*/
+
+package isabelle
+
+
+import java.io.{File => JFile}
+
+
+object ML_Process
+{
+ def apply(options: Options,
+ heap: String = "",
+ args: List[String] = Nil,
+ modes: List[String] = Nil,
+ secure: Boolean = false,
+ cwd: JFile = null,
+ env: Map[String, String] = Map.empty,
+ redirect: Boolean = false,
+ channel: Option[System_Channel] = None): Bash.Process =
+ {
+ val load_heaps =
+ {
+ if (heap == "RAW_ML_SYSTEM") Nil
+ else if (heap.iterator.contains('/')) {
+ val heap_path = Path.explode(heap)
+ if (!heap_path.is_file) error("Bad heap file: " + heap_path)
+ List(heap_path)
+ }
+ else {
+ val dirs = Isabelle_System.find_logics_dirs()
+ val heap_name = if (heap == "") Isabelle_System.getenv_strict("ISABELLE_LOGIC") else heap
+ dirs.map(_ + Path.basic(heap_name)).find(_.is_file) match {
+ case Some(heap_path) => List(heap_path)
+ case None =>
+ error("Unknown logic " + quote(heap) + " -- no heap file found in:\n" +
+ cat_lines(dirs.map(dir => " " + dir.implode)))
+ }
+ }
+ }
+
+ val eval_heaps =
+ load_heaps.map(load_heap =>
+ "(PolyML.SaveState.loadState " + ML_Syntax.print_string_raw(File.platform_path(load_heap)) +
+ "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " +
+ ML_Syntax.print_string_raw(": " + load_heap.toString + "\n") +
+ "); OS.Process.exit OS.Process.failure)")
+
+ val eval_initial =
+ if (load_heaps.isEmpty) {
+ List(
+ if (Platform.is_windows)
+ "fun exit 0 = OS.Process.exit OS.Process.success" +
+ " | exit 1 = OS.Process.exit OS.Process.failure" +
+ " | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))"
+ else
+ "fun exit rc = Posix.Process.exit (Word8.fromInt rc)",
+ "PolyML.Compiler.prompt1 := \"ML> \"",
+ "PolyML.Compiler.prompt2 := \"ML# \"")
+ }
+ else Nil
+
+ val eval_modes =
+ if (modes.isEmpty) Nil
+ else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string_raw _)(modes))
+
+ // options
+ val isabelle_process_options = Isabelle_System.tmp_file("options")
+ File.write(isabelle_process_options, YXML.string_of_body(options.encode))
+ val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
+ val eval_options = if (load_heaps.isEmpty) Nil else List("Options.load_default ()")
+
+ val eval_secure = if (secure) List("Secure.set_secure ()") else Nil
+
+ val eval_process =
+ if (load_heaps.isEmpty)
+ List("PolyML.print_depth 10")
+ else
+ channel match {
+ case None =>
+ List("(default_print_depth 10; Isabelle_Process.init_options ())")
+ case Some(ch) =>
+ List("(default_print_depth 10; Isabelle_Process.init_protocol " +
+ ML_Syntax.print_string_raw(ch.server_name) + ")")
+ }
+
+ // bash
+ val bash_args =
+ Word.explode(Isabelle_System.getenv("ML_OPTIONS")) :::
+ (eval_heaps ::: eval_initial ::: eval_modes ::: eval_options ::: eval_secure ::: eval_process).
+ map(eval => List("--eval", eval)).flatten ::: args
+
+ Bash.process(
+ """
+ [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
+
+ export ISABELLE_PID="$$"
+ export ISABELLE_TMP="$ISABELLE_TMP_PREFIX$ISABELLE_PID"
+ mkdir -p "$ISABELLE_TMP"
+ chmod $(umask -S) "$ISABELLE_TMP"
+
+ librarypath "$ML_HOME"
+ "$ML_HOME/poly" -q """ + File.bash_args(bash_args) + """
+ RC="$?"
+
+ rm -f "$ISABELLE_PROCESS_OPTIONS"
+ rmdir "$ISABELLE_TMP"
+
+ exit "$RC"
+ """, cwd = cwd, env = env ++ env_options, redirect = redirect)
+ }
+}
--- a/src/Pure/System/process_result.scala Wed Mar 09 17:22:43 2016 +0000
+++ b/src/Pure/System/process_result.scala Wed Mar 09 21:01:22 2016 +0100
@@ -10,13 +10,14 @@
rc: Int,
out_lines: List[String] = Nil,
err_lines: List[String] = Nil,
- timeout: Option[Time] = None)
+ timeout: Boolean = false,
+ timing: Timing = Timing.zero)
{
def out: String = cat_lines(out_lines)
def err: String = cat_lines(err_lines)
def error(s: String): Process_Result = copy(err_lines = err_lines ::: List(s))
- def set_timeout(t: Time): Process_Result = copy(rc = 1, timeout = Some(t))
+ def was_timeout: Process_Result = copy(rc = 1, timeout = true)
def ok: Boolean = rc == 0
def interrupted: Boolean = rc == Exn.Interrupt.return_code
@@ -32,4 +33,11 @@
Output.writeln(Library.trim_line(out))
copy(out_lines = Nil, err_lines = Nil)
}
+
+ def print_stdout: Process_Result =
+ {
+ Output.warning(Library.trim_line(err), stdout = true)
+ Output.writeln(Library.trim_line(out), stdout = true)
+ copy(out_lines = Nil, err_lines = Nil)
+ }
}
--- a/src/Pure/Thy/present.ML Wed Mar 09 17:22:43 2016 +0000
+++ b/src/Pure/Thy/present.ML Wed Mar 09 21:01:22 2016 +0100
@@ -35,7 +35,7 @@
val doc_indexN = "session";
val session_graph_path = Path.basic "session_graph.pdf";
-fun show_path path = Path.implode (Path.expand (Path.append (File.pwd ()) path));
+fun show_path path = Path.implode (Path.expand (File.full_path Path.current path));
@@ -216,7 +216,7 @@
fun isabelle_document {verbose, purge} format name tags dir =
let
val s = "\"$ISABELLE_TOOL\" document" ^ (if purge then " -c" else "") ^ " -o '" ^ format ^ "' \
- \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.shell_path dir ^ " 2>&1";
+ \-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 ();
val (out, rc) = Isabelle_System.bash_output s;
@@ -270,7 +270,7 @@
val _ = Isabelle_System.mkdirs doc_dir;
val _ =
Isabelle_System.isabelle_tool "latex"
- ("-o sty " ^ File.shell_path (Path.append doc_dir (Path.basic "root.tex")));
+ ("-o sty " ^ File.bash_path (Path.append doc_dir (Path.basic "root.tex")));
val _ = List.app (fn file => Isabelle_System.copy_file_base file doc_dir) doc_files;
val _ = Isabelle_System.copy_file graph_file (Path.append doc_dir session_graph_path);
val _ = write_tex_index tex_index doc_dir;
@@ -360,8 +360,8 @@
val _ = Isabelle_System.mkdirs doc_path;
val root_path = Path.append doc_path (Path.basic "root.tex");
val _ = Isabelle_System.copy_file (Path.explode "~~/lib/texinputs/draft.tex") root_path;
- val _ = Isabelle_System.isabelle_tool "latex" ("-o sty " ^ File.shell_path root_path);
- val _ = Isabelle_System.isabelle_tool "latex" ("-o syms " ^ File.shell_path root_path);
+ val _ = Isabelle_System.isabelle_tool "latex" ("-o sty " ^ File.bash_path root_path);
+ val _ = Isabelle_System.isabelle_tool "latex" ("-o syms " ^ File.bash_path root_path);
fun known name =
let val ss = split_lines (File.read (Path.append doc_path (Path.basic name)))
@@ -383,7 +383,7 @@
val _ = Isabelle_System.mkdirs target_dir;
val _ = Isabelle_System.copy_file result target;
in
- Isabelle_System.isabelle_tool "display" (File.shell_path target ^ " &")
+ Isabelle_System.isabelle_tool "display" (File.bash_path target ^ " &")
end);
end;
--- a/src/Pure/Tools/build.scala Wed Mar 09 17:22:43 2016 +0000
+++ b/src/Pure/Tools/build.scala Wed Mar 09 21:01:22 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 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)
@@ -621,37 +602,33 @@
strict = false)
}
- def terminate: Unit = result.cancel
- def is_finished: Boolean = result.is_finished
+ def terminate: Unit = future_result.cancel
+ def is_finished: Boolean = future_result.is_finished
- @volatile private var was_timeout: Option[Time] = None
+ @volatile private var was_timeout = false
private val timeout_request: Option[Event_Timer.Request] =
{
- val timeout = info.timeout
- val t0 = Time.now()
- if (timeout > Time.zero)
- Some(Event_Timer.request(t0 + timeout) { terminate; was_timeout = Some(Time.now() - t0) })
+ if (info.timeout > Time.zero)
+ Some(Event_Timer.request(Time.now() + info.timeout) { terminate; was_timeout = true })
else None
}
def join: Process_Result =
{
- val res = result.join
+ val result = future_result.join
- if (res.ok && !is_pure(name))
+ if (result.ok && !is_pure(name))
Present.finish(progress, browser_info, graph_file, info, name)
graph_file.delete
args_file.delete
timeout_request.foreach(_.cancel)
- if (res.interrupted) {
- was_timeout match {
- case Some(t) => res.error(Output.error_text("Timeout")).set_timeout(t)
- case None => res.error(Output.error_text("Interrupt"))
- }
+ if (result.interrupted) {
+ if (was_timeout) result.error(Output.error_text("Timeout")).was_timeout
+ else result.error(Output.error_text("Interrupt"))
}
- else res
+ else result
}
}
@@ -880,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/Pure/Tools/build_console.scala Wed Mar 09 17:22:43 2016 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,58 +0,0 @@
-/* Title: Pure/Tools/build_console.scala
- Author: Makarius
-
-Check and build Isabelle session for console tool.
-*/
-
-package isabelle
-
-
-object Build_Console
-{
- /* build_console */
-
- def build_console(
- options: Options,
- progress: Progress = Ignore_Progress,
- dirs: List[Path] = Nil,
- no_build: Boolean = false,
- system_mode: Boolean = false,
- session: String): Int =
- {
- if (no_build ||
- Build.build(options = options, build_heap = true, no_build = true,
- dirs = dirs, system_mode = system_mode, sessions = List(session)) == 0) 0
- else {
- progress.echo("Build started for Isabelle/" + session + " ...")
- Build.build(options = options, progress = progress, build_heap = true,
- dirs = dirs, system_mode = system_mode, sessions = List(session))
- }
- }
-
-
- /* command line entry point */
-
- def main(args: Array[String])
- {
- Command_Line.tool {
- args.toList match {
- case
- session ::
- Properties.Value.Boolean(no_build) ::
- Properties.Value.Boolean(system_mode) ::
- options_file ::
- Command_Line.Chunks(dirs, system_options) =>
- val options = (Options.init() /: system_options)(_ + _)
- File.write(Path.explode(options_file), YXML.string_of_body(options.encode))
-
- val progress = new Console_Progress()
- progress.interrupt_handler {
- build_console(options, progress,
- dirs.map(Path.explode(_)), no_build, system_mode, session)
- }
- case _ => error("Bad arguments:\n" + cat_lines(args))
- }
- }
- }
-}
-
--- a/src/Pure/Tools/check_sources.scala Wed Mar 09 17:22:43 2016 +0000
+++ b/src/Pure/Tools/check_sources.scala Wed Mar 09 21:01:22 2016 +0100
@@ -41,7 +41,7 @@
def check_hg(root: Path)
{
Output.writeln("Checking " + root + " ...")
- Isabelle_System.hg("--repository " + File.shell_path(root) + " root").check
+ Isabelle_System.hg("--repository " + File.bash_path(root) + " root").check
for {
file <- Isabelle_System.hg("manifest", root).check.out_lines
if file.endsWith(".thy") || file.endsWith(".ML") || file.endsWith("/ROOT")
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/ml_console.scala Wed Mar 09 21:01:22 2016 +0100
@@ -0,0 +1,129 @@
+/* Title: Pure/Tools/ml_console.scala
+ Author: Makarius
+
+Run Isabelle process with raw ML console and line editor.
+*/
+
+package isabelle
+
+
+import java.io.{IOException, BufferedReader, InputStreamReader}
+
+
+object ML_Console
+{
+ /* command line entry point */
+
+ def main(args: Array[String])
+ {
+ Command_Line.tool {
+ var dirs: List[Path] = Nil
+ var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
+ var modes: List[String] = Nil
+ var no_build = false
+ var options = Options.init()
+ var system_mode = false
+
+ val getopts = Getopts("""
+Usage: isabelle console [OPTIONS]
+
+ Options are:
+ -d DIR include session directory
+ -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(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
+ (ISABELLE_LINE_EDITOR=""" + quote(Isabelle_System.getenv("ISABELLE_LINE_EDITOR")) + """.
+""",
+ "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+ "l:" -> (arg => logic = arg),
+ "m:" -> (arg => modes = arg :: modes),
+ "n" -> (arg => no_build = true),
+ "o:" -> (arg => options = options + arg),
+ "r" -> (_ => logic = "RAW_ML_SYSTEM"),
+ "s" -> (_ => system_mode = true))
+
+ val more_args = getopts(args)
+ if (!more_args.isEmpty) getopts.usage()
+
+
+ // build
+ if (!no_build && logic != "RAW_ML_SYSTEM" &&
+ Build.build(options = options, build_heap = true, no_build = true,
+ dirs = dirs, system_mode = system_mode, sessions = List(logic)) != 0)
+ {
+ val progress = new Console_Progress
+ progress.echo("Build started for Isabelle/" + logic + " ...")
+ progress.interrupt_handler {
+ val rc =
+ Build.build(options = options, progress = progress, build_heap = true,
+ dirs = dirs, system_mode = system_mode, sessions = List(logic))
+ if (rc != 0) sys.exit(rc)
+ }
+ }
+
+ // process loop
+ val process =
+ ML_Process(options, heap = logic, args = List("-i"),
+ modes = if (logic == "RAW_ML_SYSTEM") Nil else modes ::: List("ASCII"))
+ val process_output = Future.thread[Unit]("process_output") {
+ try {
+ var result = new StringBuilder(100)
+ var finished = false
+ while (!finished) {
+ var c = -1
+ var done = false
+ while (!done && (result.length == 0 || process.stdout.ready)) {
+ c = process.stdout.read
+ if (c >= 0) result.append(c.asInstanceOf[Char])
+ else done = true
+ }
+ if (result.length > 0) {
+ System.out.print(result.toString)
+ System.out.flush()
+ result.length = 0
+ }
+ else {
+ process.stdout.close()
+ finished = true
+ }
+ }
+ }
+ catch { case e: IOException => case Exn.Interrupt() => }
+ }
+ val process_input = Future.thread[Unit]("process_input") {
+ val reader = new BufferedReader(new InputStreamReader(System.in))
+ POSIX_Interrupt.handler { process.interrupt } {
+ try {
+ var finished = false
+ while (!finished) {
+ reader.readLine() match {
+ case null =>
+ process.stdin.close()
+ finished = true
+ case line =>
+ process.stdin.write(line)
+ process.stdin.write("\n")
+ process.stdin.flush()
+ }
+ }
+ }
+ catch { case e: IOException => case Exn.Interrupt() => }
+ }
+ }
+ val process_result = Future.thread[Int]("process_result") {
+ val rc = process.join
+ process_input.cancel
+ rc
+ }
+
+ process_output.join
+ process_input.join
+ process_result.join
+ }
+ }
+}
--- a/src/Pure/build-jars Wed Mar 09 17:22:43 2016 +0000
+++ b/src/Pure/build-jars Wed Mar 09 21:01:22 2016 +0100
@@ -81,6 +81,7 @@
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
@@ -95,13 +96,13 @@
Thy/thy_syntax.scala
Tools/bibtex.scala
Tools/build.scala
- Tools/build_console.scala
Tools/build_doc.scala
Tools/check_keywords.scala
Tools/check_sources.scala
Tools/debugger.scala
Tools/doc.scala
Tools/main.scala
+ Tools/ml_console.scala
Tools/ml_statistics.scala
Tools/news.scala
Tools/print_operation.scala
--- a/src/Pure/library.ML Wed Mar 09 17:22:43 2016 +0000
+++ b/src/Pure/library.ML Wed Mar 09 21:01:22 2016 +0100
@@ -206,8 +206,6 @@
eqtype stamp
val stamp: unit -> stamp
structure Any: sig type T = exn end
- val cd: string -> unit
- val pwd: unit -> string
val getenv: string -> string
val getenv_strict: string -> string
end;
@@ -1014,12 +1012,6 @@
structure Any = struct type T = exn end;
-(* current directory *)
-
-val cd = OS.FileSys.chDir o ML_System.platform_path;
-val pwd = ML_System.standard_path o OS.FileSys.getDir;
-
-
(* getenv *)
fun getenv x =
--- a/src/Tools/Code/code_ml.ML Wed Mar 09 17:22:43 2016 +0000
+++ b/src/Tools/Code/code_ml.ML Wed Mar 09 21:01:22 2016 +0100
@@ -871,7 +871,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",
--- a/src/Tools/Code/code_target.ML Wed Mar 09 17:22:43 2016 +0000
+++ b/src/Tools/Code/code_target.ML Wed Mar 09 21:01:22 2016 +0100
@@ -348,9 +348,8 @@
fun assert_module_name "" = error "Empty module name not allowed here"
| assert_module_name module_name = module_name;
-fun using_master_directory ctxt =
- Option.map (Path.append (File.pwd ()) o
- Path.append (Resources.master_directory (Proof_Context.theory_of ctxt)));
+val using_master_directory =
+ Option.map o File.full_path o Resources.master_directory o Proof_Context.theory_of;
in
@@ -385,7 +384,7 @@
generatedN args program all_public syms);
val cmd = make_command generatedN;
in
- if Isabelle_System.bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
+ if Isabelle_System.bash ("cd " ^ File.bash_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
then error ("Code check failed for " ^ target_name ^ ": " ^ cmd)
else ()
end;
--- a/src/Tools/cache_io.ML Wed Mar 09 17:22:43 2016 +0000
+++ b/src/Tools/cache_io.ML Wed Mar 09 21:01:22 2016 +0100
@@ -62,7 +62,7 @@
val table =
if File.exists cache_path then
let
- fun err () = error ("Cache IO: corrupted cache file: " ^ File.shell_path cache_path)
+ fun err () = error ("Cache IO: corrupted cache file: " ^ File.bash_path cache_path)
fun int_of_string s =
(case read_int (raw_explode s) of
--- a/src/Tools/jEdit/src/isabelle_logic.scala Wed Mar 09 17:22:43 2016 +0000
+++ b/src/Tools/jEdit/src/isabelle_logic.scala Wed Mar 09 21:01:22 2016 +0100
@@ -69,16 +69,16 @@
dirs = session_dirs(), sessions = List(session_name()))
}
- def session_args(): String =
+ def session_start()
{
- val print_modes =
+ val modes =
(space_explode(',', PIDE.options.string("jedit_print_mode")) :::
- space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).map("-m " + _)
- (print_modes ::: List("-q", File.shell_quote(session_name()))).mkString(" ")
+ space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse
+ PIDE.session.start(receiver =>
+ Isabelle_Process(
+ PIDE.options.value, heap = session_name(), modes = modes, receiver = receiver))
}
- def session_start(): Unit = PIDE.session.start("Isabelle", session_args())
-
def session_dirs(): List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
def session_list(): List[String] =