wenzelm@30176
|
1 |
/* Title: Pure/System/isabelle_system.scala
|
wenzelm@27919
|
2 |
Author: Makarius
|
wenzelm@27919
|
3 |
|
wenzelm@44569
|
4 |
Fundamental Isabelle system environment: quasi-static module with
|
wenzelm@44569
|
5 |
optional init operation.
|
wenzelm@27919
|
6 |
*/
|
wenzelm@27919
|
7 |
|
wenzelm@27919
|
8 |
package isabelle
|
wenzelm@27919
|
9 |
|
wenzelm@44400
|
10 |
import java.lang.System
|
wenzelm@31535
|
11 |
import java.util.regex.Pattern
|
wenzelm@31820
|
12 |
import java.util.Locale
|
wenzelm@39840
|
13 |
import java.io.{InputStream, FileInputStream, OutputStream, FileOutputStream, File,
|
wenzelm@39847
|
14 |
BufferedReader, InputStreamReader, BufferedWriter, OutputStreamWriter, IOException}
|
wenzelm@34024
|
15 |
import java.awt.{GraphicsEnvironment, Font}
|
wenzelm@37468
|
16 |
import java.awt.font.TextAttribute
|
wenzelm@28063
|
17 |
|
wenzelm@28063
|
18 |
import scala.io.Source
|
wenzelm@31535
|
19 |
import scala.util.matching.Regex
|
wenzelm@34170
|
20 |
import scala.collection.mutable
|
wenzelm@27936
|
21 |
|
wenzelm@27919
|
22 |
|
wenzelm@44385
|
23 |
object Isabelle_System
|
wenzelm@44385
|
24 |
{
|
wenzelm@44532
|
25 |
/** implicit state **/
|
wenzelm@44385
|
26 |
|
wenzelm@44569
|
27 |
private case class State(standard_system: Standard_System, settings: Map[String, String])
|
wenzelm@37024
|
28 |
|
wenzelm@44532
|
29 |
@volatile private var _state: Option[State] = None
|
wenzelm@37024
|
30 |
|
wenzelm@44532
|
31 |
private def check_state(): State =
|
wenzelm@44532
|
32 |
{
|
wenzelm@44532
|
33 |
if (_state.isEmpty) init() // unsynchronized check
|
wenzelm@44532
|
34 |
_state.get
|
wenzelm@44532
|
35 |
}
|
wenzelm@44532
|
36 |
|
wenzelm@44532
|
37 |
def standard_system: Standard_System = check_state().standard_system
|
wenzelm@44532
|
38 |
def settings: Map[String, String] = check_state().settings
|
wenzelm@31799
|
39 |
|
wenzelm@37024
|
40 |
/*
|
wenzelm@37024
|
41 |
isabelle_home precedence:
|
wenzelm@37024
|
42 |
(1) this_isabelle_home as explicit argument
|
wenzelm@37024
|
43 |
(2) ISABELLE_HOME process environment variable (e.g. inherited from running isabelle tool)
|
wenzelm@37024
|
44 |
(3) isabelle.home system property (e.g. via JVM application boot process)
|
wenzelm@37024
|
45 |
*/
|
wenzelm@44532
|
46 |
def init(this_isabelle_home: String = null) = synchronized {
|
wenzelm@44532
|
47 |
if (_state.isEmpty) {
|
wenzelm@44532
|
48 |
import scala.collection.JavaConversions._
|
wenzelm@37024
|
49 |
|
wenzelm@44569
|
50 |
System.err.println("### Isabelle system initialization")
|
wenzelm@44569
|
51 |
|
wenzelm@44532
|
52 |
val standard_system = new Standard_System
|
wenzelm@44532
|
53 |
val settings =
|
wenzelm@44532
|
54 |
{
|
wenzelm@44532
|
55 |
val env = Map(System.getenv.toList: _*) +
|
wenzelm@44532
|
56 |
("THIS_JAVA" -> standard_system.this_java())
|
wenzelm@31484
|
57 |
|
wenzelm@44532
|
58 |
val isabelle_home =
|
wenzelm@44532
|
59 |
if (this_isabelle_home != null) this_isabelle_home
|
wenzelm@44532
|
60 |
else
|
wenzelm@44532
|
61 |
env.get("ISABELLE_HOME") match {
|
wenzelm@44532
|
62 |
case None | Some("") =>
|
wenzelm@44532
|
63 |
val path = System.getProperty("isabelle.home")
|
wenzelm@44532
|
64 |
if (path == null || path == "") error("Unknown Isabelle home directory")
|
wenzelm@44532
|
65 |
else path
|
wenzelm@44532
|
66 |
case Some(path) => path
|
wenzelm@44532
|
67 |
}
|
wenzelm@31484
|
68 |
|
wenzelm@44532
|
69 |
Standard_System.with_tmp_file("settings") { dump =>
|
wenzelm@44532
|
70 |
val shell_prefix =
|
wenzelm@44532
|
71 |
if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\bash", "-l")
|
wenzelm@44532
|
72 |
else Nil
|
wenzelm@44532
|
73 |
val cmdline =
|
wenzelm@44532
|
74 |
shell_prefix ::: List(isabelle_home + "/bin/isabelle", "getenv", "-d", dump.toString)
|
wenzelm@44532
|
75 |
val (output, rc) = Standard_System.raw_exec(null, env, true, cmdline: _*)
|
wenzelm@44532
|
76 |
if (rc != 0) error(output)
|
wenzelm@31484
|
77 |
|
wenzelm@44532
|
78 |
val entries =
|
wenzelm@44532
|
79 |
for (entry <- Source.fromFile(dump).mkString split "\0" if entry != "") yield {
|
wenzelm@44532
|
80 |
val i = entry.indexOf('=')
|
wenzelm@44532
|
81 |
if (i <= 0) (entry -> "")
|
wenzelm@44532
|
82 |
else (entry.substring(0, i) -> entry.substring(i + 1))
|
wenzelm@44532
|
83 |
}
|
wenzelm@44532
|
84 |
Map(entries: _*) +
|
wenzelm@44532
|
85 |
("HOME" -> System.getenv("HOME")) +
|
wenzelm@44532
|
86 |
("PATH" -> System.getenv("PATH"))
|
wenzelm@44532
|
87 |
}
|
wenzelm@34201
|
88 |
}
|
wenzelm@44569
|
89 |
_state = Some(State(standard_system, settings))
|
wenzelm@44532
|
90 |
}
|
wenzelm@27953
|
91 |
}
|
wenzelm@27919
|
92 |
|
wenzelm@31799
|
93 |
|
wenzelm@31799
|
94 |
/* getenv */
|
wenzelm@31799
|
95 |
|
wenzelm@31484
|
96 |
def getenv(name: String): String =
|
wenzelm@44532
|
97 |
settings.getOrElse(if (name == "HOME") "HOME_JVM" else name, "")
|
wenzelm@31484
|
98 |
|
wenzelm@31484
|
99 |
def getenv_strict(name: String): String =
|
wenzelm@31484
|
100 |
{
|
wenzelm@31234
|
101 |
val value = getenv(name)
|
wenzelm@27993
|
102 |
if (value != "") value else error("Undefined environment variable: " + name)
|
wenzelm@27919
|
103 |
}
|
wenzelm@27919
|
104 |
|
wenzelm@31799
|
105 |
|
wenzelm@44479
|
106 |
/** file-system operations **/
|
wenzelm@31799
|
107 |
|
wenzelm@44479
|
108 |
/* path specifications */
|
wenzelm@31799
|
109 |
|
wenzelm@44539
|
110 |
def standard_path(path: Path): String = path.expand.implode
|
wenzelm@36144
|
111 |
|
wenzelm@44532
|
112 |
def platform_path(path: Path): String = standard_system.jvm_path(standard_path(path))
|
wenzelm@44479
|
113 |
def platform_file(path: Path) = new File(platform_path(path))
|
wenzelm@29152
|
114 |
|
wenzelm@44532
|
115 |
def posix_path(jvm_path: String): String = standard_system.posix_path(jvm_path)
|
wenzelm@44532
|
116 |
|
wenzelm@27953
|
117 |
|
wenzelm@37006
|
118 |
/* try_read */
|
wenzelm@37006
|
119 |
|
wenzelm@44479
|
120 |
def try_read(paths: Seq[Path]): String =
|
wenzelm@37006
|
121 |
{
|
wenzelm@37098
|
122 |
val buf = new StringBuilder
|
wenzelm@37098
|
123 |
for {
|
wenzelm@37098
|
124 |
path <- paths
|
wenzelm@37098
|
125 |
file = platform_file(path) if file.isFile
|
wenzelm@37098
|
126 |
c <- (Source.fromFile(file) ++ Iterator.single('\n'))
|
wenzelm@37098
|
127 |
} buf.append(c)
|
wenzelm@37098
|
128 |
buf.toString
|
wenzelm@37006
|
129 |
}
|
wenzelm@37006
|
130 |
|
wenzelm@37006
|
131 |
|
wenzelm@31440
|
132 |
/* source files */
|
wenzelm@31440
|
133 |
|
wenzelm@31440
|
134 |
private def try_file(file: File) = if (file.isFile) Some(file) else None
|
wenzelm@31440
|
135 |
|
wenzelm@44479
|
136 |
def source_file(path: Path): Option[File] =
|
wenzelm@31484
|
137 |
{
|
wenzelm@44479
|
138 |
if (path.is_absolute || path.is_current)
|
wenzelm@31440
|
139 |
try_file(platform_file(path))
|
wenzelm@31440
|
140 |
else {
|
wenzelm@44479
|
141 |
val pure_file = platform_file(Path.explode("~~/src/Pure") + path)
|
wenzelm@31440
|
142 |
if (pure_file.isFile) Some(pure_file)
|
wenzelm@31440
|
143 |
else if (getenv("ML_SOURCES") != "")
|
wenzelm@44479
|
144 |
try_file(platform_file(Path.explode("$ML_SOURCES") + path))
|
wenzelm@31440
|
145 |
else None
|
wenzelm@31440
|
146 |
}
|
wenzelm@31440
|
147 |
}
|
wenzelm@31440
|
148 |
|
wenzelm@31440
|
149 |
|
wenzelm@32450
|
150 |
|
wenzelm@39847
|
151 |
/** external processes **/
|
wenzelm@39847
|
152 |
|
wenzelm@39847
|
153 |
/* plain execute */
|
wenzelm@39847
|
154 |
|
wenzelm@39847
|
155 |
def execute(redirect: Boolean, args: String*): Process =
|
wenzelm@39847
|
156 |
{
|
wenzelm@39847
|
157 |
val cmdline =
|
wenzelm@44532
|
158 |
if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\env.exe") ++ args
|
wenzelm@39847
|
159 |
else args
|
wenzelm@44532
|
160 |
Standard_System.raw_execute(null, settings, redirect, cmdline: _*)
|
wenzelm@39847
|
161 |
}
|
wenzelm@39847
|
162 |
|
wenzelm@39847
|
163 |
|
wenzelm@39847
|
164 |
/* managed process */
|
wenzelm@39847
|
165 |
|
wenzelm@39847
|
166 |
class Managed_Process(redirect: Boolean, args: String*)
|
wenzelm@39847
|
167 |
{
|
wenzelm@39847
|
168 |
private val params =
|
wenzelm@44479
|
169 |
List(standard_path(Path.explode("~~/lib/scripts/process")), "group", "-", "no_script")
|
wenzelm@39847
|
170 |
private val proc = execute(redirect, (params ++ args):_*)
|
wenzelm@39847
|
171 |
|
wenzelm@39847
|
172 |
|
wenzelm@39847
|
173 |
// channels
|
wenzelm@39847
|
174 |
|
wenzelm@39847
|
175 |
val stdin: BufferedWriter =
|
wenzelm@39847
|
176 |
new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, Standard_System.charset))
|
wenzelm@39847
|
177 |
|
wenzelm@39847
|
178 |
val stdout: BufferedReader =
|
wenzelm@39847
|
179 |
new BufferedReader(new InputStreamReader(proc.getInputStream, Standard_System.charset))
|
wenzelm@39847
|
180 |
|
wenzelm@39847
|
181 |
val stderr: BufferedReader =
|
wenzelm@39847
|
182 |
new BufferedReader(new InputStreamReader(proc.getErrorStream, Standard_System.charset))
|
wenzelm@39847
|
183 |
|
wenzelm@39847
|
184 |
|
wenzelm@39847
|
185 |
// signals
|
wenzelm@39847
|
186 |
|
wenzelm@39847
|
187 |
private val pid = stdout.readLine
|
wenzelm@39847
|
188 |
|
wenzelm@39847
|
189 |
private def kill(signal: String): Boolean =
|
wenzelm@39848
|
190 |
{
|
wenzelm@39848
|
191 |
execute(true, "kill", "-" + signal, "-" + pid).waitFor
|
wenzelm@39848
|
192 |
execute(true, "kill", "-0", "-" + pid).waitFor == 0
|
wenzelm@39848
|
193 |
}
|
wenzelm@39847
|
194 |
|
wenzelm@39847
|
195 |
private def multi_kill(signal: String): Boolean =
|
wenzelm@39847
|
196 |
{
|
wenzelm@39847
|
197 |
var running = true
|
wenzelm@39847
|
198 |
var count = 10
|
wenzelm@39847
|
199 |
while (running && count > 0) {
|
wenzelm@39847
|
200 |
if (kill(signal)) {
|
wenzelm@39847
|
201 |
Thread.sleep(100)
|
wenzelm@39847
|
202 |
count -= 1
|
wenzelm@39847
|
203 |
}
|
wenzelm@39847
|
204 |
else running = false
|
wenzelm@39847
|
205 |
}
|
wenzelm@39847
|
206 |
running
|
wenzelm@39847
|
207 |
}
|
wenzelm@39847
|
208 |
|
wenzelm@39847
|
209 |
def interrupt() { multi_kill("INT") }
|
wenzelm@39847
|
210 |
def terminate() { multi_kill("INT") && multi_kill("TERM") && kill("KILL"); proc.destroy }
|
wenzelm@39847
|
211 |
|
wenzelm@39847
|
212 |
|
wenzelm@39847
|
213 |
// JVM shutdown hook
|
wenzelm@39847
|
214 |
|
wenzelm@39847
|
215 |
private val shutdown_hook = new Thread { override def run = terminate() }
|
wenzelm@39847
|
216 |
|
wenzelm@39847
|
217 |
try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
|
wenzelm@39847
|
218 |
catch { case _: IllegalStateException => }
|
wenzelm@39847
|
219 |
|
wenzelm@39847
|
220 |
private def cleanup() =
|
wenzelm@39847
|
221 |
try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
|
wenzelm@39847
|
222 |
catch { case _: IllegalStateException => }
|
wenzelm@39847
|
223 |
|
wenzelm@39847
|
224 |
|
wenzelm@39847
|
225 |
/* result */
|
wenzelm@39847
|
226 |
|
wenzelm@39847
|
227 |
def join: Int = { val rc = proc.waitFor; cleanup(); rc }
|
wenzelm@39847
|
228 |
}
|
wenzelm@39847
|
229 |
|
wenzelm@39847
|
230 |
|
wenzelm@39847
|
231 |
/* bash */
|
wenzelm@31799
|
232 |
|
wenzelm@39845
|
233 |
def bash(script: String): (String, String, Int) =
|
wenzelm@34198
|
234 |
{
|
wenzelm@34201
|
235 |
Standard_System.with_tmp_file("isabelle_script") { script_file =>
|
wenzelm@39845
|
236 |
Standard_System.write_file(script_file, script)
|
wenzelm@39847
|
237 |
val proc = new Managed_Process(false, "bash", posix_path(script_file.getPath))
|
wenzelm@34198
|
238 |
|
wenzelm@39847
|
239 |
proc.stdin.close
|
wenzelm@39850
|
240 |
val stdout = Simple_Thread.future("bash_stdout") { Standard_System.slurp(proc.stdout) }
|
wenzelm@39850
|
241 |
val stderr = Simple_Thread.future("bash_stderr") { Standard_System.slurp(proc.stderr) }
|
wenzelm@34198
|
242 |
|
wenzelm@39845
|
243 |
val rc =
|
wenzelm@39847
|
244 |
try { proc.join }
|
wenzelm@39847
|
245 |
catch { case e: InterruptedException => Thread.interrupted; proc.terminate; 130 }
|
wenzelm@39845
|
246 |
(stdout.join, stderr.join, rc)
|
wenzelm@34198
|
247 |
}
|
wenzelm@34198
|
248 |
}
|
wenzelm@34198
|
249 |
|
wenzelm@39847
|
250 |
|
wenzelm@39847
|
251 |
/* system tools */
|
wenzelm@39847
|
252 |
|
wenzelm@31818
|
253 |
def isabelle_tool(name: String, args: String*): (String, Int) =
|
wenzelm@31484
|
254 |
{
|
wenzelm@44544
|
255 |
Path.split(getenv_strict("ISABELLE_TOOLS")).find { dir =>
|
wenzelm@44544
|
256 |
val file = platform_file(dir + Path.basic(name))
|
wenzelm@42995
|
257 |
try {
|
wenzelm@42995
|
258 |
file.isFile && file.canRead && file.canExecute &&
|
wenzelm@42995
|
259 |
!name.endsWith("~") && !name.endsWith(".orig")
|
wenzelm@42995
|
260 |
}
|
wenzelm@31818
|
261 |
catch { case _: SecurityException => false }
|
wenzelm@34200
|
262 |
} match {
|
wenzelm@31818
|
263 |
case Some(dir) =>
|
wenzelm@44544
|
264 |
val file = standard_path(dir + Path.basic(name))
|
wenzelm@44479
|
265 |
Standard_System.process_output(execute(true, (List(file) ++ args): _*))
|
wenzelm@31818
|
266 |
case None => ("Unknown Isabelle tool: " + name, 2)
|
wenzelm@31818
|
267 |
}
|
wenzelm@28063
|
268 |
}
|
wenzelm@28063
|
269 |
|
wenzelm@28063
|
270 |
|
wenzelm@28063
|
271 |
/* named pipes */
|
wenzelm@28063
|
272 |
|
wenzelm@44531
|
273 |
private val next_fifo = new Counter
|
wenzelm@39789
|
274 |
|
wenzelm@31484
|
275 |
def mk_fifo(): String =
|
wenzelm@31484
|
276 |
{
|
wenzelm@39798
|
277 |
val i = next_fifo()
|
wenzelm@39798
|
278 |
val script =
|
wenzelm@44531
|
279 |
"FIFO=\"/tmp/isabelle-fifo-${PPID}-$$" + i + "\"\n" +
|
wenzelm@39964
|
280 |
"echo -n \"$FIFO\"\n" +
|
wenzelm@39964
|
281 |
"mkfifo -m 600 \"$FIFO\"\n"
|
wenzelm@39845
|
282 |
val (out, err, rc) = bash(script)
|
wenzelm@39964
|
283 |
if (rc == 0) out else error(err.trim)
|
wenzelm@28063
|
284 |
}
|
wenzelm@28063
|
285 |
|
wenzelm@39838
|
286 |
def rm_fifo(fifo: String): Boolean =
|
wenzelm@44532
|
287 |
(new File(standard_system.jvm_path(if (Platform.is_windows) fifo + ".lnk" else fifo))).delete
|
wenzelm@28063
|
288 |
|
wenzelm@38653
|
289 |
def fifo_input_stream(fifo: String): InputStream =
|
wenzelm@31484
|
290 |
{
|
wenzelm@38653
|
291 |
if (Platform.is_windows) { // Cygwin fifo as Windows/Java input stream
|
wenzelm@44479
|
292 |
val proc = execute(false, standard_path(Path.explode("~~/lib/scripts/raw_dump")), fifo, "-")
|
wenzelm@38653
|
293 |
proc.getOutputStream.close
|
wenzelm@38653
|
294 |
proc.getErrorStream.close
|
wenzelm@38653
|
295 |
proc.getInputStream
|
wenzelm@38653
|
296 |
}
|
wenzelm@38653
|
297 |
else new FileInputStream(fifo)
|
wenzelm@29177
|
298 |
}
|
wenzelm@28063
|
299 |
|
wenzelm@38653
|
300 |
def fifo_output_stream(fifo: String): OutputStream =
|
wenzelm@38551
|
301 |
{
|
wenzelm@38653
|
302 |
if (Platform.is_windows) { // Cygwin fifo as Windows/Java output stream
|
wenzelm@44479
|
303 |
val proc = execute(false, standard_path(Path.explode("~~/lib/scripts/raw_dump")), "-", fifo)
|
wenzelm@38653
|
304 |
proc.getInputStream.close
|
wenzelm@38653
|
305 |
proc.getErrorStream.close
|
wenzelm@38653
|
306 |
val out = proc.getOutputStream
|
wenzelm@38653
|
307 |
new OutputStream {
|
wenzelm@38653
|
308 |
override def close() { out.close(); proc.waitFor() }
|
wenzelm@38653
|
309 |
override def flush() { out.flush() }
|
wenzelm@38653
|
310 |
override def write(b: Array[Byte]) { out.write(b) }
|
wenzelm@38653
|
311 |
override def write(b: Array[Byte], off: Int, len: Int) { out.write(b, off, len) }
|
wenzelm@38653
|
312 |
override def write(b: Int) { out.write(b) }
|
wenzelm@38551
|
313 |
}
|
wenzelm@38653
|
314 |
}
|
wenzelm@38653
|
315 |
else new FileOutputStream(fifo)
|
wenzelm@38551
|
316 |
}
|
wenzelm@38551
|
317 |
|
wenzelm@29152
|
318 |
|
wenzelm@32450
|
319 |
|
wenzelm@31799
|
320 |
/** Isabelle resources **/
|
wenzelm@31799
|
321 |
|
wenzelm@32328
|
322 |
/* components */
|
wenzelm@32328
|
323 |
|
wenzelm@44544
|
324 |
def components(): List[Path] =
|
wenzelm@44544
|
325 |
Path.split(getenv_strict("ISABELLE_COMPONENTS"))
|
wenzelm@32328
|
326 |
|
wenzelm@32328
|
327 |
|
wenzelm@29152
|
328 |
/* find logics */
|
wenzelm@29152
|
329 |
|
wenzelm@31484
|
330 |
def find_logics(): List[String] =
|
wenzelm@31484
|
331 |
{
|
wenzelm@29152
|
332 |
val ml_ident = getenv_strict("ML_IDENTIFIER")
|
wenzelm@34170
|
333 |
val logics = new mutable.ListBuffer[String]
|
wenzelm@44544
|
334 |
for (dir <- Path.split(getenv_strict("ISABELLE_PATH"))) {
|
wenzelm@44544
|
335 |
val files = platform_file(dir + Path.explode(ml_ident)).listFiles()
|
wenzelm@29152
|
336 |
if (files != null) {
|
wenzelm@29152
|
337 |
for (file <- files if file.isFile) logics += file.getName
|
wenzelm@29152
|
338 |
}
|
wenzelm@29152
|
339 |
}
|
wenzelm@36036
|
340 |
logics.toList.sortWith(_ < _)
|
wenzelm@29152
|
341 |
}
|
wenzelm@29570
|
342 |
|
wenzelm@29570
|
343 |
|
wenzelm@34024
|
344 |
/* fonts */
|
wenzelm@34024
|
345 |
|
wenzelm@44355
|
346 |
def get_font(family: String = "IsabelleText", size: Int = 1, bold: Boolean = false): Font =
|
wenzelm@44355
|
347 |
new Font(family, if (bold) Font.BOLD else Font.PLAIN, size)
|
wenzelm@37468
|
348 |
|
wenzelm@34049
|
349 |
def install_fonts()
|
wenzelm@34049
|
350 |
{
|
wenzelm@37468
|
351 |
val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
|
wenzelm@44544
|
352 |
for (font <- Path.split(getenv_strict("ISABELLE_FONTS")))
|
wenzelm@44544
|
353 |
ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, platform_file(font)))
|
wenzelm@34024
|
354 |
}
|
wenzelm@27919
|
355 |
}
|