author | wenzelm |
Thu, 15 Feb 2024 12:48:25 +0100 | |
changeset 79620 | 3914bca631b9 |
parent 78787 | a7e4b412cc7c |
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 |
75578 | 23 |
val download: string -> Bytes.T |
73566 | 24 |
val download_file: string -> Path.T -> unit |
73523
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73434
diff
changeset
|
25 |
val isabelle_id: unit -> string |
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73434
diff
changeset
|
26 |
val isabelle_identifier: unit -> string option |
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73434
diff
changeset
|
27 |
val isabelle_heading: unit -> string |
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73434
diff
changeset
|
28 |
val isabelle_name: unit -> string |
73547 | 29 |
val identification: unit -> string |
40743 | 30 |
end; |
31 |
||
32 |
structure Isabelle_System: ISABELLE_SYSTEM = |
|
33 |
struct |
|
34 |
||
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43849
diff
changeset
|
35 |
(* bash *) |
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43849
diff
changeset
|
36 |
|
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
37 |
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
|
38 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
39 |
fun bash_process params = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
40 |
let |
74212 | 41 |
val {script, input, cwd, putenv, redirect, timeout, description} = |
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
42 |
Bash.dest_params params; |
78716 | 43 |
val server_run = |
74210 | 44 |
[Bash.server_run, script, input, |
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
45 |
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
|
46 |
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
|
47 |
(("ISABELLE_TMP", getenv "ISABELLE_TMP") :: putenv), |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
48 |
Value.print_bool redirect, |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
49 |
Value.print_real (Time.toReal timeout), |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
50 |
description]; |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
51 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
52 |
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
|
53 |
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
|
54 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
55 |
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
|
56 |
fun with_streams f = Socket_IO.with_streams' f address password; |
73264 | 57 |
|
74210 | 58 |
fun kill (SOME uuid) = |
75577
c51e1cef1eae
more scalable byte messages, notably for Scala functions in ML;
wenzelm
parents:
74336
diff
changeset
|
59 |
with_streams (fn s => Byte_Message.write_message_string (#2 s) [Bash.server_kill, uuid]) |
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
60 |
| kill NONE = (); |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
61 |
in |
78720 | 62 |
Thread_Attributes.uninterruptible_body (fn run => |
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
63 |
let |
74210 | 64 |
fun err () = raise Fail "Malformed result from bash_process server"; |
78725
3c02ad5a1586
clarified treatment of exceptions: avoid catch-all handlers;
wenzelm
parents:
78722
diff
changeset
|
65 |
fun loop_body s = |
78716 | 66 |
(case run Byte_Message.read_message_string (#1 s) of |
74210 | 67 |
SOME (head :: args) => |
68 |
if head = Bash.server_uuid andalso length args = 1 then |
|
69 |
loop (SOME (hd args)) s |
|
70 |
else if head = Bash.server_interrupt andalso null args then |
|
78787 | 71 |
Isabelle_Thread.raise_interrupt () |
74210 | 72 |
else if head = Bash.server_failure andalso length args = 1 then |
73 |
raise Fail (hd args) |
|
74 |
else if head = Bash.server_result andalso length args >= 4 then |
|
75 |
let |
|
76 |
val a :: b :: c :: d :: lines = args; |
|
77 |
val rc = Value.parse_int a; |
|
78 |
val (elapsed, cpu) = apply2 (Time.fromMilliseconds o Value.parse_int) (b, c); |
|
79 |
val (out_lines, err_lines) = chop (Value.parse_int d) lines; |
|
80 |
in |
|
81 |
if rc = Process_Result.timeout_rc then raise Timeout.TIMEOUT elapsed |
|
82 |
else |
|
83 |
Process_Result.make |
|
84 |
{rc = rc, |
|
85 |
out_lines = out_lines, |
|
86 |
err_lines = err_lines, |
|
87 |
timing = {elapsed = elapsed, cpu = cpu, gc = Time.zeroTime}} |
|
88 |
end |
|
89 |
else err () |
|
90 |
| _ => err ()) |
|
78725
3c02ad5a1586
clarified treatment of exceptions: avoid catch-all handlers;
wenzelm
parents:
78722
diff
changeset
|
91 |
and loop maybe_uuid s = |
78757 | 92 |
(case Exn.capture_body (fn () => loop_body s) of |
78725
3c02ad5a1586
clarified treatment of exceptions: avoid catch-all handlers;
wenzelm
parents:
78722
diff
changeset
|
93 |
Exn.Res res => res |
3c02ad5a1586
clarified treatment of exceptions: avoid catch-all handlers;
wenzelm
parents:
78722
diff
changeset
|
94 |
| Exn.Exn exn => (kill maybe_uuid; Exn.reraise exn)); |
78716 | 95 |
in |
96 |
with_streams (fn s => (Byte_Message.write_message_string (#2 s) server_run; loop NONE s)) |
|
78720 | 97 |
end) |
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
98 |
end; |
73604 | 99 |
|
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
100 |
val bash = Bash.script #> bash_process #> Process_Result.print #> Process_Result.rc; |
73281 | 101 |
|
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43849
diff
changeset
|
102 |
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
|
103 |
let |
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
104 |
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
|
105 |
val _ = warning (Process_Result.err res); |
73275 | 106 |
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
|
107 |
|
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43849
diff
changeset
|
108 |
|
71902
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
109 |
(* bash functions *) |
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
110 |
|
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
111 |
fun bash_functions () = |
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
112 |
bash_process (Bash.script "declare -Fx") |
73279 | 113 |
|> Process_Result.check |
114 |
|> Process_Result.out_lines |
|
115 |
|> map_filter (space_explode " " #> try List.last); |
|
71902
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
116 |
|
71911 | 117 |
fun check_bash_function ctxt arg = |
71912 | 118 |
Completion.check_entity Markup.bash_functionN |
119 |
(bash_functions () |> map (rpair Position.none)) ctxt arg; |
|
71902
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
120 |
|
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
121 |
|
73322 | 122 |
(* directory and file operations *) |
123 |
||
73567 | 124 |
fun scala_function name = ignore o Scala.function name o map absolute_path; |
40743 | 125 |
|
73322 | 126 |
fun make_directory path = (scala_function "make_directory" [path]; path); |
40743 | 127 |
|
73322 | 128 |
fun copy_dir src dst = scala_function "copy_dir" [src, dst]; |
40743 | 129 |
|
73322 | 130 |
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
|
131 |
|
73322 | 132 |
fun copy_file_base (base_dir, src) target_dir = |
73567 | 133 |
ignore (Scala.function "copy_file_base" |
134 |
[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
|
135 |
|
41307
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
136 |
|
56498 | 137 |
(* tmp files *) |
41307
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
138 |
|
42127
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
41944
diff
changeset
|
139 |
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
|
140 |
let |
42127
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
41944
diff
changeset
|
141 |
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
|
142 |
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
|
143 |
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
|
144 |
in path end; |
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
145 |
|
78722
3636dc23aa0e
more robust management of resources, using Thread_Attributes.uninterruptible;
wenzelm
parents:
78721
diff
changeset
|
146 |
fun with_tmp_file name ext = Thread_Attributes.uninterruptible (fn run => fn f => |
3636dc23aa0e
more robust management of resources, using Thread_Attributes.uninterruptible;
wenzelm
parents:
78721
diff
changeset
|
147 |
let |
3636dc23aa0e
more robust management of resources, using Thread_Attributes.uninterruptible;
wenzelm
parents:
78721
diff
changeset
|
148 |
val path = create_tmp_path name ext; |
3636dc23aa0e
more robust management of resources, using Thread_Attributes.uninterruptible;
wenzelm
parents:
78721
diff
changeset
|
149 |
val result = Exn.capture (run f) path; |
3636dc23aa0e
more robust management of resources, using Thread_Attributes.uninterruptible;
wenzelm
parents:
78721
diff
changeset
|
150 |
val _ = try File.rm path; |
3636dc23aa0e
more robust management of resources, using Thread_Attributes.uninterruptible;
wenzelm
parents:
78721
diff
changeset
|
151 |
in Exn.release result end); |
41307
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
152 |
|
56498 | 153 |
|
154 |
(* tmp dirs *) |
|
155 |
||
73324 | 156 |
fun rm_tree path = scala_function "rm_tree" [path]; |
157 |
||
78721 | 158 |
fun with_tmp_dir name = Thread_Attributes.uninterruptible (fn run => fn f => |
78719
89038d9ef77d
more robust management of resources, using Thread_Attributes.uninterruptible;
wenzelm
parents:
78716
diff
changeset
|
159 |
let |
89038d9ef77d
more robust management of resources, using Thread_Attributes.uninterruptible;
wenzelm
parents:
78716
diff
changeset
|
160 |
val path = create_tmp_path name ""; |
89038d9ef77d
more robust management of resources, using Thread_Attributes.uninterruptible;
wenzelm
parents:
78716
diff
changeset
|
161 |
val _ = make_directory path; |
89038d9ef77d
more robust management of resources, using Thread_Attributes.uninterruptible;
wenzelm
parents:
78716
diff
changeset
|
162 |
val result = Exn.capture (run f) path; |
89038d9ef77d
more robust management of resources, using Thread_Attributes.uninterruptible;
wenzelm
parents:
78716
diff
changeset
|
163 |
val _ = try rm_tree path; |
78720 | 164 |
in Exn.release result end); |
41307
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
165 |
|
72948 | 166 |
|
167 |
(* download file *) |
|
168 |
||
75578 | 169 |
val download = Bytes.string #> Scala.function1_bytes "download"; |
73566 | 170 |
|
75578 | 171 |
fun download_file url path = Bytes.write path (download url); |
72948 | 172 |
|
73523
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73434
diff
changeset
|
173 |
|
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73434
diff
changeset
|
174 |
(* Isabelle distribution identification *) |
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73434
diff
changeset
|
175 |
|
73565 | 176 |
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
|
177 |
|
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73434
diff
changeset
|
178 |
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
|
179 |
|
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73434
diff
changeset
|
180 |
fun isabelle_heading () = |
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73434
diff
changeset
|
181 |
(case isabelle_identifier () of |
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73434
diff
changeset
|
182 |
NONE => "" |
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73434
diff
changeset
|
183 |
| SOME version => " (" ^ version ^ ")"); |
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73434
diff
changeset
|
184 |
|
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73434
diff
changeset
|
185 |
fun isabelle_name () = getenv_strict "ISABELLE_NAME"; |
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73434
diff
changeset
|
186 |
|
74336
7bb0ac635397
permissive identification, e.g. relevant for HOL-SPARK examples running on rsync-clone;
wenzelm
parents:
74212
diff
changeset
|
187 |
fun identification () = |
7bb0ac635397
permissive identification, e.g. relevant for HOL-SPARK examples running on rsync-clone;
wenzelm
parents:
74212
diff
changeset
|
188 |
"Isabelle" ^ (case try isabelle_id () of SOME id => "/" ^ id | NONE => "") ^ isabelle_heading (); |
73547 | 189 |
|
40743 | 190 |
end; |