author | wenzelm |
Thu, 12 Aug 2021 14:18:46 +0200 | |
changeset 74147 | d030b988d470 |
parent 74142 | 0f051404f487 |
child 74210 | c14774713d62 |
permissions | -rw-r--r-- |
40743 | 1 |
(* Title: Pure/System/isabelle_system.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
Isabelle system support. |
|
5 |
*) |
|
6 |
||
7 |
signature ISABELLE_SYSTEM = |
|
8 |
sig |
|
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
9 |
val bash_process: Bash.params -> Process_Result.T |
71902
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
10 |
val bash_output: string -> string * int |
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
11 |
val bash: string -> int |
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
12 |
val bash_functions: unit -> string list |
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
13 |
val check_bash_function: Proof.context -> string * Position.T -> string |
73434
00b77365552e
clarified signature: refer to file name instead of file content;
wenzelm
parents:
73419
diff
changeset
|
14 |
val absolute_path: Path.T -> string |
72376 | 15 |
val make_directory: Path.T -> Path.T |
40743 | 16 |
val copy_dir: Path.T -> Path.T -> unit |
56533
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
17 |
val copy_file: Path.T -> Path.T -> unit |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
18 |
val copy_file_base: Path.T * Path.T -> Path.T -> unit |
42127
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
41944
diff
changeset
|
19 |
val create_tmp_path: string -> string -> Path.T |
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
41944
diff
changeset
|
20 |
val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a |
73324 | 21 |
val rm_tree: Path.T -> unit |
41307
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
22 |
val with_tmp_dir: string -> (Path.T -> 'a) -> 'a |
73566 | 23 |
val download: string -> string |
24 |
val download_file: string -> Path.T -> unit |
|
73775 | 25 |
val decode_base64: string -> string |
26 |
val encode_base64: string -> string |
|
73523
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73434
diff
changeset
|
27 |
val isabelle_id: unit -> string |
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73434
diff
changeset
|
28 |
val isabelle_identifier: unit -> string option |
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73434
diff
changeset
|
29 |
val isabelle_heading: unit -> string |
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73434
diff
changeset
|
30 |
val isabelle_name: unit -> string |
73547 | 31 |
val identification: unit -> string |
40743 | 32 |
end; |
33 |
||
34 |
structure Isabelle_System: ISABELLE_SYSTEM = |
|
35 |
struct |
|
36 |
||
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43849
diff
changeset
|
37 |
(* bash *) |
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43849
diff
changeset
|
38 |
|
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
39 |
val absolute_path = Path.implode o File.absolute_path; |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
40 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
41 |
fun bash_process params = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
42 |
let |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
43 |
val {script, input, cwd, putenv, redirect, timeout, description: string} = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
44 |
Bash.dest_params params; |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
45 |
val run = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
46 |
["run", script, input, |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
47 |
let open XML.Encode in YXML.string_of_body (option (string o absolute_path) cwd) end, |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
48 |
let open XML.Encode in YXML.string_of_body o list (pair string string) end |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
49 |
(("ISABELLE_TMP", getenv "ISABELLE_TMP") :: putenv), |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
50 |
Value.print_bool redirect, |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
51 |
Value.print_real (Time.toReal timeout), |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
52 |
description]; |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
53 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
54 |
val address = Options.default_string \<^system_option>\<open>bash_process_address\<close>; |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
55 |
val password = Options.default_string \<^system_option>\<open>bash_process_password\<close>; |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
56 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
57 |
val _ = address = "" andalso raise Fail "Bad bash_process server address"; |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
58 |
fun with_streams f = Socket_IO.with_streams' f address password; |
73264 | 59 |
|
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
60 |
fun kill (SOME uuid) = with_streams (fn s => Byte_Message.write_message (#2 s) ["kill", uuid]) |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
61 |
| kill NONE = (); |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
62 |
in |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
63 |
Thread_Attributes.uninterruptible (fn restore_attributes => fn () => |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
64 |
let |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
65 |
fun loop maybe_uuid streams = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
66 |
(case restore_attributes Byte_Message.read_message (#1 streams) of |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
67 |
SOME ["uuid", uuid] => loop (SOME uuid) streams |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
68 |
| SOME ["interrupt"] => raise Exn.Interrupt |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
69 |
| SOME ["failure", msg] => raise Fail msg |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
70 |
| SOME ("result" :: a :: b :: c :: d :: lines) => |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
71 |
let |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
72 |
val rc = Value.parse_int a; |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
73 |
val (elapsed, cpu) = apply2 (Time.fromMilliseconds o Value.parse_int) (b, c); |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
74 |
val (out_lines, err_lines) = chop (Value.parse_int d) lines; |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
75 |
in |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
76 |
if rc = Process_Result.timeout_rc then raise Timeout.TIMEOUT elapsed |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
77 |
else |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
78 |
Process_Result.make |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
79 |
{rc = rc, |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
80 |
out_lines = out_lines, |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
81 |
err_lines = err_lines, |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
82 |
timing = {elapsed = elapsed, cpu = cpu, gc = Time.zeroTime}} |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
83 |
end |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
84 |
| _ => raise Fail "Malformed bash_process server result") |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
85 |
handle exn => (kill maybe_uuid; Exn.reraise exn); |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
86 |
in with_streams (fn s => (Byte_Message.write_message (#2 s) run; loop NONE s)) end) () |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
87 |
end; |
73604 | 88 |
|
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
89 |
val bash = Bash.script #> bash_process #> Process_Result.print #> Process_Result.rc; |
73281 | 90 |
|
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43849
diff
changeset
|
91 |
fun bash_output s = |
47499
4b0daca2bf88
redirect bash stderr to Isabelle warning as appropriate -- avoid raw process error output which may either get ignored or overload PIDE syslog in extreme cases;
wenzelm
parents:
46502
diff
changeset
|
92 |
let |
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
93 |
val res = bash_process (Bash.script s); |
73277
0110e2e2964c
clarified signature: always trim_line of Process_Result.out/err, uniformly in ML and Scala;
wenzelm
parents:
73275
diff
changeset
|
94 |
val _ = warning (Process_Result.err res); |
73275 | 95 |
in (Process_Result.out res, Process_Result.rc res) end; |
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43849
diff
changeset
|
96 |
|
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43849
diff
changeset
|
97 |
|
71902
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
98 |
(* bash functions *) |
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
99 |
|
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
100 |
fun bash_functions () = |
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
101 |
bash_process (Bash.script "declare -Fx") |
73279 | 102 |
|> Process_Result.check |
103 |
|> Process_Result.out_lines |
|
104 |
|> map_filter (space_explode " " #> try List.last); |
|
71902
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
105 |
|
71911 | 106 |
fun check_bash_function ctxt arg = |
71912 | 107 |
Completion.check_entity Markup.bash_functionN |
108 |
(bash_functions () |> map (rpair Position.none)) ctxt arg; |
|
71902
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
109 |
|
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
110 |
|
73322 | 111 |
(* directory and file operations *) |
112 |
||
73567 | 113 |
fun scala_function name = ignore o Scala.function name o map absolute_path; |
40743 | 114 |
|
73322 | 115 |
fun make_directory path = (scala_function "make_directory" [path]; path); |
40743 | 116 |
|
73322 | 117 |
fun copy_dir src dst = scala_function "copy_dir" [src, dst]; |
40743 | 118 |
|
73322 | 119 |
fun copy_file src dst = scala_function "copy_file" [src, dst]; |
56533
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
120 |
|
73322 | 121 |
fun copy_file_base (base_dir, src) target_dir = |
73567 | 122 |
ignore (Scala.function "copy_file_base" |
123 |
[absolute_path base_dir, Path.implode src, absolute_path target_dir]); |
|
56533
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
124 |
|
41307
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
125 |
|
56498 | 126 |
(* tmp files *) |
41307
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
127 |
|
42127
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
41944
diff
changeset
|
128 |
fun create_tmp_path name ext = |
41307
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
129 |
let |
42127
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
41944
diff
changeset
|
130 |
val path = File.tmp_path (Path.basic (name ^ serial_string ()) |> Path.ext ext); |
41307
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
131 |
val _ = File.exists path andalso |
41944
b97091ae583a
Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
wenzelm
parents:
41352
diff
changeset
|
132 |
raise Fail ("Temporary file already exists: " ^ Path.print path); |
41307
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
133 |
in path end; |
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
134 |
|
42127
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
41944
diff
changeset
|
135 |
fun with_tmp_file name ext f = |
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
41944
diff
changeset
|
136 |
let val path = create_tmp_path name ext |
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
41944
diff
changeset
|
137 |
in Exn.release (Exn.capture f path before ignore (try File.rm path)) end; |
41307
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
138 |
|
56498 | 139 |
|
140 |
(* tmp dirs *) |
|
141 |
||
73324 | 142 |
fun rm_tree path = scala_function "rm_tree" [path]; |
143 |
||
41307
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
144 |
fun with_tmp_dir name f = |
72376 | 145 |
let val path = create_tmp_path name "" |
146 |
in Exn.release (Exn.capture f (make_directory path) before ignore (try rm_tree path)) end; |
|
41307
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
147 |
|
72948 | 148 |
|
149 |
(* download file *) |
|
150 |
||
73566 | 151 |
val download = Scala.function1 "download"; |
152 |
||
153 |
fun download_file url path = File.write path (download url); |
|
72948 | 154 |
|
73523
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73434
diff
changeset
|
155 |
|
73576 | 156 |
(* base64 *) |
157 |
||
158 |
val decode_base64 = Scala.function1 "decode_base64"; |
|
159 |
val encode_base64 = Scala.function1 "encode_base64"; |
|
160 |
||
161 |
||
73523
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73434
diff
changeset
|
162 |
(* Isabelle distribution identification *) |
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73434
diff
changeset
|
163 |
|
73565 | 164 |
fun isabelle_id () = Scala.function1 "isabelle_id" ""; |
73523
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73434
diff
changeset
|
165 |
|
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73434
diff
changeset
|
166 |
fun isabelle_identifier () = try getenv_strict "ISABELLE_IDENTIFIER"; |
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73434
diff
changeset
|
167 |
|
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73434
diff
changeset
|
168 |
fun isabelle_heading () = |
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73434
diff
changeset
|
169 |
(case isabelle_identifier () of |
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73434
diff
changeset
|
170 |
NONE => "" |
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73434
diff
changeset
|
171 |
| SOME version => " (" ^ version ^ ")"); |
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73434
diff
changeset
|
172 |
|
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73434
diff
changeset
|
173 |
fun isabelle_name () = getenv_strict "ISABELLE_NAME"; |
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73434
diff
changeset
|
174 |
|
73547 | 175 |
fun identification () = "Isabelle/" ^ isabelle_id () ^ isabelle_heading (); |
176 |
||
40743 | 177 |
end; |