diff --git a/bin/isabelle_process b/bin/isabelle_process --- a/bin/isabelle_process +++ b/bin/isabelle_process @@ -1,242 +1,231 @@ #!/usr/bin/env bash # # Author: Markus Wenzel, TU Muenchen # # Isabelle process startup script. if [ -L "$0" ]; then TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')" exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@" fi ## 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] [INPUT] [OUTPUT]" 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 " -T ADDR startup process wrapper, with socket address" - echo " -W IN:OUT startup process wrapper, with input/output fifos" echo " -e MLTEXT pass MLTEXT to the ML session" 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 " -r open heap file read-only" echo " -w reset write permissions on OUTPUT" echo echo " INPUT (default \"$ISABELLE_LOGIC\") and OUTPUT specify in/out heaps." echo " These are either names to be searched in the Isabelle path, or" echo " actual file names (containing at least one /)." echo " If INPUT is \"RAW_ML_SYSTEM\", just start the bare bones ML system." echo exit 1 } function fail() { echo "$1" >&2 exit 2 } ## process command line # options OPTIONS_FILE="" +PROCESS_SOCKET="" SECURE="" -WRAPPER_SOCKET="" -WRAPPER_FIFOS="" MLTEXT="" MODES="" declare -a SYSTEM_OPTIONS=() TERMINATE="" READONLY="" NOWRITE="" -while getopts "O:ST:W:e:m:o:qrw" OPT +while getopts "O:P:Se:m:o:qrw" OPT do case "$OPT" in O) OPTIONS_FILE="$OPTARG" ;; + P) + PROCESS_SOCKET="$OPTARG" + ;; S) SECURE=true ;; - T) - WRAPPER_SOCKET="$OPTARG" - ;; - W) - WRAPPER_FIFOS="$OPTARG" - ;; e) MLTEXT="$MLTEXT $OPTARG" ;; m) if [ -z "$MODES" ]; then MODES="\"$OPTARG\"" else MODES="\"$OPTARG\", $MODES" fi ;; o) SYSTEM_OPTIONS["${#SYSTEM_OPTIONS[@]}"]="$OPTARG" ;; q) TERMINATE=true ;; r) READONLY=true ;; w) NOWRITE=true ;; \?) usage ;; esac done shift $(($OPTIND - 1)) # args INPUT="" OUTPUT="" if [ "$#" -ge 1 ]; then INPUT="$1" shift fi if [ "$#" -ge 1 ]; then OUTPUT="$1" shift fi [ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; } ## check ML system [ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle." ## input heap file [ -z "$INPUT" ] && INPUT="$ISABELLE_LOGIC" case "$INPUT" in RAW_ML_SYSTEM) INFILE="" ;; */*) INFILE="$INPUT" [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\"" ;; *) INFILE="" ISA_PATH="" splitarray ":" "$ISABELLE_PATH"; PATHS=("${SPLITARRAY[@]}") for DIR in "${PATHS[@]}" do DIR="$DIR/$ML_IDENTIFIER" ISA_PATH="$ISA_PATH $DIR\n" [ -z "$INFILE" -a -f "$DIR/$INPUT" ] && INFILE="$DIR/$INPUT" done if [ -z "$INFILE" ]; then echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2 echo -ne "$ISA_PATH" >&2 exit 2 fi ;; esac ## output heap file case "$OUTPUT" in "") if [ -z "$READONLY" -a -w "$INFILE" ]; then perl -e "exit (((stat('$INFILE'))[2] & 0222) != 0 ? 0 : 1);" && OUTFILE="$INFILE" fi ;; */*) OUTFILE="$OUTPUT" ;; *) mkdir -p "$ISABELLE_OUTPUT" OUTFILE="$ISABELLE_OUTPUT/$OUTPUT" ;; esac ## 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" ## run it! ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-) [ -n "$MODES" ] && MLTEXT="Unsynchronized.change print_mode (append [$MODES]); $MLTEXT" [ -n "$SECURE" ] && MLTEXT="$MLTEXT; Secure.set_secure ();" -if [ -n "$WRAPPER_SOCKET" ]; then - MLTEXT="$MLTEXT; Isabelle_Process.init_socket \"$WRAPPER_SOCKET\";" -elif [ -n "$WRAPPER_FIFOS" ]; then - splitarray ":" "$WRAPPER_FIFOS"; FIFOS=("${SPLITARRAY[@]}") - [ "${#FIFOS[@]}" -eq 2 ] || fail "Expected IN:OUT fifo specification" - [ -p "${FIFOS[0]}" ] || fail "Bad input fifo: ${FIFOS[0]}" - [ -p "${FIFOS[1]}" ] || fail "Bad output fifo: ${FIFOS[1]}" - MLTEXT="$MLTEXT; Isabelle_Process.init_fifos \"${FIFOS[0]}\" \"${FIFOS[1]}\";" +if [ -n "$PROCESS_SOCKET" ]; then + MLTEXT="$MLTEXT; 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 [ "$INPUT" != RAW_ML_SYSTEM -a "$INPUT" != RAW ]; then MLTEXT="Exn.capture_exit 2 Options.load_default (); $MLTEXT" fi fi export INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_PID ISABELLE_TMP ISABELLE_PROCESS_OPTIONS if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" else "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE" fi RC="$?" [ -n "$ISABELLE_PROCESS_OPTIONS" ] && rm -f "$ISABELLE_PROCESS_OPTIONS" rmdir "$ISABELLE_TMP" exit "$RC" diff --git a/src/Doc/System/Basics.thy b/src/Doc/System/Basics.thy --- a/src/Doc/System/Basics.thy +++ b/src/Doc/System/Basics.thy @@ -1,538 +1,537 @@ theory Basics imports Base begin chapter \The Isabelle system environment\ text \This manual describes Isabelle together with related tools and user interfaces as seen from a system oriented view. See also the \emph{Isabelle/Isar Reference Manual} @{cite "isabelle-isar-ref"} for the actual Isabelle input language and related concepts, and \emph{The Isabelle/Isar Implementation Manual} @{cite "isabelle-implementation"} for the main concepts of the underlying implementation in Isabelle/ML. \medskip The Isabelle system environment provides the following basic infrastructure to integrate tools smoothly. \begin{enumerate} \item The \emph{Isabelle settings} mechanism provides process environment variables to all Isabelle executables (including tools and user interfaces). \item The raw \emph{Isabelle process} (@{executable_ref "isabelle_process"}) runs logic sessions either interactively or in batch mode. In particular, this view abstracts over the invocation of the actual ML system to be used. Regular users rarely need to care about the low-level process. \item The main \emph{Isabelle tool wrapper} (@{executable_ref isabelle}) provides a generic startup environment Isabelle related utilities, user interfaces etc. Such tools automatically benefit from the settings mechanism. \end{enumerate} \ section \Isabelle settings \label{sec:settings}\ text \ The Isabelle system heavily depends on the \emph{settings mechanism}\indexbold{settings}. Essentially, this is a statically scoped collection of environment variables, such as @{setting ISABELLE_HOME}, @{setting ML_SYSTEM}, @{setting ML_HOME}. These variables are \emph{not} intended to be set directly from the shell, though. Isabelle employs a somewhat more sophisticated scheme of \emph{settings files} --- one for site-wide defaults, another for additional user-specific modifications. With all configuration variables in clearly defined places, this scheme is more maintainable and user-friendly than global shell environment variables. In particular, we avoid the typical situation where prospective users of a software package are told to put several things into their shell startup scripts, before being able to actually run the program. Isabelle requires none such administrative chores of its end-users --- the executables can be invoked straight away. Occasionally, users would still want to put the @{file "$ISABELLE_HOME/bin"} directory into their shell's search path, but this is not required. \ subsection \Bootstrapping the environment \label{sec:boot}\ text \Isabelle executables need to be run within a proper settings environment. This is bootstrapped as described below, on the first invocation of one of the outer wrapper scripts (such as @{executable_ref isabelle}). This happens only once for each process tree, i.e.\ the environment is passed to subprocesses according to regular Unix conventions. \begin{enumerate} \item The special variable @{setting_def ISABELLE_HOME} is determined automatically from the location of the binary that has been run. You should not try to set @{setting ISABELLE_HOME} manually. Also note that the Isabelle executables either have to be run from their original location in the distribution directory, or via the executable objects created by the @{tool install} tool. Symbolic links are admissible, but a plain copy of the @{file "$ISABELLE_HOME/bin"} files will not work! \item The file @{file "$ISABELLE_HOME/etc/settings"} is run as a @{executable_ref bash} shell script with the auto-export option for variables enabled. This file holds a rather long list of shell variable assigments, thus providing the site-wide default settings. The Isabelle distribution already contains a global settings file with sensible defaults for most variables. When installing the system, only a few of these may have to be adapted (probably @{setting ML_SYSTEM} etc.). \item The file @{file_unchecked "$ISABELLE_HOME_USER/etc/settings"} (if it exists) is run in the same way as the site default settings. Note that the variable @{setting ISABELLE_HOME_USER} has already been set before --- usually to something like @{verbatim "$USER_HOME/.isabelle/IsabelleXXXX"}. Thus individual users may override the site-wide defaults. Typically, a user settings file contains only a few lines, with some assignments that are actually changed. Never copy the central @{file "$ISABELLE_HOME/etc/settings"} file! \end{enumerate} Since settings files are regular GNU @{executable_def bash} scripts, one may use complex shell commands, such as @{verbatim "if"} or @{verbatim "case"} statements to set variables depending on the system architecture or other environment variables. Such advanced features should be added only with great care, though. In particular, external environment references should be kept at a minimum. \medskip A few variables are somewhat special: \begin{itemize} \item @{setting_def ISABELLE_PROCESS} and @{setting_def ISABELLE_TOOL} are set automatically to the absolute path names of the @{executable "isabelle_process"} and @{executable isabelle} executables, respectively. \item @{setting_ref ISABELLE_OUTPUT} will have the identifiers of the Isabelle distribution (cf.\ @{setting ISABELLE_IDENTIFIER}) and the ML system (cf.\ @{setting ML_IDENTIFIER}) appended automatically to its value. \end{itemize} \medskip Note that the settings environment may be inspected with the @{tool getenv} tool. This might help to figure out the effect of complex settings scripts.\ subsection \Common variables\ text \ This is a reference of common Isabelle settings variables. Note that the list is somewhat open-ended. Third-party utilities or interfaces may add their own selection. Variables that are special in some sense are marked with @{text "\<^sup>*"}. \begin{description} \item[@{setting_def USER_HOME}@{text "\<^sup>*"}] Is the cross-platform user home directory. On Unix systems this is usually the same as @{setting HOME}, but on Windows it is the regular home directory of the user, not the one of within the Cygwin root file-system.\footnote{Cygwin itself offers another choice whether its HOME should point to the \texttt{/home} directory tree or the Windows user home.} \item[@{setting_def ISABELLE_HOME}@{text "\<^sup>*"}] is the location of the top-level Isabelle distribution directory. This is automatically determined from the Isabelle executable that has been invoked. Do not attempt to set @{setting ISABELLE_HOME} yourself from the shell! \item[@{setting_def ISABELLE_HOME_USER}] is the user-specific counterpart of @{setting ISABELLE_HOME}. The default value is relative to @{file_unchecked "$USER_HOME/.isabelle"}, under rare circumstances this may be changed in the global setting file. Typically, the @{setting ISABELLE_HOME_USER} directory mimics @{setting ISABELLE_HOME} to some extend. In particular, site-wide defaults may be overridden by a private @{verbatim "$ISABELLE_HOME_USER/etc/settings"}. \item[@{setting_def ISABELLE_PLATFORM_FAMILY}@{text "\<^sup>*"}] is automatically set to the general platform family: @{verbatim linux}, @{verbatim macos}, @{verbatim windows}. Note that platform-dependent tools usually need to refer to the more specific identification according to @{setting ISABELLE_PLATFORM}, @{setting ISABELLE_PLATFORM32}, @{setting ISABELLE_PLATFORM64}. \item[@{setting_def ISABELLE_PLATFORM}@{text "\<^sup>*"}] is automatically set to a symbolic identifier for the underlying hardware and operating system. The Isabelle platform identification always refers to the 32 bit variant, even this is a 64 bit machine. Note that the ML or Java runtime may have a different idea, depending on which binaries are actually run. \item[@{setting_def ISABELLE_PLATFORM64}@{text "\<^sup>*"}] is similar to @{setting ISABELLE_PLATFORM} but refers to the proper 64 bit variant on a platform that supports this; the value is empty for 32 bit. Note that the following bash expression (including the quotes) prefers the 64 bit platform, if that is available: @{verbatim [display] "\"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}\""} \item[@{setting_def ISABELLE_PROCESS}@{text "\<^sup>*"}, @{setting ISABELLE_TOOL}@{text "\<^sup>*"}] are automatically set to the full path names of the @{executable "isabelle_process"} and @{executable isabelle} executables, respectively. Thus other tools and scripts need not assume that the @{file "$ISABELLE_HOME/bin"} directory is on the current search path of the shell. \item[@{setting_def ISABELLE_IDENTIFIER}@{text "\<^sup>*"}] refers to the name of this Isabelle distribution, e.g.\ ``@{verbatim Isabelle2012}''. \item[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, @{setting_def ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def ML_IDENTIFIER}@{text "\<^sup>*"}] specify the underlying ML system to be used for Isabelle. There is only a fixed set of admissable @{setting ML_SYSTEM} names (see the @{file "$ISABELLE_HOME/etc/settings"} file of the distribution). The actual compiler binary will be run from the directory @{setting ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the command line. The optional @{setting ML_PLATFORM} may specify the binary format of ML heap images, which is useful for cross-platform installations. The value of @{setting ML_IDENTIFIER} is automatically obtained by composing the values of @{setting ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version values. \item[@{setting_def ML_SYSTEM_POLYML}@{text "\<^sup>*"}] is @{verbatim true} for @{setting ML_SYSTEM} values derived from Poly/ML, as opposed to SML/NJ where it is empty. This is particularly useful with the build option @{system_option condition} (\secref{sec:system-options}) to restrict big sessions to something that SML/NJ can still handle. \item[@{setting_def ISABELLE_JDK_HOME}] needs to point to a full JDK (Java Development Kit) installation with @{verbatim javac} and @{verbatim jar} executables. This is essential for Isabelle/Scala and other JVM-based tools to work properly. Note that conventional @{verbatim JAVA_HOME} usually points to the JRE (Java Runtime Environment), not JDK. \item[@{setting_def ISABELLE_PATH}] is a list of directories (separated by colons) where Isabelle logic images may reside. When looking up heaps files, the value of @{setting ML_IDENTIFIER} is appended to each component internally. \item[@{setting_def ISABELLE_OUTPUT}@{text "\<^sup>*"}] is a directory where output heap files should be stored by default. The ML system and Isabelle version identifier is appended here, too. \item[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where theory browser information (HTML text, graph data, and printable documents) is stored (see also \secref{sec:info}). The default value is @{file_unchecked "$ISABELLE_HOME_USER/browser_info"}. \item[@{setting_def ISABELLE_LOGIC}] specifies the default logic to load if none is given explicitely by the user. The default value is @{verbatim HOL}. \item[@{setting_def ISABELLE_LINE_EDITOR}] specifies the line editor for the @{tool_ref console} interface. \item[@{setting_def ISABELLE_LATEX}, @{setting_def ISABELLE_PDFLATEX}, @{setting_def ISABELLE_BIBTEX}] refer to {\LaTeX} related tools for Isabelle document preparation (see also \secref{sec:tool-latex}). \item[@{setting_def ISABELLE_TOOLS}] is a colon separated list of directories that are scanned by @{executable isabelle} for external utility programs (see also \secref{sec:isabelle-tool}). \item[@{setting_def ISABELLE_DOCS}] is a colon separated list of directories with documentation files. \item[@{setting_def PDF_VIEWER}] specifies the program to be used for displaying @{verbatim pdf} files. \item[@{setting_def DVI_VIEWER}] specifies the program to be used for displaying @{verbatim dvi} files. \item[@{setting_def ISABELLE_TMP_PREFIX}@{text "\<^sup>*"}] is the prefix from which any running @{executable "isabelle_process"} derives an individual directory for temporary files. \end{description} \ subsection \Additional components \label{sec:components}\ text \Any directory may be registered as an explicit \emph{Isabelle component}. The general layout conventions are that of the main Isabelle distribution itself, and the following two files (both optional) have a special meaning: \begin{itemize} \item @{verbatim "etc/settings"} holds additional settings that are initialized when bootstrapping the overall Isabelle environment, cf.\ \secref{sec:boot}. As usual, the content is interpreted as a @{verbatim bash} script. It may refer to the component's enclosing directory via the @{verbatim "COMPONENT"} shell variable. For example, the following setting allows to refer to files within the component later on, without having to hardwire absolute paths: \begin{ttbox} MY_COMPONENT_HOME="$COMPONENT" \end{ttbox} Components can also add to existing Isabelle settings such as @{setting_def ISABELLE_TOOLS}, in order to provide component-specific tools that can be invoked by end-users. For example: \begin{ttbox} ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools" \end{ttbox} \item @{verbatim "etc/components"} holds a list of further sub-components of the same structure. The directory specifications given here can be either absolute (with leading @{verbatim "/"}) or relative to the component's main directory. \end{itemize} The root of component initialization is @{setting ISABELLE_HOME} itself. After initializing all of its sub-components recursively, @{setting ISABELLE_HOME_USER} is included in the same manner (if that directory exists). This allows to install private components via @{file_unchecked "$ISABELLE_HOME_USER/etc/components"}, although it is often more convenient to do that programmatically via the @{verbatim init_component} shell function in the @{verbatim "etc/settings"} script of @{verbatim "$ISABELLE_HOME_USER"} (or any other component directory). For example: \begin{ttbox} init_component "$HOME/screwdriver-2.0" \end{ttbox} This is tolerant wrt.\ missing component directories, but might produce a warning. \medskip More complex situations may be addressed by initializing components listed in a given catalog file, relatively to some base directory: \begin{ttbox} init_components "$HOME/my_component_store" "some_catalog_file" \end{ttbox} The component directories listed in the catalog file are treated as relative to the given base directory. See also \secref{sec:tool-components} for some tool-support for resolving components that are formally initialized but not installed yet. \ section \The raw Isabelle process \label{sec:isabelle-process}\ text \ The @{executable_def "isabelle_process"} executable runs bare-bones Isabelle logic sessions --- either interactively or in batch mode. It provides an abstraction over the underlying ML system, and over the actual heap file locations. Its usage is: \begin{ttbox} Usage: isabelle_process [OPTIONS] [INPUT] [OUTPUT] Options are: -O system options from given YXML file + -P SOCKET startup process wrapper via TCP socket -S secure mode -- disallow critical operations - -T ADDR startup process wrapper, with socket address - -W IN:OUT startup process wrapper, with input/output fifos -e MLTEXT pass MLTEXT to the ML session -m MODE add print mode for output -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -q non-interactive session -r open heap file read-only -w reset write permissions on OUTPUT INPUT (default "\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps. These are either names to be searched in the Isabelle path, or actual file names (containing at least one /). If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system. \end{ttbox} Input files without path specifications are looked up in the @{setting ISABELLE_PATH} setting, which may consist of multiple components separated by colons --- these are tried in the given order with the value of @{setting ML_IDENTIFIER} appended internally. In a similar way, base names are relative to the directory specified by @{setting ISABELLE_OUTPUT}. In any case, actual file locations may also be given by including at least one slash (@{verbatim "/"}) in the name (hint: use @{verbatim "./"} to refer to the current directory). \ subsubsection \Options\ text \ If the input heap file does not have write permission bits set, or the @{verbatim "-r"} option is given explicitly, then the session started will be read-only. That is, the ML world cannot be committed back into the image file. Otherwise, a writable session enables commits into either the input file, or into another output heap file (if that is given as the second argument on the command line). The read-write state of sessions is determined at startup only, it cannot be changed intermediately. Also note that heap images may require considerable amounts of disk space (approximately 50--200~MB). Users are responsible for themselves to dispose their heap files when they are no longer needed. \medskip The @{verbatim "-w"} option makes the output heap file read-only after terminating. Thus subsequent invocations cause the logic image to be read-only automatically. \medskip Using the @{verbatim "-e"} option, arbitrary ML code may be passed to the Isabelle session from the command line. Multiple @{verbatim "-e"}'s are evaluated in the given order. Strange things may happen when erroneous ML code is provided. Also make sure that the ML commands are terminated properly by semicolon. \medskip The @{verbatim "-m"} option adds identifiers of print modes to be made active for this session. Typically, this is used by some user interface, e.g.\ to enable output of proper mathematical symbols. \medskip Isabelle normally enters an interactive top-level loop (after processing the @{verbatim "-e"} texts). The @{verbatim "-q"} option inhibits interaction, thus providing a pure batch mode facility. \medskip Option @{verbatim "-o"} allows to override Isabelle system options for this process, see also \secref{sec:system-options}. Alternatively, option @{verbatim "-O"} specifies the full environment of system options as a file in YXML format (according to the Isabelle/Scala function @{verbatim isabelle.Options.encode}). - \medskip The @{verbatim "-T"} or @{verbatim "-W"} option makes - Isabelle enter a special process wrapper for interaction via - Isabelle/Scala, see also @{file - "~~/src/Pure/System/isabelle_process.scala"}. The protocol between - the ML and JVM process is private to the implementation. + \medskip The @{verbatim "-P"} option starts the Isabelle process wrapper + for Isabelle/Scala, with a private protocol running over the specified TCP + socket. Isabelle/ML and Isabelle/Scala provide various programming + interfaces to invoke protocol functions over untyped strings and XML + trees. \medskip The @{verbatim "-S"} option makes the Isabelle process more secure by disabling some critical operations, notably runtime compilation and evaluation of ML source code. \ subsubsection \Examples\ text \ Run an interactive session of the default object-logic (as specified by the @{setting ISABELLE_LOGIC} setting) like this: \begin{ttbox} isabelle_process \end{ttbox} Usually @{setting ISABELLE_LOGIC} refers to one of the standard logic images, which are read-only by default. A writable session --- based on @{verbatim HOL}, but output to @{verbatim Test} (in the directory specified by the @{setting ISABELLE_OUTPUT} setting) --- may be invoked as follows: \begin{ttbox} isabelle_process HOL Test \end{ttbox} Ending this session normally (e.g.\ by typing control-D) dumps the whole ML system state into @{verbatim Test} (be prepared for more than 100\,MB): The @{verbatim Test} session may be continued later (still in writable state) by: \begin{ttbox} isabelle_process Test \end{ttbox} A read-only @{verbatim Test} session may be started by: \begin{ttbox} isabelle_process -r Test \end{ttbox} \bigskip The next example demonstrates batch execution of Isabelle. We retrieve the @{verbatim Main} theory value from the theory loader within ML (observe the delicate quoting rules for the Bash shell vs.\ ML): \begin{ttbox} isabelle_process -e 'Thy_Info.get_theory "Main";' -q -r HOL \end{ttbox} Note that the output text will be interspersed with additional junk messages by the ML runtime environment. The @{verbatim "-W"} option allows to communicate with the Isabelle process via an external program in a more robust fashion. \ section \The Isabelle tool wrapper \label{sec:isabelle-tool}\ text \ All Isabelle related tools and interfaces are called via a common wrapper --- @{executable isabelle}: \begin{ttbox} Usage: isabelle TOOL [ARGS ...] Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help. Available tools: \dots \end{ttbox} In principle, Isabelle tools are ordinary executable scripts that are run within the Isabelle settings environment, see \secref{sec:settings}. The set of available tools is collected by @{executable isabelle} from the directories listed in the @{setting ISABELLE_TOOLS} setting. Do not try to call the scripts directly from the shell. Neither should you add the tool directories to your shell's search path! \ subsubsection \Examples\ text \Show the list of available documentation of the Isabelle distribution: \begin{ttbox} isabelle doc \end{ttbox} View a certain document as follows: \begin{ttbox} isabelle doc system \end{ttbox} Query the Isabelle settings environment: \begin{ttbox} isabelle getenv ISABELLE_HOME_USER \end{ttbox} \ end \ No newline at end of file diff --git a/src/Pure/System/isabelle_process.ML b/src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML +++ b/src/Pure/System/isabelle_process.ML @@ -1,214 +1,210 @@ (* Title: Pure/System/isabelle_process.ML Author: Makarius Isabelle process wrapper. *) signature ISABELLE_PROCESS = sig val is_active: unit -> bool val protocol_command: string -> (string list -> unit) -> unit val reset_tracing: Document_ID.exec -> unit val crashes: exn list Synchronized.var - val init_fifos: string -> string -> unit - val init_socket: string -> unit + val init: string -> unit end; structure Isabelle_Process: ISABELLE_PROCESS = struct (* print mode *) val isabelle_processN = "isabelle_process"; fun is_active () = Print_Mode.print_mode_active isabelle_processN; val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape; val _ = Markup.add_mode isabelle_processN YXML.output_markup; (* protocol commands *) local val commands = Synchronized.var "Isabelle_Process.commands" (Symtab.empty: (string list -> unit) Symtab.table); in fun protocol_command name cmd = Synchronized.change commands (fn cmds => (if not (Symtab.defined cmds name) then () else warning ("Redefining Isabelle protocol command " ^ quote name); Symtab.update (name, cmd) cmds)); fun run_command name args = (case Symtab.lookup (Synchronized.value commands) name of NONE => error ("Undefined Isabelle protocol command " ^ quote name) | SOME cmd => (Runtime.exn_trace_system (fn () => cmd args) handle _ (*sic!*) => error ("Isabelle protocol command failure: " ^ quote name))); end; (* restricted tracing messages *) val tracing_messages = Synchronized.var "tracing_messages" (Inttab.empty: int Inttab.table); fun reset_tracing exec_id = Synchronized.change tracing_messages (Inttab.delete_safe exec_id); fun update_tracing () = (case Position.parse_id (Position.thread_data ()) of NONE => () | SOME exec_id => let val ok = Synchronized.change_result tracing_messages (fn tab => let val n = the_default 0 (Inttab.lookup tab exec_id) + 1; val ok = n <= Options.default_int "editor_tracing_messages"; in (ok, Inttab.update (exec_id, n) tab) end); in if ok then () else let val (text, promise) = Active.dialog_text (); val _ = writeln ("Tracing paused. " ^ text "Stop" ^ ", or continue with next " ^ text "100" ^ ", " ^ text "1000" ^ ", " ^ text "10000" ^ " messages?") val m = Markup.parse_int (Future.join promise) handle Fail _ => error "Stopped"; in Synchronized.change tracing_messages (Inttab.map_default (exec_id, 0) (fn k => k - m)) end end); (* output channels *) val serial_props = Markup.serial_properties o serial; fun init_channels channel = let val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF); val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF); val msg_channel = Message_Channel.make channel; fun message name props body = Message_Channel.send msg_channel (Message_Channel.message name props body); fun standard_message props name body = if forall (fn s => s = "") body then () else let val props' = (case (Properties.defined props Markup.idN, Position.get_id (Position.thread_data ())) of (false, SOME id') => props @ [(Markup.idN, id')] | _ => props); in message name props' body end; in Output.status_fn := standard_message [] Markup.statusN; Output.report_fn := standard_message [] Markup.reportN; Output.result_fn := (fn props => fn s => standard_message (props @ serial_props ()) Markup.resultN s); Output.writeln_fn := (fn s => standard_message (serial_props ()) Markup.writelnN s); Output.state_fn := (fn s => standard_message (serial_props ()) Markup.stateN s); Output.information_fn := (fn s => standard_message (serial_props ()) Markup.informationN s); Output.tracing_fn := (fn s => (update_tracing (); standard_message (serial_props ()) Markup.tracingN s)); Output.warning_fn := (fn s => standard_message (serial_props ()) Markup.warningN s); Output.legacy_fn := (fn s => standard_message (serial_props ()) Markup.legacyN s); Output.error_message_fn := (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s); Output.system_message_fn := message Markup.systemN []; Output.protocol_message_fn := message Markup.protocolN; message Markup.initN [] [Session.welcome ()]; msg_channel end; (* protocol loop -- uninterruptible *) val crashes = Synchronized.var "Isabelle_Process.crashes" ([]: exn list); local fun recover crash = (Synchronized.change crashes (cons crash); Output.physical_stderr "Recovered from Isabelle process crash -- see also Isabelle_Process.crashes\n"); fun read_chunk channel len = let val n = (case Int.fromString len of SOME n => n | NONE => error ("Isabelle process: malformed header " ^ quote len)); val chunk = System_Channel.inputN channel n; val i = size chunk; in if i <> n then error ("Isabelle process: bad chunk (unexpected EOF after " ^ string_of_int i ^ " of " ^ string_of_int n ^ " bytes)") else chunk end; fun read_command channel = System_Channel.input_line channel |> Option.map (fn line => map (read_chunk channel) (space_explode "," line)); fun task_context e = Future.task_context "Isabelle_Process.loop" (Future.new_group NONE) e (); in fun loop channel = let val continue = (case read_command channel of NONE => false | SOME [] => (Output.system_message "Isabelle process: no input"; true) | SOME (name :: args) => (task_context (fn () => run_command name args); true)) handle exn => (Runtime.exn_system_message exn handle crash => recover crash; true); in if continue then loop channel else (Future.shutdown (); Execution.reset (); ()) end; end; (* init *) 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 rendezvous => +val init = uninterruptible (fn _ => fn socket => let val _ = SHA1_Samples.test () handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); reraise exn); val _ = Output.physical_stderr Symbol.STX; val _ = Printer.show_markup_default := true; val _ = Context.set_thread_data NONE; val _ = Unsynchronized.change print_mode (fn mode => (mode @ default_modes1) |> fold (update op =) default_modes2); - val channel = rendezvous (); + val channel = System_Channel.rendezvous socket; val msg_channel = init_channels channel; val _ = Session.init_protocol_handlers (); val _ = loop channel; in Message_Channel.shutdown msg_channel end); -fun init_fifos fifo1 fifo2 = init (fn () => System_Channel.fifo_rendezvous fifo1 fifo2); -fun init_socket name = init (fn () => System_Channel.socket_rendezvous name); - end; diff --git a/src/Pure/System/system_channel.ML b/src/Pure/System/system_channel.ML --- a/src/Pure/System/system_channel.ML +++ b/src/Pure/System/system_channel.ML @@ -1,79 +1,51 @@ (* Title: Pure/System/system_channel.ML Author: Makarius -Portable system channel for inter-process communication, based on -named pipes or sockets. +Socket-based system channel for inter-process communication. *) signature SYSTEM_CHANNEL = sig type T val input_line: T -> string option val inputN: T -> int -> string val output: T -> string -> unit val flush: T -> unit - val fifo_rendezvous: string -> string -> T - val socket_rendezvous: string -> T + val rendezvous: string -> T end; structure System_Channel: SYSTEM_CHANNEL = struct -datatype T = System_Channel of - {input_line: unit -> string option, - inputN: int -> string, - output: string -> unit, - flush: unit -> unit}; - -fun input_line (System_Channel {input_line = f, ...}) = f (); -fun inputN (System_Channel {inputN = f, ...}) n = f n; -fun output (System_Channel {output = f, ...}) s = f s; -fun flush (System_Channel {flush = f, ...}) = f (); - - -(* named pipes *) +datatype T = System_Channel of BinIO.instream * BinIO.outstream; -fun fifo_rendezvous fifo1 fifo2 = - let - val in_stream = TextIO.openIn fifo1; - val out_stream = TextIO.openOut fifo2; - val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream out_stream, IO.BLOCK_BUF); - in - System_Channel - {input_line = fn () => TextIO.inputLine in_stream, - inputN = fn n => TextIO.inputN (in_stream, n), - output = fn s => TextIO.output (out_stream, s), - flush = fn () => TextIO.flushOut out_stream} - end; - - -(* sockets *) - -fun read_line in_stream = +fun input_line (System_Channel (in_stream, _)) = let fun result cs = String.implode (rev (#"\n" :: cs)); fun read cs = (case BinIO.input1 in_stream of NONE => if null cs then NONE else SOME (result cs) | SOME b => (case Byte.byteToChar b of #"\n" => SOME (result cs) | c => read (c :: cs))); in read [] end; -fun socket_rendezvous name = +fun inputN (System_Channel (in_stream, _)) n = + if n = 0 then "" (*workaround for polyml-5.5.1 or earlier*) + else Byte.bytesToString (BinIO.inputN (in_stream, n)); + +fun output (System_Channel (_, out_stream)) s = + BinIO.output (out_stream, Byte.stringToBytes s); + +fun flush (System_Channel (_, out_stream)) = + BinIO.flushOut out_stream; + +fun rendezvous name = let val (in_stream, out_stream) = Socket_IO.open_streams name; val _ = BinIO.StreamIO.setBufferMode (BinIO.getOutstream out_stream, IO.BLOCK_BUF); - in - System_Channel - {input_line = fn () => read_line in_stream, - inputN = fn n => - if n = 0 then "" (*workaround for polyml-5.5.1 or earlier*) - else Byte.bytesToString (BinIO.inputN (in_stream, n)), - output = fn s => BinIO.output (out_stream, Byte.stringToBytes s), - flush = fn () => BinIO.flushOut out_stream} - end; + in System_Channel (in_stream, out_stream) end; end; diff --git a/src/Pure/System/system_channel.scala b/src/Pure/System/system_channel.scala --- a/src/Pure/System/system_channel.scala +++ b/src/Pure/System/system_channel.scala @@ -1,94 +1,35 @@ /* Title: Pure/System/system_channel.scala Author: Makarius -Portable system channel for inter-process communication, based on -named pipes or sockets. +Socket-based system channel for inter-process communication. */ package isabelle -import java.io.{InputStream, OutputStream, File => JFile, FileInputStream, - FileOutputStream, IOException} +import java.io.{InputStream, OutputStream} import java.net.{ServerSocket, InetAddress} object System_Channel { - def apply(): System_Channel = new Socket_Channel - // FIXME if (Platform.is_windows) new Socket_Channel else new Fifo_Channel -} - -abstract class System_Channel -{ - def params: List[String] - def prover_args: List[String] - def rendezvous(): (OutputStream, InputStream) - def accepted(): Unit -} - - -/** named pipes **/ - -private object Fifo_Channel -{ - private val next_fifo = Counter.make() + def apply(): System_Channel = new System_Channel } -private class Fifo_Channel extends System_Channel -{ - require(!Platform.is_windows) - - private def mk_fifo(): String = - { - val i = Fifo_Channel.next_fifo() - val script = - "FIFO=\"${TMPDIR:-/tmp}/isabelle-fifo-${PPID}-$$" + i + "\"\n" + - "echo -n \"$FIFO\"\n" + - "mkfifo -m 600 \"$FIFO\"\n" - val result = Isabelle_System.bash(script) - if (result.rc == 0) result.out else error(result.err) - } - - private def rm_fifo(fifo: String): Boolean = (new JFile(fifo)).delete - - private def fifo_input_stream(fifo: String): InputStream = new FileInputStream(fifo) - private def fifo_output_stream(fifo: String): OutputStream = new FileOutputStream(fifo) - - private val fifo1 = mk_fifo() - private val fifo2 = mk_fifo() - - def params: List[String] = List(fifo1, fifo2) - - val prover_args: List[String] = List ("-W", fifo1 + ":" + fifo2) - - def rendezvous(): (OutputStream, InputStream) = - { - val output_stream = fifo_output_stream(fifo1) - val input_stream = fifo_input_stream(fifo2) - (output_stream, input_stream) - } - - def accepted() { rm_fifo(fifo1); rm_fifo(fifo2) } -} - - -/** sockets **/ - -private class Socket_Channel extends System_Channel +class System_Channel private { private val server = new ServerSocket(0, 2, InetAddress.getByName("127.0.0.1")) def params: List[String] = List("127.0.0.1", server.getLocalPort.toString) - def prover_args: List[String] = List("-T", "127.0.0.1:" + server.getLocalPort) + def prover_args: List[String] = List("-P", "127.0.0.1:" + server.getLocalPort) def rendezvous(): (OutputStream, InputStream) = { val socket = server.accept socket.setTcpNoDelay(true) (socket.getOutputStream, socket.getInputStream) } def accepted() { server.close } }