more robust system channel via options that are private to the user;
authorwenzelm
Wed Jan 02 20:20:01 2019 +0100 (13 months ago)
changeset 6957209a6a7c04b45
parent 69571 676182f2e375
child 69573 c7a69b6cd405
more robust system channel via options that are private to the user;
etc/options
src/Pure/ML/ml_process.scala
src/Pure/PIDE/prover.scala
src/Pure/System/isabelle_process.ML
src/Pure/System/isabelle_process.scala
src/Pure/System/system_channel.scala
     1.1 --- a/etc/options	Wed Jan 02 12:50:32 2019 +0100
     1.2 +++ b/etc/options	Wed Jan 02 20:20:01 2019 +0100
     1.3 @@ -302,3 +302,9 @@
     1.4  option build_log_ssh_port : int = 0
     1.5  option build_log_history : int = 30  -- "length of relevant history (in days)"
     1.6  option build_log_transaction_size : int = 1  -- "number of log files for each db update"
     1.7 +
     1.8 +
     1.9 +section "Isabelle/Scala/ML system channel"
    1.10 +
    1.11 +option system_channel_address : string = ""
    1.12 +option system_channel_password : string = ""
     2.1 --- a/src/Pure/ML/ml_process.scala	Wed Jan 02 12:50:32 2019 +0100
     2.2 +++ b/src/Pure/ML/ml_process.scala	Wed Jan 02 20:20:01 2019 +0100
     2.3 @@ -22,7 +22,6 @@
     2.4      env: Map[String, String] = Isabelle_System.settings(),
     2.5      redirect: Boolean = false,
     2.6      cleanup: () => Unit = () => (),
     2.7 -    channel: Option[System_Channel] = None,
     2.8      sessions_structure: Option[Sessions.Structure] = None,
     2.9      session_base: Option[Sessions.Base] = None,
    2.10      store: Option[Sessions.Store] = None): Bash.Process =
    2.11 @@ -89,6 +88,7 @@
    2.12  
    2.13      // options
    2.14      val isabelle_process_options = Isabelle_System.tmp_file("options")
    2.15 +    Isabelle_System.bash("chmod 600 " + File.bash_path(File.path(isabelle_process_options)))
    2.16      File.write(isabelle_process_options, YXML.string_of_body(options.encode))
    2.17      val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
    2.18      val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
    2.19 @@ -120,13 +120,7 @@
    2.20      val eval_process =
    2.21        if (heaps.isEmpty)
    2.22          List("PolyML.print_depth " + ML_Syntax.print_int(options.int("ML_print_depth")))
    2.23 -      else
    2.24 -        channel match {
    2.25 -          case None =>
    2.26 -            List("Isabelle_Process.init_options ()")
    2.27 -          case Some(ch) =>
    2.28 -            List("Isabelle_Process.init_protocol " + ML_Syntax.print_string_bytes(ch.server_name))
    2.29 -        }
    2.30 +      else List("Isabelle_Process.init ()")
    2.31  
    2.32      // ISABELLE_TMP
    2.33      val isabelle_tmp = Isabelle_System.tmp_dir("process")
     3.1 --- a/src/Pure/PIDE/prover.scala	Wed Jan 02 12:50:32 2019 +0100
     3.2 +++ b/src/Pure/PIDE/prover.scala	Wed Jan 02 20:20:01 2019 +0100
     3.3 @@ -82,8 +82,6 @@
     3.4  
     3.5    private def output(kind: String, props: Properties.T, body: XML.Body)
     3.6    {
     3.7 -    if (kind == Markup.INIT) channel.accepted()
     3.8 -
     3.9      val main = XML.Elem(Markup(kind, props), Protocol_Message.clean_reports(body))
    3.10      val reports = Protocol_Message.reports(props, body)
    3.11      for (msg <- main :: reports) receiver(new Prover.Output(xml_cache.elem(msg)))
    3.12 @@ -155,7 +153,7 @@
    3.13        system_output("process_manager terminated")
    3.14        exit_message(result)
    3.15      }
    3.16 -    channel.accepted()
    3.17 +    channel.shutdown()
    3.18    }
    3.19  
    3.20  
     4.1 --- a/src/Pure/System/isabelle_process.ML	Wed Jan 02 12:50:32 2019 +0100
     4.2 +++ b/src/Pure/System/isabelle_process.ML	Wed Jan 02 20:20:01 2019 +0100
     4.3 @@ -10,9 +10,9 @@
     4.4    val protocol_command: string -> (string list -> unit) -> unit
     4.5    val reset_tracing: Document_ID.exec -> unit
     4.6    val crashes: exn list Synchronized.var
     4.7 -  val init_protocol: string -> unit
     4.8    val init_options: unit -> unit
     4.9    val init_options_interactive: unit -> unit
    4.10 +  val init: unit -> unit
    4.11  end;
    4.12  
    4.13  structure Isabelle_Process: ISABELLE_PROCESS =
    4.14 @@ -173,7 +173,7 @@
    4.15  val default_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN];
    4.16  val default_modes2 = [isabelle_processN, Pretty.symbolicN];
    4.17  
    4.18 -val init_protocol = Thread_Attributes.uninterruptible (fn _ => fn socket =>
    4.19 +val init_protocol = Thread_Attributes.uninterruptible (fn _ => fn (address, password) =>
    4.20    let
    4.21      val _ = SHA1.test_samples ()
    4.22        handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); Exn.reraise exn);
    4.23 @@ -184,7 +184,8 @@
    4.24        Unsynchronized.change print_mode
    4.25          (fn mode => (mode @ default_modes1) |> fold (update op =) default_modes2);
    4.26  
    4.27 -    val (in_stream, out_stream) = Socket_IO.open_streams socket;
    4.28 +    val (in_stream, out_stream) = Socket_IO.open_streams address;
    4.29 +    val _ = Byte_Message.write_line out_stream password;
    4.30      val msg_channel = init_channels out_stream;
    4.31      val _ = loop in_stream;
    4.32      val _ = Message_Channel.shutdown msg_channel;
    4.33 @@ -211,4 +212,17 @@
    4.34    Multithreading.parallel_proofs := (if Options.default_int "parallel_proofs" > 0 then 3 else 0);
    4.35    Printer.show_markup_default := true);
    4.36  
    4.37 +
    4.38 +(* generic init *)
    4.39 +
    4.40 +fun init () =
    4.41 +  let
    4.42 +    val address = Options.default_string \<^system_option>\<open>system_channel_address\<close>;
    4.43 +    val password = Options.default_string \<^system_option>\<open>system_channel_password\<close>;
    4.44 +  in
    4.45 +    if address <> "" andalso password <> ""
    4.46 +    then init_protocol (address, password)
    4.47 +    else init_options ()
    4.48 +  end;
    4.49 +
    4.50  end;
     5.1 --- a/src/Pure/System/isabelle_process.scala	Wed Jan 02 12:50:32 2019 +0100
     5.2 +++ b/src/Pure/System/isabelle_process.scala	Wed Jan 02 20:20:01 2019 +0100
     5.3 @@ -49,10 +49,13 @@
     5.4      val channel = System_Channel()
     5.5      val process =
     5.6        try {
     5.7 -        ML_Process(options, logic = logic, args = args, dirs = dirs, modes = modes, cwd = cwd,
     5.8 -          env = env, sessions_structure = sessions_structure, store = store, channel = Some(channel))
     5.9 +        val channel_options =
    5.10 +          options.string.update("system_channel_address", channel.address).
    5.11 +            string.update("system_channel_password", channel.password)
    5.12 +        ML_Process(channel_options, logic = logic, args = args, dirs = dirs, modes = modes,
    5.13 +            cwd = cwd, env = env, sessions_structure = sessions_structure, store = store)
    5.14        }
    5.15 -      catch { case exn @ ERROR(_) => channel.accepted(); throw exn }
    5.16 +      catch { case exn @ ERROR(_) => channel.shutdown(); throw exn }
    5.17      process.stdin.close
    5.18  
    5.19      new Prover(receiver, xml_cache, channel, process)
     6.1 --- a/src/Pure/System/system_channel.scala	Wed Jan 02 12:50:32 2019 +0100
     6.2 +++ b/src/Pure/System/system_channel.scala	Wed Jan 02 20:20:01 2019 +0100
     6.3 @@ -20,14 +20,27 @@
     6.4  {
     6.5    private val server = new ServerSocket(0, 50, Server.localhost)
     6.6  
     6.7 -  val server_name: String = Server.print_address(server.getLocalPort)
     6.8 -  override def toString: String = server_name
     6.9 +  val address: String = Server.print_address(server.getLocalPort)
    6.10 +  val password: String = UUID.random().toString
    6.11 +
    6.12 +  override def toString: String = address
    6.13 +
    6.14 +  def shutdown() { server.close }
    6.15  
    6.16    def rendezvous(): (OutputStream, InputStream) =
    6.17    {
    6.18      val socket = server.accept
    6.19 -    (socket.getOutputStream, socket.getInputStream)
    6.20 -  }
    6.21 +    try {
    6.22 +      val out_stream = socket.getOutputStream
    6.23 +      val in_stream = socket.getInputStream
    6.24  
    6.25 -  def accepted() { server.close }
    6.26 +      if (Byte_Message.read_line(in_stream).map(_.text) == Some(password)) (out_stream, in_stream)
    6.27 +      else {
    6.28 +        out_stream.close
    6.29 +        in_stream.close
    6.30 +        error("Failed to connect system channel: bad password")
    6.31 +      }
    6.32 +    }
    6.33 +    finally { shutdown() }
    6.34 +  }
    6.35  }