46 /* process and result */ |
46 /* process and result */ |
47 |
47 |
48 private def make_description(description: String): String = |
48 private def make_description(description: String): String = |
49 proper_string(description) getOrElse "bash_process" |
49 proper_string(description) getOrElse "bash_process" |
50 |
50 |
|
51 def local_bash_process(): String = |
|
52 File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")) |
|
53 |
|
54 def local_bash(): String = |
|
55 if (Platform.is_unix) "bash" |
|
56 else isabelle.setup.Environment.cygwin_root() + "\\bin\\bash.exe" |
|
57 |
|
58 def remote_bash_process(ssh: SSH.Session): String = { |
|
59 val component = Components.provide(Component_Bash_Process.home, ssh = ssh) |
|
60 val exe = Component_Bash_Process.remote_program(component) |
|
61 ssh.make_command(args_host = true, args = ssh.bash_path(exe)) |
|
62 } |
|
63 |
51 type Watchdog = (Time, Process => Boolean) |
64 type Watchdog = (Time, Process => Boolean) |
52 |
65 |
53 def process(script: String, |
66 def process(script: String, |
54 description: String = "", |
67 description: String = "", |
|
68 ssh: SSH.System = SSH.Local, |
55 cwd: JFile = null, |
69 cwd: JFile = null, |
56 env: JMap[String, String] = Isabelle_System.settings(), |
70 env: JMap[String, String] = Isabelle_System.settings(), |
57 redirect: Boolean = false, |
71 redirect: Boolean = false, |
58 cleanup: () => Unit = () => ()): Process = |
72 cleanup: () => Unit = () => ()): Process = |
59 new Process(script, description, cwd, env, redirect, cleanup) |
73 new Process(script, description, ssh, cwd, env, redirect, cleanup) |
60 |
74 |
61 class Process private[Bash]( |
75 class Process private[Bash]( |
62 script: String, |
76 script: String, |
63 description: String, |
77 description: String, |
|
78 ssh: SSH.System, |
64 cwd: JFile, |
79 cwd: JFile, |
65 env: JMap[String, String], |
80 env: JMap[String, String], |
66 redirect: Boolean, |
81 redirect: Boolean, |
67 cleanup: () => Unit |
82 cleanup: () => Unit |
68 ) { |
83 ) { |
69 override def toString: String = make_description(description) |
84 override def toString: String = make_description(description) |
70 |
85 |
71 private val timing_file = Isabelle_System.tmp_file("bash_timing") |
86 private val proc_command: JList[String] = new LinkedList[String] |
|
87 |
|
88 private val winpid_file: Option[JFile] = |
|
89 if (ssh.is_local && Platform.is_windows) Some(Isabelle_System.tmp_file("bash_winpid")) |
|
90 else None |
|
91 private val winpid_script = |
|
92 winpid_file match { |
|
93 case None => "" |
|
94 case Some(file) => |
|
95 "read < /proc/self/winpid > /dev/null 2> /dev/null\n" + |
|
96 """echo -n "$REPLY" > """ + File.bash_path(file) + "\n\n" |
|
97 } |
|
98 |
|
99 private val timing_file = ssh.tmp_file("bash_timing") |
72 private val timing = Synchronized[Option[Timing]](None) |
100 private val timing = Synchronized[Option[Timing]](None) |
73 def get_timing: Timing = timing.value getOrElse Timing.zero |
101 def get_timing: Timing = timing.value getOrElse Timing.zero |
74 |
102 |
75 private val winpid_file: Option[JFile] = |
103 private val script_file: Path = ssh.tmp_file("bash_script") |
76 if (Platform.is_windows) Some(Isabelle_System.tmp_file("bash_winpid")) else None |
104 ssh.write(script_file, winpid_script + script) |
77 private val winpid_script = |
105 |
78 winpid_file match { |
106 private val ssh_file: Option[JFile] = |
79 case None => script |
107 ssh.ssh_session match { |
80 case Some(file) => |
108 case None => |
81 "read < /proc/self/winpid > /dev/null 2> /dev/null\n" + |
109 proc_command.add(local_bash_process()) |
82 """echo -n "$REPLY" > """ + File.bash_path(file) + "\n\n" + script |
110 proc_command.add(File.platform_path(timing_file)) |
83 } |
111 proc_command.add("bash") |
84 |
112 proc_command.add(File.platform_path(script_file)) |
85 private val script_file: JFile = Isabelle_System.tmp_file("bash_script") |
113 None |
86 File.write(script_file, winpid_script) |
114 case Some(ssh_session) => |
|
115 val ssh_script = |
|
116 "exec " + remote_bash_process(ssh_session) + " " + |
|
117 ssh.bash_path(timing_file) + " bash " + |
|
118 ssh.bash_path(script_file) |
|
119 val file = Isabelle_System.tmp_file("bash_ssh") |
|
120 File.write(file, ssh_script) |
|
121 proc_command.add(local_bash()) |
|
122 proc_command.add(file.getPath) |
|
123 Some(file) |
|
124 } |
87 |
125 |
88 private val proc = |
126 private val proc = |
89 isabelle.setup.Environment.process_builder( |
127 isabelle.setup.Environment.process_builder(proc_command, cwd, env, redirect).start() |
90 JList.of(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), |
|
91 File.standard_path(timing_file), "bash", File.standard_path(script_file)), |
|
92 cwd, env, redirect).start() |
|
93 |
128 |
94 |
129 |
95 // channels |
130 // channels |
96 |
131 |
97 val stdin: BufferedWriter = |
132 val stdin: BufferedWriter = |
106 |
141 |
107 // signals |
142 // signals |
108 |
143 |
109 private val group_pid = stdout.readLine |
144 private val group_pid = stdout.readLine |
110 |
145 |
111 private def process_alive(pid: String): Boolean = |
146 private def local_process_alive(pid: String): Boolean = |
112 (for { |
147 ssh.is_local && |
113 p <- Value.Long.unapply(pid) |
148 (for { |
114 handle <- ProcessHandle.of(p).toScala |
149 p <- Value.Long.unapply(pid) |
115 } yield handle.isAlive) getOrElse false |
150 handle <- ProcessHandle.of(p).toScala |
|
151 } yield handle.isAlive).getOrElse(false) |
116 |
152 |
117 private def root_process_alive(): Boolean = |
153 private def root_process_alive(): Boolean = |
118 winpid_file match { |
154 winpid_file match { |
119 case None => process_alive(group_pid) |
155 case None => local_process_alive(group_pid) |
120 case Some(file) => |
156 case Some(file) => |
121 file.exists() && process_alive(Library.trim_line(File.read(file))) |
157 file.exists() && local_process_alive(Library.trim_line(File.read(file))) |
122 } |
158 } |
123 |
159 |
124 @tailrec private def signal(s: String, count: Int = 1): Boolean = { |
160 @tailrec private def signal(s: String, count: Int = 1): Boolean = { |
125 count <= 0 || { |
161 count <= 0 || { |
126 isabelle.setup.Environment.kill_process(group_pid, s) |
162 ssh.kill_process(group_pid, s) |
127 val running = |
163 val running = root_process_alive() || ssh.kill_process(group_pid, "0") |
128 root_process_alive() || |
|
129 isabelle.setup.Environment.kill_process(group_pid, "0") |
|
130 if (running) { |
164 if (running) { |
131 Time.seconds(0.1).sleep() |
165 Time.seconds(if (ssh.is_local) 0.1 else 0.25).sleep() |
132 signal(s, count - 1) |
166 signal(s, count - 1) |
133 } |
167 } |
134 else false |
168 else false |
135 } |
169 } |
136 } |
170 } |
152 Isabelle_System.create_shutdown_hook { terminate() } |
186 Isabelle_System.create_shutdown_hook { terminate() } |
153 |
187 |
154 private def do_cleanup(): Unit = { |
188 private def do_cleanup(): Unit = { |
155 Isabelle_System.remove_shutdown_hook(shutdown_hook) |
189 Isabelle_System.remove_shutdown_hook(shutdown_hook) |
156 |
190 |
157 script_file.delete() |
|
158 winpid_file.foreach(_.delete()) |
191 winpid_file.foreach(_.delete()) |
|
192 ssh_file.foreach(_.delete()) |
|
193 |
|
194 ssh.delete(script_file) |
159 |
195 |
160 timing.change { |
196 timing.change { |
161 case None => |
197 case None => |
162 if (timing_file.isFile) { |
198 if (ssh.is_file(timing_file)) { |
163 val t = |
199 val t = |
164 Word.explode(File.read(timing_file)) match { |
200 Word.explode(ssh.read(timing_file)) match { |
165 case List(Value.Long(elapsed), Value.Long(cpu)) => |
201 case List(Value.Long(elapsed), Value.Long(cpu)) => |
166 Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero) |
202 Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero) |
167 case _ => Timing.zero |
203 case _ => Timing.zero |
168 } |
204 } |
169 timing_file.delete |
205 ssh.delete(timing_file) |
170 Some(t) |
206 Some(t) |
171 } |
207 } |
172 else Some(Timing.zero) |
208 else Some(Timing.zero) |
173 case some => some |
209 case some => some |
174 } |
210 } |