src/Pure/Tools/build_job.scala
author wenzelm
Thu, 26 Nov 2020 13:15:57 +0100
changeset 72717 4fa1aa5dac4f
parent 72715 2615b8c05337
child 72721 79f5e843e5ec
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Tools/build_job.scala
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
     3
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
     4
Build job running prover process, with rudimentary PIDE session.
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
     5
*/
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
     6
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
     7
package isabelle
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
     8
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
     9
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    10
import scala.collection.mutable
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    11
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    12
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    13
class Build_Job(progress: Progress,
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    14
  session_name: String,
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    15
  val info: Sessions.Info,
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    16
  deps: Sessions.Deps,
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    17
  store: Sessions.Store,
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    18
  do_store: Boolean,
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    19
  verbose: Boolean,
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    20
  val numa_node: Option[Int],
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    21
  command_timings0: List[Properties.T])
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    22
{
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    23
  val options: Options = NUMA.policy_options(info.options, numa_node)
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    24
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    25
  private val sessions_structure = deps.sessions_structure
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    26
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    27
  private val future_result: Future[Process_Result] =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    28
    Future.thread("build", uninterruptible = true) {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    29
      val parent = info.parent.getOrElse("")
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    30
      val base = deps(parent)
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    31
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    32
      val env =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    33
        Isabelle_System.settings() +
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    34
          ("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString)
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    35
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    36
      val is_pure = Sessions.is_pure(session_name)
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    37
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    38
      val use_prelude = if (is_pure) Thy_Header.ml_roots.map(_._1) else Nil
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    39
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    40
      val eval_store =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    41
        if (do_store) {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    42
          (if (info.theories.nonEmpty) List("ML_Heap.share_common_data ()") else Nil) :::
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    43
          List("ML_Heap.save_child " +
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    44
            ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(session_name))))
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    45
        }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    46
        else Nil
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    47
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    48
      val resources = new Resources(sessions_structure, base, command_timings = command_timings0)
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    49
      val session =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    50
        new Session(options, resources) {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    51
          override val xml_cache: XML.Cache = store.xml_cache
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    52
          override val xz_cache: XZ.Cache = store.xz_cache
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    53
        }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    54
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    55
      object Build_Session_Errors
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    56
      {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    57
        private val promise: Promise[List[String]] = Future.promise
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    58
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    59
        def result: Exn.Result[List[String]] = promise.join_result
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    60
        def cancel: Unit = promise.cancel
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    61
        def apply(errs: List[String])
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    62
        {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    63
          try { promise.fulfill(errs) }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    64
          catch { case _: IllegalStateException => }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    65
        }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    66
      }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    67
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    68
      val export_consumer =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    69
        Export.consumer(store.open_database(session_name, output = true), cache = store.xz_cache)
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    70
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    71
      val stdout = new StringBuilder(1000)
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    72
      val stderr = new StringBuilder(1000)
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    73
      val messages = new mutable.ListBuffer[XML.Elem]
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    74
      val command_timings = new mutable.ListBuffer[Properties.T]
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    75
      val theory_timings = new mutable.ListBuffer[Properties.T]
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    76
      val session_timings = new mutable.ListBuffer[Properties.T]
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    77
      val runtime_statistics = new mutable.ListBuffer[Properties.T]
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    78
      val task_statistics = new mutable.ListBuffer[Properties.T]
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    79
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    80
      def fun(
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    81
        name: String,
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    82
        acc: mutable.ListBuffer[Properties.T],
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    83
        unapply: Properties.T => Option[Properties.T]): (String, Session.Protocol_Function) =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    84
      {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    85
        name -> ((msg: Prover.Protocol_Output) =>
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    86
          unapply(msg.properties) match {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    87
            case Some(props) => acc += props; true
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    88
            case _ => false
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    89
          })
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    90
      }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    91
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    92
      session.init_protocol_handler(new Session.Protocol_Handler
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    93
        {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    94
          override def exit() { Build_Session_Errors.cancel }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    95
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    96
          private def build_session_finished(msg: Prover.Protocol_Output): Boolean =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    97
          {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    98
            val (rc, errors) =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    99
              try {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   100
                val (rc, errs) =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   101
                {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   102
                  import XML.Decode._
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   103
                  pair(int, list(x => x))(Symbol.decode_yxml(msg.text))
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   104
                }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   105
                val errors =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   106
                  for (err <- errs) yield {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   107
                    val prt = Protocol_Message.expose_no_reports(err)
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   108
                    Pretty.string_of(prt, metric = Symbol.Metric)
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   109
                  }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   110
                (rc, errors)
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   111
              }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   112
              catch { case ERROR(err) => (2, List(err)) }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   113
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   114
            session.protocol_command("Prover.stop", rc.toString)
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   115
            Build_Session_Errors(errors)
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   116
            true
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   117
          }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   118
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   119
          private def loading_theory(msg: Prover.Protocol_Output): Boolean =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   120
            msg.properties match {
72692
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72683
diff changeset
   121
              case Markup.Loading_Theory(Markup.Name(name)) =>
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   122
                progress.theory(Progress.Theory(name, session = session_name))
72692
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72683
diff changeset
   123
                false
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   124
              case _ => false
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   125
            }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   126
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   127
          private def export(msg: Prover.Protocol_Output): Boolean =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   128
            msg.properties match {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   129
              case Protocol.Export(args) =>
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   130
                export_consumer(session_name, args, msg.bytes)
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   131
                true
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   132
              case _ => false
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   133
            }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   134
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   135
          override val functions =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   136
            List(
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   137
              Markup.Build_Session_Finished.name -> build_session_finished,
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   138
              Markup.Loading_Theory.name -> loading_theory,
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   139
              Markup.EXPORT -> export,
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   140
              fun(Markup.Theory_Timing.name, theory_timings, Markup.Theory_Timing.unapply),
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   141
              fun(Markup.Session_Timing.name, session_timings, Markup.Session_Timing.unapply),
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   142
              fun(Markup.Task_Statistics.name, task_statistics, Markup.Task_Statistics.unapply))
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   143
        })
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   144
72711
9e89c2e15d36 clarified command_timings protocol;
wenzelm
parents: 72701
diff changeset
   145
      session.command_timings += Session.Consumer("command_timings")
9e89c2e15d36 clarified command_timings protocol;
wenzelm
parents: 72701
diff changeset
   146
        {
9e89c2e15d36 clarified command_timings protocol;
wenzelm
parents: 72701
diff changeset
   147
          case Session.Command_Timing(props) =>
9e89c2e15d36 clarified command_timings protocol;
wenzelm
parents: 72701
diff changeset
   148
            for {
9e89c2e15d36 clarified command_timings protocol;
wenzelm
parents: 72701
diff changeset
   149
              elapsed <- Markup.Elapsed.unapply(props)
9e89c2e15d36 clarified command_timings protocol;
wenzelm
parents: 72701
diff changeset
   150
              elapsed_time = Time.seconds(elapsed)
9e89c2e15d36 clarified command_timings protocol;
wenzelm
parents: 72701
diff changeset
   151
              if elapsed_time.is_relevant && elapsed_time >= options.seconds("command_timing_threshold")
9e89c2e15d36 clarified command_timings protocol;
wenzelm
parents: 72701
diff changeset
   152
            } command_timings += props.filter(Markup.command_timing_property)
9e89c2e15d36 clarified command_timings protocol;
wenzelm
parents: 72701
diff changeset
   153
        }
9e89c2e15d36 clarified command_timings protocol;
wenzelm
parents: 72701
diff changeset
   154
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   155
      session.runtime_statistics += Session.Consumer("ML_statistics")
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   156
        {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   157
          case Session.Runtime_Statistics(props) => runtime_statistics += props
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   158
        }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   159
72692
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72683
diff changeset
   160
      session.finished_theories += Session.Consumer[Command.State]("finished_theories")
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72683
diff changeset
   161
        {
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72683
diff changeset
   162
          case st =>
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72683
diff changeset
   163
            val command = st.command
72717
wenzelm
parents: 72715
diff changeset
   164
            val markup = st.markups(Command.Markup_Index.markup)
wenzelm
parents: 72715
diff changeset
   165
wenzelm
parents: 72715
diff changeset
   166
            def export(name: String, xml: XML.Body)
wenzelm
parents: 72715
diff changeset
   167
            {
wenzelm
parents: 72715
diff changeset
   168
              val theory_name = command.node_name.theory
wenzelm
parents: 72715
diff changeset
   169
              val args = Protocol.Export.Args(theory_name = theory_name, name = name)
wenzelm
parents: 72715
diff changeset
   170
              export_consumer(session_name, args, Bytes(YXML.string_of_body(xml)))
wenzelm
parents: 72715
diff changeset
   171
            }
wenzelm
parents: 72715
diff changeset
   172
wenzelm
parents: 72715
diff changeset
   173
            export(Export.MARKUP,
wenzelm
parents: 72715
diff changeset
   174
              markup.to_XML(command.range, command.source, Markup.Elements.full))
72692
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72683
diff changeset
   175
        }
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72683
diff changeset
   176
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   177
      session.all_messages += Session.Consumer[Any]("build_session_output")
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   178
        {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   179
          case msg: Prover.Output =>
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   180
            val message = msg.message
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   181
            if (msg.is_stdout) {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   182
              stdout ++= Symbol.encode(XML.content(message))
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   183
            }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   184
            else if (msg.is_stderr) {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   185
              stderr ++= Symbol.encode(XML.content(message))
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   186
            }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   187
            else if (Protocol.is_exported(message)) {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   188
              messages += message
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   189
            }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   190
            else if (msg.is_exit) {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   191
              val err =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   192
                "Prover terminated" +
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   193
                  (msg.properties match {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   194
                    case Markup.Process_Result(result) => ": " + result.print_rc
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   195
                    case _ => ""
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   196
                  })
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   197
              Build_Session_Errors(List(err))
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   198
            }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   199
          case _ =>
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   200
        }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   201
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   202
      val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store)
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   203
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   204
      val process =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   205
        Isabelle_Process(session, options, sessions_structure, store,
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   206
          logic = parent, raw_ml_system = is_pure,
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   207
          use_prelude = use_prelude, eval_main = eval_main,
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   208
          cwd = info.dir.file, env = env)
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   209
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   210
      val build_errors =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   211
        Isabelle_Thread.interrupt_handler(_ => process.terminate) {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   212
          Exn.capture { process.await_startup } match {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   213
            case Exn.Res(_) =>
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   214
              val resources_yxml = resources.init_session_yxml
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   215
              val args_yxml =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   216
                YXML.string_of_body(
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   217
                  {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   218
                    import XML.Encode._
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   219
                    pair(string, list(pair(Options.encode, list(pair(string, properties)))))(
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   220
                      (session_name, info.theories))
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   221
                  })
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   222
              session.protocol_command("build_session", resources_yxml, args_yxml)
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   223
              Build_Session_Errors.result
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   224
            case Exn.Exn(exn) => Exn.Res(List(Exn.message(exn)))
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   225
          }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   226
        }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   227
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   228
      val process_result =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   229
        Isabelle_Thread.interrupt_handler(_ => process.terminate) { process.await_shutdown }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   230
72697
e16f85e3c288 more robust;
wenzelm
parents: 72696
diff changeset
   231
      session.stop()
e16f85e3c288 more robust;
wenzelm
parents: 72696
diff changeset
   232
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   233
      val export_errors =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   234
        export_consumer.shutdown(close = true).map(Output.error_message_text)
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   235
72699
ed59a506998f clarified document_output vs. progress;
wenzelm
parents: 72697
diff changeset
   236
      val (document_output, document_errors) =
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   237
        try {
72675
cc1347c8c804 clarified document output;
wenzelm
parents: 72673
diff changeset
   238
          if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty)
cc1347c8c804 clarified document output;
wenzelm
parents: 72673
diff changeset
   239
          {
72715
2615b8c05337 clarified signature --- avoid repeated open_database on server;
wenzelm
parents: 72711
diff changeset
   240
            using(store.open_database_context(deps.sessions_structure))(db_context =>
2615b8c05337 clarified signature --- avoid repeated open_database on server;
wenzelm
parents: 72711
diff changeset
   241
              {
2615b8c05337 clarified signature --- avoid repeated open_database on server;
wenzelm
parents: 72711
diff changeset
   242
                val documents =
2615b8c05337 clarified signature --- avoid repeated open_database on server;
wenzelm
parents: 72711
diff changeset
   243
                  Presentation.build_documents(session_name, deps, db_context,
2615b8c05337 clarified signature --- avoid repeated open_database on server;
wenzelm
parents: 72711
diff changeset
   244
                    output_sources = info.document_output,
2615b8c05337 clarified signature --- avoid repeated open_database on server;
wenzelm
parents: 72711
diff changeset
   245
                    output_pdf = info.document_output,
2615b8c05337 clarified signature --- avoid repeated open_database on server;
wenzelm
parents: 72711
diff changeset
   246
                    progress = progress,
2615b8c05337 clarified signature --- avoid repeated open_database on server;
wenzelm
parents: 72711
diff changeset
   247
                    verbose = verbose)
2615b8c05337 clarified signature --- avoid repeated open_database on server;
wenzelm
parents: 72711
diff changeset
   248
                db_context.output_database(session_name)(db =>
2615b8c05337 clarified signature --- avoid repeated open_database on server;
wenzelm
parents: 72711
diff changeset
   249
                  documents.foreach(_.write(db, session_name)))
2615b8c05337 clarified signature --- avoid repeated open_database on server;
wenzelm
parents: 72711
diff changeset
   250
                (documents.flatMap(_.log_lines), Nil)
2615b8c05337 clarified signature --- avoid repeated open_database on server;
wenzelm
parents: 72711
diff changeset
   251
              })
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   252
          }
72699
ed59a506998f clarified document_output vs. progress;
wenzelm
parents: 72697
diff changeset
   253
          (Nil, Nil)
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   254
        }
72699
ed59a506998f clarified document_output vs. progress;
wenzelm
parents: 72697
diff changeset
   255
        catch { case Exn.Interrupt.ERROR(msg) => (Nil, List(msg)) }
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   256
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   257
      val result =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   258
      {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   259
        val more_output =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   260
          Library.trim_line(stdout.toString) ::
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   261
            messages.toList.map(message =>
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   262
              Symbol.encode(Protocol.message_text(List(message), metric = Symbol.Metric))) :::
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   263
            command_timings.toList.map(Protocol.Command_Timing_Marker.apply) :::
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   264
            theory_timings.toList.map(Protocol.Theory_Timing_Marker.apply) :::
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   265
            session_timings.toList.map(Protocol.Session_Timing_Marker.apply) :::
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   266
            runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) :::
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   267
            task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply) :::
72699
ed59a506998f clarified document_output vs. progress;
wenzelm
parents: 72697
diff changeset
   268
            document_output
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   269
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   270
        val more_errors =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   271
          Library.trim_line(stderr.toString) :: export_errors ::: document_errors
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   272
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   273
        process_result.output(more_output).errors(more_errors)
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   274
      }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   275
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   276
      build_errors match {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   277
        case Exn.Res(build_errs) =>
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   278
          val errs = build_errs ::: document_errors
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   279
          if (errs.isEmpty) result
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   280
          else {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   281
            result.error_rc.output(
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   282
              errs.flatMap(s => split_lines(Output.error_message_text(s))) :::
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   283
                errs.map(Protocol.Error_Message_Marker.apply))
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   284
          }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   285
        case Exn.Exn(Exn.Interrupt()) =>
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   286
          if (result.ok) result.copy(rc = Exn.Interrupt.return_code) else result
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   287
        case Exn.Exn(exn) => throw exn
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   288
      }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   289
    }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   290
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   291
  def terminate: Unit = future_result.cancel
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   292
  def is_finished: Boolean = future_result.is_finished
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   293
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   294
  private val timeout_request: Option[Event_Timer.Request] =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   295
  {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   296
    if (info.timeout > Time.zero)
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   297
      Some(Event_Timer.request(Time.now() + info.timeout) { terminate })
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   298
    else None
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   299
  }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   300
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   301
  def join: (Process_Result, Option[String]) =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   302
  {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   303
    val result1 = future_result.join
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   304
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   305
    val was_timeout =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   306
      timeout_request match {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   307
        case None => false
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   308
        case Some(request) => !request.cancel
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   309
      }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   310
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   311
    val result2 =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   312
      if (result1.interrupted) {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   313
        if (was_timeout) result1.error(Output.error_message_text("Timeout")).was_timeout
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   314
        else result1.error(Output.error_message_text("Interrupt"))
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   315
      }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   316
      else result1
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   317
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   318
    val heap_digest =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   319
      if (result2.ok && do_store && store.output_heap(session_name).is_file)
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   320
        Some(Sessions.write_heap_digest(store.output_heap(session_name)))
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   321
      else None
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   322
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   323
    (result2, heap_digest)
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   324
  }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   325
}