author | wenzelm |
Fri, 24 Feb 2023 20:40:50 +0100 | |
changeset 77368 | 7c57d9586f4c |
parent 76729 | b045b40a65cc |
child 77414 | 0d5994eef9e6 |
permissions | -rw-r--r-- |
43283 | 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 | 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 | 9 |
|
73897 | 10 |
import java.util.{Map => JMap} |
65310 | 11 |
import java.io.{File => JFile} |
12 |
||
13 |
||
75393 | 14 |
object Isabelle_Process { |
73802 | 15 |
def start( |
76729 | 16 |
store: Sessions.Store, |
65216 | 17 |
options: Options, |
76729 | 18 |
session: Session, |
76656 | 19 |
session_background: Sessions.Background, |
65216 | 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 | 24 |
modes: List[String] = Nil, |
65310 | 25 |
cwd: JFile = null, |
75393 | 26 |
env: JMap[String, String] = Isabelle_System.settings() |
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 | 30 |
try { |
76729 | 31 |
val ml_options = |
32 |
options. |
|
33 |
string.update("system_channel_address", channel.address). |
|
69572
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
68209
diff
changeset
|
34 |
string.update("system_channel_password", channel.password) |
76729 | 35 |
ML_Process(store, ml_options, session_background, |
71639
ec84f542e411
clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
wenzelm
parents:
71607
diff
changeset
|
36 |
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
|
37 |
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
|
38 |
modes = modes, cwd = cwd, env = env) |
57916 | 39 |
} |
69572
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
68209
diff
changeset
|
40 |
catch { case exn @ ERROR(_) => channel.shutdown(); throw exn } |
57917 | 41 |
|
73802 | 42 |
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
|
43 |
process.stdin.close() |
73802 | 44 |
session.start(receiver => new Prover(receiver, session.cache, channel, process)) |
45 |
||
46 |
isabelle_process |
|
57917 | 47 |
} |
57916 | 48 |
} |
71604 | 49 |
|
75393 | 50 |
class Isabelle_Process private(session: Session, process: Bash.Process) { |
71607 | 51 |
private val startup = Future.promise[String] |
52 |
private val terminated = Future.promise[Process_Result] |
|
71604 | 53 |
|
54 |
session.phase_changed += |
|
55 |
Session.Consumer(getClass.getName) { |
|
56 |
case Session.Ready => |
|
71607 | 57 |
startup.fulfill("") |
58 |
case Session.Terminated(result) => |
|
59 |
if (!result.ok && !startup.is_finished) { |
|
76488 | 60 |
val syslog = session.syslog.content() |
77368 | 61 |
val err = "Session startup failed" + if_proper(syslog, ":\n" + syslog) |
71607 | 62 |
startup.fulfill(err) |
63 |
} |
|
64 |
terminated.fulfill(result) |
|
71604 | 65 |
case _ => |
66 |
} |
|
67 |
||
71607 | 68 |
def await_startup(): Isabelle_Process = |
69 |
startup.join match { |
|
70 |
case "" => this |
|
71 |
case err => session.stop(); error(err) |
|
71604 | 72 |
} |
73 |
||
75393 | 74 |
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
|
75 |
val result = terminated.join |
4d2de35214c5
proper treatment of protocol exceptions and prover termination: avoid session.stop while saving image;
wenzelm
parents:
71639
diff
changeset
|
76 |
session.stop() |
4d2de35214c5
proper treatment of protocol exceptions and prover termination: avoid session.stop while saving image;
wenzelm
parents:
71639
diff
changeset
|
77 |
result |
4d2de35214c5
proper treatment of protocol exceptions and prover termination: avoid session.stop while saving image;
wenzelm
parents:
71639
diff
changeset
|
78 |
} |
71718 | 79 |
|
73367 | 80 |
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
|
81 |
} |