alternative Socket_Channel;
authorwenzelm
Wed Sep 21 22:18:17 2011 +0200 (2011-09-21)
changeset 45028d608dd8cd409
parent 45027 f459e93a038e
child 45029 63144ea111f7
alternative Socket_Channel;
use BinIO for fifos uniformly;
bin/isabelle-process
doc-src/System/Thy/Basics.thy
doc-src/System/Thy/document/Basics.tex
src/Pure/General/socket_io.ML
src/Pure/System/isabelle_process.ML
src/Pure/System/system_channel.scala
     1.1 --- a/bin/isabelle-process	Wed Sep 21 20:35:50 2011 +0200
     1.2 +++ b/bin/isabelle-process	Wed Sep 21 22:18:17 2011 +0200
     1.3 @@ -29,6 +29,7 @@
     1.4    echo "    -I           startup Isar interaction mode"
     1.5    echo "    -P           startup Proof General interaction mode"
     1.6    echo "    -S           secure mode -- disallow critical operations"
     1.7 +  echo "    -T ADDR      startup process wrapper, with socket address"
     1.8    echo "    -W IN:OUT    startup process wrapper, with input/output fifos"
     1.9    echo "    -X           startup PGIP interaction mode"
    1.10    echo "    -e MLTEXT    pass MLTEXT to the ML session"
    1.11 @@ -61,6 +62,7 @@
    1.12  ISAR=false
    1.13  PROOFGENERAL=""
    1.14  SECURE=""
    1.15 +WRAPPER_SOCKET=""
    1.16  WRAPPER_FIFOS=""
    1.17  PGIP=""
    1.18  MLTEXT=""
    1.19 @@ -69,7 +71,7 @@
    1.20  READONLY=""
    1.21  NOWRITE=""
    1.22  
    1.23 -while getopts "IPSW:Xe:fm:qruw" OPT
    1.24 +while getopts "IPST:W:Xe:fm:qruw" OPT
    1.25  do
    1.26    case "$OPT" in
    1.27      I)
    1.28 @@ -81,6 +83,9 @@
    1.29      S)
    1.30        SECURE=true
    1.31        ;;
    1.32 +    T)
    1.33 +      WRAPPER_SOCKET="$OPTARG"
    1.34 +      ;;
    1.35      W)
    1.36        WRAPPER_FIFOS="$OPTARG"
    1.37        ;;
    1.38 @@ -213,12 +218,14 @@
    1.39  
    1.40  NICE="nice"
    1.41  
    1.42 -if [ -n "$WRAPPER_FIFOS" ]; then
    1.43 +if [ -n "$WRAPPER_SOCKET" ]; then
    1.44 +  MLTEXT="$MLTEXT; Isabelle_Process.init_socket \"$WRAPPER_SOCKET\";"
    1.45 +elif [ -n "$WRAPPER_FIFOS" ]; then
    1.46    splitarray ":" "$WRAPPER_FIFOS"; FIFOS=("${SPLITARRAY[@]}")
    1.47    [ "${#FIFOS[@]}" -eq 2 ] || fail "Expected IN:OUT fifo specification"
    1.48    [ -p "${FIFOS[0]}" ] || fail "Bad input fifo: ${FIFOS[0]}"
    1.49    [ -p "${FIFOS[1]}" ] || fail "Bad output fifo: ${FIFOS[1]}"
    1.50 -  MLTEXT="$MLTEXT; Isabelle_Process.init \"${FIFOS[0]}\" \"${FIFOS[1]}\";"
    1.51 +  MLTEXT="$MLTEXT; Isabelle_Process.init_fifos \"${FIFOS[0]}\" \"${FIFOS[1]}\";"
    1.52  elif [ -n "$PGIP" ]; then
    1.53    MLTEXT="$MLTEXT; ProofGeneralPgip.init_pgip $ISAR;"
    1.54  elif [ -n "$PROOFGENERAL" ]; then
     2.1 --- a/doc-src/System/Thy/Basics.thy	Wed Sep 21 20:35:50 2011 +0200
     2.2 +++ b/doc-src/System/Thy/Basics.thy	Wed Sep 21 22:18:17 2011 +0200
     2.3 @@ -332,6 +332,7 @@
     2.4      -I           startup Isar interaction mode
     2.5      -P           startup Proof General interaction mode
     2.6      -S           secure mode -- disallow critical operations
     2.7 +    -T ADDR      startup process wrapper, with socket address
     2.8      -W IN:OUT    startup process wrapper, with input/output fifos
     2.9      -X           startup PGIP interaction mode
    2.10      -e MLTEXT    pass MLTEXT to the ML session
    2.11 @@ -409,11 +410,11 @@
    2.12    interaction with the Proof General user interface, and the
    2.13    @{verbatim "-X"} option enables XML-based PGIP communication.
    2.14  
    2.15 -  \medskip The @{verbatim "-W"} option makes Isabelle enter a special
    2.16 -  process wrapper for interaction via the Isabelle/Scala layer, see
    2.17 -  also @{file "~~/src/Pure/System/isabelle_process.scala"}.  The
    2.18 -  protocol between the ML and JVM process is private to the
    2.19 -  implementation.
    2.20 +  \medskip The @{verbatim "-T"} or @{verbatim "-W"} option makes
    2.21 +  Isabelle enter a special process wrapper for interaction via the
    2.22 +  Isabelle/Scala layer, see also @{file
    2.23 +  "~~/src/Pure/System/isabelle_process.scala"}.  The protocol between
    2.24 +  the ML and JVM process is private to the implementation.
    2.25  
    2.26    \medskip The @{verbatim "-S"} option makes the Isabelle process more
    2.27    secure by disabling some critical operations, notably runtime
     3.1 --- a/doc-src/System/Thy/document/Basics.tex	Wed Sep 21 20:35:50 2011 +0200
     3.2 +++ b/doc-src/System/Thy/document/Basics.tex	Wed Sep 21 22:18:17 2011 +0200
     3.3 @@ -343,6 +343,7 @@
     3.4      -I           startup Isar interaction mode
     3.5      -P           startup Proof General interaction mode
     3.6      -S           secure mode -- disallow critical operations
     3.7 +    -T ADDR      startup process wrapper, with socket address
     3.8      -W IN:OUT    startup process wrapper, with input/output fifos
     3.9      -X           startup PGIP interaction mode
    3.10      -e MLTEXT    pass MLTEXT to the ML session
    3.11 @@ -420,11 +421,10 @@
    3.12    interaction with the Proof General user interface, and the
    3.13    \verb|-X| option enables XML-based PGIP communication.
    3.14  
    3.15 -  \medskip The \verb|-W| option makes Isabelle enter a special
    3.16 -  process wrapper for interaction via the Isabelle/Scala layer, see
    3.17 -  also \verb|~~/src/Pure/System/isabelle_process.scala|.  The
    3.18 -  protocol between the ML and JVM process is private to the
    3.19 -  implementation.
    3.20 +  \medskip The \verb|-T| or \verb|-W| option makes
    3.21 +  Isabelle enter a special process wrapper for interaction via the
    3.22 +  Isabelle/Scala layer, see also \verb|~~/src/Pure/System/isabelle_process.scala|.  The protocol between
    3.23 +  the ML and JVM process is private to the implementation.
    3.24  
    3.25    \medskip The \verb|-S| option makes the Isabelle process more
    3.26    secure by disabling some critical operations, notably runtime
     4.1 --- a/src/Pure/General/socket_io.ML	Wed Sep 21 20:35:50 2011 +0200
     4.2 +++ b/src/Pure/General/socket_io.ML	Wed Sep 21 22:18:17 2011 +0200
     4.3 @@ -9,7 +9,7 @@
     4.4  signature SOCKET_IO =
     4.5  sig
     4.6    val make_streams: Socket.active INetSock.stream_sock -> BinIO.instream * BinIO.outstream
     4.7 -  val open_streams: string * int -> BinIO.instream * BinIO.outstream
     4.8 +  val open_streams: string -> BinIO.instream * BinIO.outstream
     4.9  end;
    4.10  
    4.11  structure Socket_IO: SOCKET_IO =
    4.12 @@ -68,15 +68,17 @@
    4.13    in (in_stream, out_stream) end;
    4.14  
    4.15  
    4.16 -fun open_streams (hostname, port) =
    4.17 +fun open_streams socket_name =
    4.18    let
    4.19 -    val host =
    4.20 -      (case NetHostDB.getByName hostname of
    4.21 -        NONE => error ("Bad host name: " ^ quote hostname)
    4.22 -      | SOME host => host);
    4.23 -    val addr = INetSock.toAddr (NetHostDB.addr host, port);
    4.24 +    fun err () = error ("Bad socket name: " ^ quote socket_name);
    4.25 +    val (host, port) =
    4.26 +      (case space_explode ":" socket_name of
    4.27 +        [h, p] =>
    4.28 +         (case NetHostDB.getByName h of SOME host => host | NONE => err (),
    4.29 +          case Int.fromString p of SOME port => port | NONE => err ())
    4.30 +      | _ => err ());
    4.31      val socket: Socket.active INetSock.stream_sock = INetSock.TCP.socket ();
    4.32 -    val _ = Socket.connect (socket, addr);
    4.33 +    val _ = Socket.connect (socket, INetSock.toAddr (NetHostDB.addr host, port));
    4.34    in make_streams socket end;
    4.35  
    4.36  end;
     5.1 --- a/src/Pure/System/isabelle_process.ML	Wed Sep 21 20:35:50 2011 +0200
     5.2 +++ b/src/Pure/System/isabelle_process.ML	Wed Sep 21 22:18:17 2011 +0200
     5.3 @@ -21,7 +21,8 @@
     5.4    val add_command: string -> (string list -> unit) -> unit
     5.5    val command: string -> string list -> unit
     5.6    val crashes: exn list Synchronized.var
     5.7 -  val init: string -> string -> unit
     5.8 +  val init_socket: string -> unit
     5.9 +  val init_fifos: string -> string -> unit
    5.10  end;
    5.11  
    5.12  structure Isabelle_Process: ISABELLE_PROCESS =
    5.13 @@ -81,11 +82,11 @@
    5.14  
    5.15  fun message_output mbox out_stream =
    5.16    let
    5.17 -    fun flush () = ignore (try TextIO.flushOut out_stream);
    5.18 +    fun flush () = ignore (try BinIO.flushOut out_stream);
    5.19      fun loop receive =
    5.20        (case receive mbox of
    5.21          SOME (msg, do_flush) =>
    5.22 -         (List.app (fn s => TextIO.output (out_stream, s)) msg;
    5.23 +         (List.app (fn s => BinIO.output (out_stream, Byte.stringToBytes s)) msg;
    5.24            if do_flush then flush () else ();
    5.25            loop (Mailbox.receive_timeout (seconds 0.02)))
    5.26        | NONE => (flush (); loop (SOME o Mailbox.receive)));
    5.27 @@ -93,12 +94,8 @@
    5.28  
    5.29  in
    5.30  
    5.31 -fun setup_channels in_fifo out_fifo =
    5.32 +fun setup_channels out_stream =
    5.33    let
    5.34 -    (*rendezvous*)
    5.35 -    val in_stream = TextIO.openIn in_fifo;
    5.36 -    val out_stream = TextIO.openOut out_fifo;
    5.37 -
    5.38      val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF);
    5.39      val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF);
    5.40  
    5.41 @@ -114,8 +111,7 @@
    5.42      Output.Private_Hooks.raw_message_fn := message true mbox "H";
    5.43      Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
    5.44      Output.Private_Hooks.prompt_fn := ignore;
    5.45 -    message true mbox "A" [] (Session.welcome ());
    5.46 -    in_stream
    5.47 +    message true mbox "A" [] (Session.welcome ())
    5.48    end;
    5.49  
    5.50  end;
    5.51 @@ -131,13 +127,25 @@
    5.52    (Synchronized.change crashes (cons crash);
    5.53      warning "Recovering from Isabelle process crash -- see also Isabelle_Process.crashes");
    5.54  
    5.55 +fun read_line stream =
    5.56 +  let
    5.57 +    val content = String.implode o rev;
    5.58 +    fun read cs =
    5.59 +      (case BinIO.input1 stream of
    5.60 +        NONE => (content cs, null cs)
    5.61 +      | SOME b =>
    5.62 +          (case Byte.byteToChar b of
    5.63 +            #"\n" => (content cs, false)
    5.64 +          | c => read (c :: cs)));
    5.65 +  in case read [] of ("", true) => NONE | (s, _) => SOME s end;
    5.66 +
    5.67  fun read_chunk stream len =
    5.68    let
    5.69      val n =
    5.70        (case Int.fromString len of
    5.71          SOME n => n
    5.72        | NONE => error ("Isabelle process: malformed chunk header " ^ quote len));
    5.73 -    val chunk = TextIO.inputN (stream, n);
    5.74 +    val chunk = Byte.bytesToString (BinIO.inputN (stream, n));
    5.75      val m = size chunk;
    5.76    in
    5.77      if m = n then chunk
    5.78 @@ -145,7 +153,7 @@
    5.79    end;
    5.80  
    5.81  fun read_command stream =
    5.82 -  (case TextIO.inputLine stream of
    5.83 +  (case read_line stream of
    5.84      NONE => raise Runtime.TERMINATE
    5.85    | SOME line => map (read_chunk stream) (space_explode "," line));
    5.86  
    5.87 @@ -170,7 +178,7 @@
    5.88  
    5.89  (* init *)
    5.90  
    5.91 -fun init in_fifo out_fifo = ignore (Simple_Thread.fork false (fn () =>
    5.92 +fun init make_streams = ignore (Simple_Thread.fork false (fn () =>
    5.93    let
    5.94      val _ = OS.Process.sleep (seconds 0.5);  (*yield to raw ML toplevel*)
    5.95      val _ = Output.physical_stdout Symbol.STX;
    5.96 @@ -186,11 +194,18 @@
    5.97          (fold (update op =)
    5.98            [Symbol.xsymbolsN, isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]);
    5.99  
   5.100 -    val in_stream = setup_channels in_fifo out_fifo;
   5.101 +    val (in_stream, out_stream) = make_streams ();
   5.102 +    val _ = setup_channels out_stream;
   5.103 +
   5.104      val _ = Keyword.status ();
   5.105      val _ = Thy_Info.status ();
   5.106      val _ = Output.status (Markup.markup Markup.ready "process ready");
   5.107    in loop in_stream end));
   5.108  
   5.109 +fun rendezvous fifo1 fifo2 = (BinIO.openIn fifo1, BinIO.openOut fifo2);
   5.110 +fun init_fifos fifo1 fifo2 = init (fn () => rendezvous fifo1 fifo2);
   5.111 +
   5.112 +fun init_socket socket_name = init (fn () => Socket_IO.open_streams socket_name);
   5.113 +
   5.114  end;
   5.115  
     6.1 --- a/src/Pure/System/system_channel.scala	Wed Sep 21 20:35:50 2011 +0200
     6.2 +++ b/src/Pure/System/system_channel.scala	Wed Sep 21 22:18:17 2011 +0200
     6.3 @@ -1,13 +1,15 @@
     6.4  /*  Title:      Pure/System/system_channel.scala
     6.5      Author:     Makarius
     6.6  
     6.7 -Portable system channel for inter-process communication.
     6.8 +Portable system channel for inter-process communication, based on
     6.9 +named pipes or sockets.
    6.10  */
    6.11  
    6.12  package isabelle
    6.13  
    6.14  
    6.15  import java.io.{InputStream, OutputStream, File, FileInputStream, FileOutputStream, IOException}
    6.16 +import java.net.{ServerSocket, InetAddress}
    6.17  
    6.18  
    6.19  object System_Channel
    6.20 @@ -23,6 +25,8 @@
    6.21  }
    6.22  
    6.23  
    6.24 +/** named pipes **/
    6.25 +
    6.26  object Fifo_Channel
    6.27  {
    6.28    private val next_fifo = new Counter
    6.29 @@ -30,8 +34,6 @@
    6.30  
    6.31  class Fifo_Channel extends System_Channel
    6.32  {
    6.33 -  /* operations on named pipes */
    6.34 -
    6.35    private def mk_fifo(): String =
    6.36    {
    6.37      val i = Fifo_Channel.next_fifo()
    6.38 @@ -81,8 +83,6 @@
    6.39    }
    6.40  
    6.41  
    6.42 -  /* initialization */
    6.43 -
    6.44    private val fifo1 = mk_fifo()
    6.45    private val fifo2 = mk_fifo()
    6.46  
    6.47 @@ -90,7 +90,6 @@
    6.48  
    6.49    def rendezvous(): (OutputStream, InputStream) =
    6.50    {
    6.51 -    /*rendezvous*/
    6.52      val output_stream = fifo_output_stream(fifo1)
    6.53      val input_stream = fifo_input_stream(fifo2)
    6.54      (output_stream, input_stream)
    6.55 @@ -98,3 +97,21 @@
    6.56  
    6.57    def accepted() { rm_fifo(fifo1); rm_fifo(fifo2) }
    6.58  }
    6.59 +
    6.60 +
    6.61 +/** sockets **/
    6.62 +
    6.63 +class Socket_Channel extends System_Channel
    6.64 +{
    6.65 +  private val server = new ServerSocket(0, 2, InetAddress.getByName("127.0.0.1"))
    6.66 +
    6.67 +  def isabelle_args: List[String] = List("-T", "127.0.0.1:" + server.getLocalPort)
    6.68 +
    6.69 +  def rendezvous(): (OutputStream, InputStream) =
    6.70 +  {
    6.71 +    val socket = server.accept
    6.72 +    (socket.getOutputStream, socket.getInputStream)
    6.73 +  }
    6.74 +
    6.75 +  def accepted() { server.close }
    6.76 +}