author | wenzelm |
Sat, 01 Jun 2024 12:35:38 +0200 | |
changeset 80225 | d9ff4296e3b7 |
parent 80224 | db92e0b6a11a |
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 |
|
12 |
||
75393 | 13 |
object Isabelle_Process { |
73802 | 14 |
def start( |
65216 | 15 |
options: Options, |
76729 | 16 |
session: Session, |
76656 | 17 |
session_background: Sessions.Background, |
77414
0d5994eef9e6
clarified signature: allow to provide session_heaps by different means, e.g. from tmp directory or alternative session structure;
wenzelm
parents:
77368
diff
changeset
|
18 |
session_heaps: List[Path], |
71639
ec84f542e411
clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
wenzelm
parents:
71607
diff
changeset
|
19 |
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
|
20 |
eval_main: String = "", |
65216 | 21 |
modes: List[String] = Nil, |
80224
db92e0b6a11a
clarified signature: prefer symbolic isabelle.Path over physical java.io.File;
wenzelm
parents:
79053
diff
changeset
|
22 |
cwd: Path = Path.current, |
75393 | 23 |
env: JMap[String, String] = Isabelle_System.settings() |
24 |
): Isabelle_Process = { |
|
79053
badb3da19ac6
disable unix_domain for now: somewhat unstable, e.g. "isabelle build -b HOL-Analysis" on arm64_32-darwin (studio1);
wenzelm
parents:
79050
diff
changeset
|
25 |
val channel = System_Channel() |
62556
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62555
diff
changeset
|
26 |
val process = |
57916 | 27 |
try { |
76729 | 28 |
val ml_options = |
29 |
options. |
|
30 |
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
|
31 |
string.update("system_channel_password", channel.password) |
77414
0d5994eef9e6
clarified signature: allow to provide session_heaps by different means, e.g. from tmp directory or alternative session structure;
wenzelm
parents:
77368
diff
changeset
|
32 |
ML_Process(ml_options, session_background, session_heaps, |
71639
ec84f542e411
clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
wenzelm
parents:
71607
diff
changeset
|
33 |
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
|
34 |
modes = modes, cwd = cwd, env = env) |
57916 | 35 |
} |
69572
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
68209
diff
changeset
|
36 |
catch { case exn @ ERROR(_) => channel.shutdown(); throw exn } |
57917 | 37 |
|
73802 | 38 |
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
|
39 |
process.stdin.close() |
73802 | 40 |
session.start(receiver => new Prover(receiver, session.cache, channel, process)) |
41 |
||
42 |
isabelle_process |
|
57917 | 43 |
} |
57916 | 44 |
} |
71604 | 45 |
|
75393 | 46 |
class Isabelle_Process private(session: Session, process: Bash.Process) { |
71607 | 47 |
private val startup = Future.promise[String] |
48 |
private val terminated = Future.promise[Process_Result] |
|
71604 | 49 |
|
50 |
session.phase_changed += |
|
51 |
Session.Consumer(getClass.getName) { |
|
52 |
case Session.Ready => |
|
71607 | 53 |
startup.fulfill("") |
54 |
case Session.Terminated(result) => |
|
55 |
if (!result.ok && !startup.is_finished) { |
|
76488 | 56 |
val syslog = session.syslog.content() |
77368 | 57 |
val err = "Session startup failed" + if_proper(syslog, ":\n" + syslog) |
71607 | 58 |
startup.fulfill(err) |
59 |
} |
|
60 |
terminated.fulfill(result) |
|
71604 | 61 |
case _ => |
62 |
} |
|
63 |
||
71607 | 64 |
def await_startup(): Isabelle_Process = |
65 |
startup.join match { |
|
66 |
case "" => this |
|
67 |
case err => session.stop(); error(err) |
|
71604 | 68 |
} |
69 |
||
75393 | 70 |
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
|
71 |
val result = terminated.join |
4d2de35214c5
proper treatment of protocol exceptions and prover termination: avoid session.stop while saving image;
wenzelm
parents:
71639
diff
changeset
|
72 |
session.stop() |
4d2de35214c5
proper treatment of protocol exceptions and prover termination: avoid session.stop while saving image;
wenzelm
parents:
71639
diff
changeset
|
73 |
result |
4d2de35214c5
proper treatment of protocol exceptions and prover termination: avoid session.stop while saving image;
wenzelm
parents:
71639
diff
changeset
|
74 |
} |
71718 | 75 |
|
73367 | 76 |
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
|
77 |
} |