# HG changeset patch # User wenzelm # Date 1281370712 -7200 # Node ID 3d4e521014f74484c965fe6cd311e533698ec749 # Parent 175a5b4b2c941d7c284c88b630772cb608eb04f1 Isabelle_Process: separate input fifo for commands (still using the old tty protocol); some partial workarounds for Cygwin; diff -r 175a5b4b2c94 -r 3d4e521014f7 bin/isabelle-process --- a/bin/isabelle-process Mon Aug 09 13:56:02 2010 +0200 +++ b/bin/isabelle-process Mon Aug 09 18:18:32 2010 +0200 @@ -29,8 +29,8 @@ echo " -I startup Isar interaction mode" echo " -P startup Proof General interaction mode" echo " -S secure mode -- disallow critical operations" + echo " -W IN:OUT startup process wrapper, with input/output fifos" echo " -X startup PGIP interaction mode" - echo " -W OUTPUT startup process wrapper, with messages going to OUTPUT stream" echo " -e MLTEXT pass MLTEXT to the ML session" echo " -f pass 'Session.finish();' to the ML session" echo " -m MODE add print mode for output" @@ -61,7 +61,7 @@ ISAR=false PROOFGENERAL="" SECURE="" -WRAPPER_OUTPUT="" +WRAPPER_FIFOS="" PGIP="" MLTEXT="" MODES="" @@ -82,7 +82,7 @@ SECURE=true ;; W) - WRAPPER_OUTPUT="$OPTARG" + WRAPPER_FIFOS="$OPTARG" ;; X) PGIP=true @@ -212,9 +212,13 @@ [ -n "$SECURE" ] && MLTEXT="$MLTEXT Secure.set_secure ();" NICE="nice" -if [ -n "$WRAPPER_OUTPUT" ]; then - [ "$WRAPPER_OUTPUT" = "-" -o -p "$WRAPPER_OUTPUT" ] || fail "Bad named pipe: $WRAPPER_OUTPUT" - MLTEXT="$MLTEXT; Isabelle_Process.init \"$WRAPPER_OUTPUT\";" + +if [ -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[0]}\" \"${FIFOS[1]}\";" elif [ -n "$PGIP" ]; then MLTEXT="$MLTEXT; ProofGeneralPgip.init_pgip $ISAR;" elif [ -n "$PROOFGENERAL" ]; then diff -r 175a5b4b2c94 -r 3d4e521014f7 doc-src/System/Thy/Basics.thy --- a/doc-src/System/Thy/Basics.thy Mon Aug 09 13:56:02 2010 +0200 +++ b/doc-src/System/Thy/Basics.thy Mon Aug 09 18:18:32 2010 +0200 @@ -331,7 +331,7 @@ -I startup Isar interaction mode -P startup Proof General interaction mode -S secure mode -- disallow critical operations - -W OUTPUT startup process wrapper, with messages going to OUTPUT stream + -W IN:OUT startup process wrapper, with input/output fifos -X startup PGIP interaction mode -e MLTEXT pass MLTEXT to the ML session -f pass 'Session.finish();' to the ML session @@ -406,12 +406,13 @@ interaction mode on startup, instead of the primitive ML top-level. The @{verbatim "-P"} option configures the top-level loop for interaction with the Proof General user interface, and the - @{verbatim "-X"} option enables XML-based PGIP communication. The - @{verbatim "-W"} option makes Isabelle enter a special process - wrapper for interaction via an external program; the protocol is a - stripped-down version of Proof General the interaction mode, see - also @{"file" "~~/src/Pure/System/isabelle_process.ML"} and @{"file" - "~~/src/Pure/System/isabelle_process.scala"}. + @{verbatim "-X"} option enables XML-based PGIP communication. + + \medskip The @{verbatim "-W"} option makes Isabelle enter a special + process wrapper for interaction via the Isabelle/Scala layer, 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 "-S"} option makes the Isabelle process more secure by disabling some critical operations, notably runtime diff -r 175a5b4b2c94 -r 3d4e521014f7 doc-src/System/Thy/document/Basics.tex --- a/doc-src/System/Thy/document/Basics.tex Mon Aug 09 13:56:02 2010 +0200 +++ b/doc-src/System/Thy/document/Basics.tex Mon Aug 09 18:18:32 2010 +0200 @@ -344,7 +344,7 @@ -I startup Isar interaction mode -P startup Proof General interaction mode -S secure mode -- disallow critical operations - -W OUTPUT startup process wrapper, with messages going to OUTPUT stream + -W IN:OUT startup process wrapper, with input/output fifos -X startup PGIP interaction mode -e MLTEXT pass MLTEXT to the ML session -f pass 'Session.finish();' to the ML session @@ -419,11 +419,13 @@ interaction mode on startup, instead of the primitive ML top-level. The \verb|-P| option configures the top-level loop for interaction with the Proof General user interface, and the - \verb|-X| option enables XML-based PGIP communication. The - \verb|-W| option makes Isabelle enter a special process - wrapper for interaction via an external program; the protocol is a - stripped-down version of Proof General the interaction mode, see - also \hyperlink{file.~~/src/Pure/System/isabelle-process.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}System{\isacharslash}isabelle{\isacharunderscore}process{\isachardot}ML}}}} and \hyperlink{file.~~/src/Pure/System/isabelle-process.scala}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}System{\isacharslash}isabelle{\isacharunderscore}process{\isachardot}scala}}}}. + \verb|-X| option enables XML-based PGIP communication. + + \medskip The \verb|-W| option makes Isabelle enter a special + process wrapper for interaction via the Isabelle/Scala layer, see + also \hyperlink{file.~~/src/Pure/System/isabelle-process.scala}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}System{\isacharslash}isabelle{\isacharunderscore}process{\isachardot}scala}}}}. The + protocol between the ML and JVM process is private to the + implementation. \medskip The \verb|-S| option makes the Isabelle process more secure by disabling some critical operations, notably runtime diff -r 175a5b4b2c94 -r 3d4e521014f7 lib/Tools/mkfifo --- a/lib/Tools/mkfifo Mon Aug 09 13:56:02 2010 +0200 +++ b/lib/Tools/mkfifo Mon Aug 09 18:18:32 2010 +0200 @@ -28,6 +28,8 @@ [ "$#" != 0 ] && usage +#FIXME potential race condition wrt. future processes with same pid FIFO="/tmp/isabelle-fifo$$" -mkfifo -m 600 "$FIFO" || fail "Failed to create named pipe $FIFO" + +mkfifo -m 600 "$FIFO" || fail "Failed to create fifo: $FIFO" echo "$FIFO" diff -r 175a5b4b2c94 -r 3d4e521014f7 src/Pure/General/source.ML --- a/src/Pure/General/source.ML Mon Aug 09 13:56:02 2010 +0200 +++ b/src/Pure/General/source.ML Mon Aug 09 18:18:32 2010 +0200 @@ -19,7 +19,7 @@ val exhausted: ('a, 'b) source -> ('a, 'a list) source val of_string: string -> (string, string list) source val of_string_limited: int -> string -> (string, substring) source - val tty: (string, unit) source + val tty: TextIO.instream -> (string, unit) source val source': 'a -> 'b Scan.stopper -> ('a * 'b list -> 'c list * ('a * 'b list)) -> (bool * (string -> 'a * 'b list -> 'c list * ('a * 'b list))) option -> ('b, 'e) source -> ('c, 'a * ('b, 'e) source) source @@ -129,11 +129,11 @@ | SOME _ => TextIO.input instream :: slurp ()); in maps explode (slurp ()) end; -val tty = make_source [] () default_prompt (fn prompt => fn () => - let val input = slurp_input TextIO.stdIn in +fun tty in_stream = make_source [] () default_prompt (fn prompt => fn () => + let val input = slurp_input in_stream in if exists (fn c => c = "\n") input then (input, ()) else - (case (Output.prompt prompt; TextIO.inputLine TextIO.stdIn) of + (case (Output.prompt prompt; TextIO.inputLine in_stream) of SOME line => (input @ explode line, ()) | NONE => (input, ())) end); diff -r 175a5b4b2c94 -r 3d4e521014f7 src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Mon Aug 09 13:56:02 2010 +0200 +++ b/src/Pure/Isar/outer_syntax.ML Mon Aug 09 18:18:32 2010 +0200 @@ -29,7 +29,7 @@ val parse: Position.T -> string -> Toplevel.transition list val process_file: Path.T -> theory -> theory type isar - val isar: bool -> isar + val isar: TextIO.instream -> bool -> isar val prepare_command: Position.T -> string -> Toplevel.transition val load_thy: string -> (unit -> theory) -> Position.T -> string -> (unit -> unit) * theory end; @@ -222,8 +222,8 @@ Source.source) Source.source) Source.source) Source.source) Source.source) Source.source) Source.source) Source.source; -fun isar term : isar = - Source.tty +fun isar in_stream term : isar = + Source.tty in_stream |> Symbol.source {do_recover = true} |> Token.source {do_recover = SOME true} Keyword.get_lexicons Position.none |> toplevel_source term (SOME true) get_command; diff -r 175a5b4b2c94 -r 3d4e521014f7 src/Pure/ProofGeneral/proof_general_emacs.ML --- a/src/Pure/ProofGeneral/proof_general_emacs.ML Mon Aug 09 13:56:02 2010 +0200 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Mon Aug 09 18:18:32 2010 +0200 @@ -245,7 +245,8 @@ sync_thy_loader (); Unsynchronized.change print_mode (update (op =) proof_generalN); Secure.PG_setup (); - Isar.toplevel_loop {init = true, welcome = true, sync = true, secure = Secure.is_secure ()}); + Isar.toplevel_loop TextIO.stdIn + {init = true, welcome = true, sync = true, secure = Secure.is_secure ()}); (* fake old ThyLoad -- with new semantics *) diff -r 175a5b4b2c94 -r 3d4e521014f7 src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Aug 09 13:56:02 2010 +0200 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Aug 09 18:18:32 2010 +0200 @@ -1000,7 +1000,8 @@ val xmlP = XML.parse_comments |-- XML.parse_element >> single - val tty_src = Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE Source.tty) + val tty_src = + Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE (Source.tty TextIO.stdIn)) fun pgip_toplevel x = loop true x end diff -r 175a5b4b2c94 -r 3d4e521014f7 src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Mon Aug 09 13:56:02 2010 +0200 +++ b/src/Pure/System/isabelle_process.ML Mon Aug 09 18:18:32 2010 +0200 @@ -11,7 +11,7 @@ signature ISABELLE_PROCESS = sig val isabelle_processN: string - val init: string -> unit + val init: string -> string -> unit end; structure Isabelle_Process: ISABELLE_PROCESS = @@ -60,13 +60,19 @@ (OS.Process.sleep (Time.fromMilliseconds 50); try TextIO.flushOut stream; loop ()); in loop end; +fun rendezvous f fifo = + let + val path = File.platform_path (Path.explode fifo); + val result = f fifo; (*block until peer is ready*) + val _ = OS.FileSys.remove path; (*ready; prevent future access -- potential race condition*) + in result end; + in -fun setup_channels out = +fun setup_channels in_fifo out_fifo = let - val path = File.platform_path (Path.explode out); - val out_stream = TextIO.openOut path; (*fifo blocks until reader is ready*) - val _ = OS.FileSys.remove path; (*prevent alien access, indicate writer is ready*) + val in_stream = rendezvous TextIO.openIn in_fifo; + val out_stream = rendezvous TextIO.openOut out_fifo; val _ = Simple_Thread.fork false (auto_flush out_stream); val _ = Simple_Thread.fork false (auto_flush TextIO.stdOut); val _ = Simple_Thread.fork false (auto_flush TextIO.stdErr); @@ -80,7 +86,7 @@ Output.debug_fn := standard_message out_stream "H"; Output.priority_fn := ! Output.writeln_fn; Output.prompt_fn := ignore; - out_stream + (in_stream, out_stream) end; end; @@ -88,13 +94,15 @@ (* init *) -fun init out = - (Unsynchronized.change print_mode - (fold (update op =) [isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]); - setup_channels out |> init_message; - quick_and_dirty := true; (* FIXME !? *) - Keyword.status (); - Output.status (Markup.markup Markup.ready ""); - Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true}); +fun init in_fifo out_fifo = + let + val _ = Unsynchronized.change print_mode + (fold (update op =) [isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]); + val (in_stream, out_stream) = setup_channels in_fifo out_fifo; + val _ = init_message out_stream; + val _ = quick_and_dirty := true; (* FIXME !? *) + val _ = Keyword.status (); + val _ = Output.status (Markup.markup Markup.ready ""); + in Isar.toplevel_loop in_stream {init = true, welcome = false, sync = true, secure = true} end; end; diff -r 175a5b4b2c94 -r 3d4e521014f7 src/Pure/System/isabelle_process.scala --- a/src/Pure/System/isabelle_process.scala Mon Aug 09 13:56:02 2010 +0200 +++ b/src/Pure/System/isabelle_process.scala Mon Aug 09 18:18:32 2010 +0200 @@ -178,11 +178,14 @@ } - /* stdin */ + /* commands */ - private class Stdin_Thread(out_stream: OutputStream) extends Thread("isabelle: stdin") { - override def run() = { - val writer = new BufferedWriter(new OutputStreamWriter(out_stream, Standard_System.charset)) + private class Command_Thread(fifo: String) extends Thread("isabelle: commands") + { + override def run() + { + val stream = system.fifo_output_stream(fifo) + val writer = new BufferedWriter(new OutputStreamWriter(stream, Standard_System.charset)) var finished = false while (!finished) { try { @@ -200,19 +203,21 @@ //}}} } catch { - case e: IOException => put_result(Markup.SYSTEM, "Stdin thread: " + e.getMessage) + case e: IOException => put_result(Markup.SYSTEM, "Command thread: " + e.getMessage) } } - put_result(Markup.SYSTEM, "Stdin thread terminated") + put_result(Markup.SYSTEM, "Command thread terminated") } } - /* stdout */ + /* raw stdout */ - private class Stdout_Thread(in_stream: InputStream) extends Thread("isabelle: stdout") { - override def run() = { - val reader = new BufferedReader(new InputStreamReader(in_stream, Standard_System.charset)) + private class Stdout_Thread(stream: InputStream) extends Thread("isabelle: stdout") + { + override def run() = + { + val reader = new BufferedReader(new InputStreamReader(stream, Standard_System.charset)) var result = new StringBuilder(100) var finished = false @@ -253,7 +258,7 @@ private class Protocol_Error(msg: String) extends Exception(msg) override def run() { - val stream = system.fifo_stream(fifo) + val stream = system.fifo_input_stream(fifo) val default_buffer = new Array[Byte](65536) var c = -1 @@ -329,43 +334,44 @@ /** main **/ { - /* messages */ + /* private communication channels */ - val message_fifo = system.mk_fifo() - def rm_fifo() = system.rm_fifo(message_fifo) + val in_fifo = system.mk_fifo() + val out_fifo = system.mk_fifo() + def rm_fifos() = { system.rm_fifo(in_fifo); system.rm_fifo(out_fifo) } - val message_thread = new Message_Thread(message_fifo) + val command_thread = new Command_Thread(in_fifo) + val message_thread = new Message_Thread(out_fifo) + + command_thread.start message_thread.start /* exec process */ try { - val cmdline = List(system.getenv_strict("ISABELLE_PROCESS"), "-W", message_fifo) ++ args + val cmdline = + List(system.getenv_strict("ISABELLE_PROCESS"), "-W", in_fifo + ":" + out_fifo) ++ args proc = system.execute(true, cmdline: _*) } catch { case e: IOException => - rm_fifo() + rm_fifos() error("Failed to execute Isabelle process: " + e.getMessage) } - - - /* stdin/stdout */ - - new Stdin_Thread(proc.getOutputStream).start new Stdout_Thread(proc.getInputStream).start /* exit */ new Thread("isabelle: exit") { - override def run() = { + override def run() + { val rc = proc.waitFor() Thread.sleep(300) // FIXME property!? put_result(Markup.SYSTEM, "Exit thread terminated") put_result(Markup.EXIT, rc.toString) - rm_fifo() + rm_fifos() } }.start } diff -r 175a5b4b2c94 -r 3d4e521014f7 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Mon Aug 09 13:56:02 2010 +0200 +++ b/src/Pure/System/isabelle_system.scala Mon Aug 09 18:18:32 2010 +0200 @@ -8,9 +8,8 @@ import java.util.regex.Pattern import java.util.Locale -import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, - BufferedInputStream, FileInputStream, BufferedReader, InputStreamReader, - File, IOException} +import java.io.{BufferedInputStream, FileInputStream, BufferedOutputStream, FileOutputStream, + OutputStream, File, IOException} import java.awt.{GraphicsEnvironment, Font} import java.awt.font.TextAttribute @@ -288,11 +287,12 @@ if (rc != 0) error(result) } - def fifo_stream(fifo: String): BufferedInputStream = + def fifo_input_stream(fifo: String): BufferedInputStream = { - // blocks until writer is ready + // block until peer is ready val stream = if (Platform.is_windows) { + // Cygwin fifo as Windows/Java input stream val proc = execute(false, "cat", fifo) proc.getOutputStream.close proc.getErrorStream.close @@ -302,6 +302,34 @@ new BufferedInputStream(stream) } + def fifo_output_stream(fifo: String): BufferedOutputStream = + { + // block until peer is ready + val stream = + if (Platform.is_windows) { + // Cygwin fifo as Windows/Java output stream (beware of buffering) + // FIXME FIXME FIXME + val script = + "open(FIFO, \">" + fifo + "\") || die $!; my $buffer; " + + "while ((sysread STDIN, $buffer, 65536), length $buffer > 0)" + + " { syswrite FIFO, $buffer; }; close FIFO;" + val proc = execute(false, "perl", "-e", script) + proc.getInputStream.close + proc.getErrorStream.close + val out = proc.getOutputStream + new OutputStream { + override def close() { out.close(); proc.waitFor() } + override def flush() { out.flush() } + override def write(b: Array[Byte]) { out.write(b) } + override def write(b: Array[Byte], off: Int, len: Int) { out.write(b, off, len) } + override def write(b: Int) { out.write(b) } + } + proc.getOutputStream + } + else new FileOutputStream(fifo) + new BufferedOutputStream(stream) + } + /** Isabelle resources **/ diff -r 175a5b4b2c94 -r 3d4e521014f7 src/Pure/System/isar.ML --- a/src/Pure/System/isar.ML Mon Aug 09 13:56:02 2010 +0200 +++ b/src/Pure/System/isar.ML Mon Aug 09 18:18:32 2010 +0200 @@ -18,7 +18,8 @@ val kill: unit -> unit val kill_proof: unit -> unit val crashes: exn list Unsynchronized.ref - val toplevel_loop: {init: bool, welcome: bool, sync: bool, secure: bool} -> unit + val toplevel_loop: TextIO.instream -> + {init: bool, welcome: bool, sync: bool, secure: bool} -> unit val loop: unit -> unit val main: unit -> unit end; @@ -131,20 +132,22 @@ in -fun toplevel_loop {init = do_init, welcome, sync, secure} = +fun toplevel_loop in_stream {init = do_init, welcome, sync, secure} = (Context.set_thread_data NONE; Secure.Isar_setup (); if do_init then init () else (); if welcome then writeln (Session.welcome ()) else (); - uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar sync)) ()); + uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar in_stream sync)) ()); end; fun loop () = - toplevel_loop {init = false, welcome = false, sync = false, secure = Secure.is_secure ()}; + toplevel_loop TextIO.stdIn + {init = false, welcome = false, sync = false, secure = Secure.is_secure ()}; fun main () = - toplevel_loop {init = true, welcome = true, sync = false, secure = Secure.is_secure ()}; + toplevel_loop TextIO.stdIn + {init = true, welcome = true, sync = false, secure = Secure.is_secure ()};