src/Pure/System/isabelle_process.scala
author wenzelm
Fri, 16 Dec 2022 17:51:52 +0100
changeset 76656 a8f452f7c503
parent 76655 b3d458a90aeb
child 76729 b045b40a65cc
permissions -rw-r--r--
clarified names;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43283
446e6621762d updated headers;
wenzelm
parents: 40848
diff changeset
     1
/*  Title:      Pure/System/isabelle_process.scala
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
     3
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
     4
Isabelle process wrapper.
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
     5
*/
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
     6
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
     7
package isabelle
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
     8
55618
995162143ef4 tuned imports;
wenzelm
parents: 54443
diff changeset
     9
73897
0ddb5de0506e clarified signature: prefer Java interfaces;
wenzelm
parents: 73803
diff changeset
    10
import java.util.{Map => JMap}
65310
da9f1ef8ef7c more process arguments;
wenzelm
parents: 65225
diff changeset
    11
import java.io.{File => JFile}
da9f1ef8ef7c more process arguments;
wenzelm
parents: 65225
diff changeset
    12
da9f1ef8ef7c more process arguments;
wenzelm
parents: 65225
diff changeset
    13
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73897
diff changeset
    14
object Isabelle_Process {
73802
8d9ac6cfc270 clarified signature;
wenzelm
parents: 73367
diff changeset
    15
  def start(
71594
8a298184f3f9 clarified signature;
wenzelm
parents: 69572
diff changeset
    16
    session: Session,
65216
060a8a1f2dec tuned signature;
wenzelm
parents: 62754
diff changeset
    17
    options: Options,
76656
a8f452f7c503 clarified names;
wenzelm
parents: 76655
diff changeset
    18
    session_background: Sessions.Background,
71598
269dc4bf1f40 clarified signature;
wenzelm
parents: 71597
diff changeset
    19
    store: Sessions.Store,
65216
060a8a1f2dec tuned signature;
wenzelm
parents: 62754
diff changeset
    20
    logic: String = "",
71639
ec84f542e411 clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
wenzelm
parents: 71607
diff changeset
    21
    raw_ml_system: Boolean = false,
ec84f542e411 clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
wenzelm
parents: 71607
diff changeset
    22
    use_prelude: List[String] = Nil,
ec84f542e411 clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
wenzelm
parents: 71607
diff changeset
    23
    eval_main: String = "",
65216
060a8a1f2dec tuned signature;
wenzelm
parents: 62754
diff changeset
    24
    modes: List[String] = Nil,
65310
da9f1ef8ef7c more process arguments;
wenzelm
parents: 65225
diff changeset
    25
    cwd: JFile = null,
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73897
diff changeset
    26
    env: JMap[String, String] = Isabelle_System.settings()
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73897
diff changeset
    27
  ): Isabelle_Process = {
62556
c115e69f457f more abstract Session.start, without prover command-line;
wenzelm
parents: 62555
diff changeset
    28
    val channel = System_Channel()
c115e69f457f more abstract Session.start, without prover command-line;
wenzelm
parents: 62555
diff changeset
    29
    val process =
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    30
      try {
69572
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 68209
diff changeset
    31
        val channel_options =
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 68209
diff changeset
    32
          options.string.update("system_channel_address", channel.address).
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 68209
diff changeset
    33
            string.update("system_channel_password", channel.password)
76656
a8f452f7c503 clarified names;
wenzelm
parents: 76655
diff changeset
    34
        ML_Process(channel_options, session_background, store,
71639
ec84f542e411 clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
wenzelm
parents: 71607
diff changeset
    35
          logic = logic, raw_ml_system = raw_ml_system,
ec84f542e411 clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
wenzelm
parents: 71607
diff changeset
    36
          use_prelude = use_prelude, eval_main = eval_main,
ec84f542e411 clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
wenzelm
parents: 71607
diff changeset
    37
          modes = modes, cwd = cwd, env = env)
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    38
      }
69572
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 68209
diff changeset
    39
      catch { case exn @ ERROR(_) => channel.shutdown(); throw exn }
57917
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    40
73802
8d9ac6cfc270 clarified signature;
wenzelm
parents: 73367
diff changeset
    41
    val isabelle_process = new Isabelle_Process(session, process)
73803
2141d6c83511 tuned --- potentially more robust (e.g. session.phase_changed vs. isabelle_process.terminated);
wenzelm
parents: 73802
diff changeset
    42
    process.stdin.close()
73802
8d9ac6cfc270 clarified signature;
wenzelm
parents: 73367
diff changeset
    43
    session.start(receiver => new Prover(receiver, session.cache, channel, process))
8d9ac6cfc270 clarified signature;
wenzelm
parents: 73367
diff changeset
    44
8d9ac6cfc270 clarified signature;
wenzelm
parents: 73367
diff changeset
    45
    isabelle_process
57917
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    46
  }
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    47
}
71604
c6fa217c9d5e clarified signature: more robust startup_join;
wenzelm
parents: 71598
diff changeset
    48
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73897
diff changeset
    49
class Isabelle_Process private(session: Session, process: Bash.Process) {
71607
d97f504c8145 clarified Isabelle_Process phases;
wenzelm
parents: 71605
diff changeset
    50
  private val startup = Future.promise[String]
d97f504c8145 clarified Isabelle_Process phases;
wenzelm
parents: 71605
diff changeset
    51
  private val terminated = Future.promise[Process_Result]
71604
c6fa217c9d5e clarified signature: more robust startup_join;
wenzelm
parents: 71598
diff changeset
    52
c6fa217c9d5e clarified signature: more robust startup_join;
wenzelm
parents: 71598
diff changeset
    53
  session.phase_changed +=
c6fa217c9d5e clarified signature: more robust startup_join;
wenzelm
parents: 71598
diff changeset
    54
    Session.Consumer(getClass.getName) {
c6fa217c9d5e clarified signature: more robust startup_join;
wenzelm
parents: 71598
diff changeset
    55
      case Session.Ready =>
71607
d97f504c8145 clarified Isabelle_Process phases;
wenzelm
parents: 71605
diff changeset
    56
        startup.fulfill("")
d97f504c8145 clarified Isabelle_Process phases;
wenzelm
parents: 71605
diff changeset
    57
      case Session.Terminated(result) =>
d97f504c8145 clarified Isabelle_Process phases;
wenzelm
parents: 71605
diff changeset
    58
        if (!result.ok && !startup.is_finished) {
76488
1eed7e1300ed clarified signature: more public operations;
wenzelm
parents: 75393
diff changeset
    59
          val syslog = session.syslog.content()
71607
d97f504c8145 clarified Isabelle_Process phases;
wenzelm
parents: 71605
diff changeset
    60
          val err = "Session startup failed" + (if (syslog.isEmpty) "" else ":\n" + syslog)
d97f504c8145 clarified Isabelle_Process phases;
wenzelm
parents: 71605
diff changeset
    61
          startup.fulfill(err)
d97f504c8145 clarified Isabelle_Process phases;
wenzelm
parents: 71605
diff changeset
    62
        }
d97f504c8145 clarified Isabelle_Process phases;
wenzelm
parents: 71605
diff changeset
    63
        terminated.fulfill(result)
71604
c6fa217c9d5e clarified signature: more robust startup_join;
wenzelm
parents: 71598
diff changeset
    64
      case _ =>
c6fa217c9d5e clarified signature: more robust startup_join;
wenzelm
parents: 71598
diff changeset
    65
    }
c6fa217c9d5e clarified signature: more robust startup_join;
wenzelm
parents: 71598
diff changeset
    66
71607
d97f504c8145 clarified Isabelle_Process phases;
wenzelm
parents: 71605
diff changeset
    67
  def await_startup(): Isabelle_Process =
d97f504c8145 clarified Isabelle_Process phases;
wenzelm
parents: 71605
diff changeset
    68
    startup.join match {
d97f504c8145 clarified Isabelle_Process phases;
wenzelm
parents: 71605
diff changeset
    69
      case "" => this
d97f504c8145 clarified Isabelle_Process phases;
wenzelm
parents: 71605
diff changeset
    70
      case err => session.stop(); error(err)
71604
c6fa217c9d5e clarified signature: more robust startup_join;
wenzelm
parents: 71598
diff changeset
    71
    }
c6fa217c9d5e clarified signature: more robust startup_join;
wenzelm
parents: 71598
diff changeset
    72
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73897
diff changeset
    73
  def await_shutdown(): Process_Result = {
71667
4d2de35214c5 proper treatment of protocol exceptions and prover termination: avoid session.stop while saving image;
wenzelm
parents: 71639
diff changeset
    74
    val result = terminated.join
4d2de35214c5 proper treatment of protocol exceptions and prover termination: avoid session.stop while saving image;
wenzelm
parents: 71639
diff changeset
    75
    session.stop()
4d2de35214c5 proper treatment of protocol exceptions and prover termination: avoid session.stop while saving image;
wenzelm
parents: 71639
diff changeset
    76
    result
4d2de35214c5 proper treatment of protocol exceptions and prover termination: avoid session.stop while saving image;
wenzelm
parents: 71639
diff changeset
    77
  }
71718
54ac957c53ec more robust interrupts;
wenzelm
parents: 71667
diff changeset
    78
73367
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73340
diff changeset
    79
  def terminate(): Unit = process.terminate()
71667
4d2de35214c5 proper treatment of protocol exceptions and prover termination: avoid session.stop while saving image;
wenzelm
parents: 71639
diff changeset
    80
}