author | wenzelm |
Mon, 22 Feb 2021 15:24:04 +0100 | |
changeset 73277 | 0110e2e2964c |
parent 73275 | f0db1e4c89bc |
child 73279 | 37aff2142295 |
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 |
|
73275 | 9 |
val bash_process: string -> Process_Result.T |
71902
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
10 |
val bash_output_check: string -> string |
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
11 |
val bash_output: string -> string * int |
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
12 |
val bash: string -> int |
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
13 |
val bash_functions: unit -> string list |
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
14 |
val check_bash_function: Proof.context -> string * Position.T -> string |
66679 | 15 |
val rm_tree: Path.T -> unit |
72376 | 16 |
val make_directory: Path.T -> Path.T |
40745 | 17 |
val mkdir: Path.T -> unit |
40743 | 18 |
val copy_dir: Path.T -> Path.T -> unit |
56533
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
19 |
val copy_file: Path.T -> Path.T -> unit |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
20 |
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
|
21 |
val create_tmp_path: string -> string -> Path.T |
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
41944
diff
changeset
|
22 |
val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a |
41307
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
23 |
val with_tmp_dir: string -> (Path.T -> 'a) -> 'a |
72948 | 24 |
val download: string -> string |
40743 | 25 |
end; |
26 |
||
27 |
structure Isabelle_System: ISABELLE_SYSTEM = |
|
28 |
struct |
|
29 |
||
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43849
diff
changeset
|
30 |
(* bash *) |
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43849
diff
changeset
|
31 |
|
73275 | 32 |
fun bash_process script = |
73264 | 33 |
Scala.function_thread "bash_process" |
34 |
("export ISABELLE_TMP=" ^ Bash.string (getenv "ISABELLE_TMP") ^ "\n" ^ script) |
|
73268
c8abfe393c16
more accurate process_result in ML, corresponding to Process_Result in Scala;
wenzelm
parents:
73264
diff
changeset
|
35 |
|> space_explode "\000" |
c8abfe393c16
more accurate process_result in ML, corresponding to Process_Result in Scala;
wenzelm
parents:
73264
diff
changeset
|
36 |
|> (fn [] => raise Exn.Interrupt |
c8abfe393c16
more accurate process_result in ML, corresponding to Process_Result in Scala;
wenzelm
parents:
73264
diff
changeset
|
37 |
| [err] => error err |
73273
17c28251fff0
clarified signature: process_result timing from Isabelle/Scala;
wenzelm
parents:
73268
diff
changeset
|
38 |
| a :: b :: c :: d :: lines => |
73264 | 39 |
let |
73268
c8abfe393c16
more accurate process_result in ML, corresponding to Process_Result in Scala;
wenzelm
parents:
73264
diff
changeset
|
40 |
val rc = Value.parse_int a; |
73273
17c28251fff0
clarified signature: process_result timing from Isabelle/Scala;
wenzelm
parents:
73268
diff
changeset
|
41 |
val (elapsed, cpu) = apply2 (Time.fromMilliseconds o Value.parse_int) (b, c); |
73275 | 42 |
val (out_lines, err_lines) = chop (Value.parse_int d) lines; |
73273
17c28251fff0
clarified signature: process_result timing from Isabelle/Scala;
wenzelm
parents:
73268
diff
changeset
|
43 |
in |
73275 | 44 |
Process_Result.make |
45 |
{rc = rc, |
|
46 |
out_lines = out_lines, |
|
47 |
err_lines = err_lines, |
|
48 |
timing = {elapsed = elapsed, cpu = cpu, gc = Time.zeroTime}} |
|
73273
17c28251fff0
clarified signature: process_result timing from Isabelle/Scala;
wenzelm
parents:
73268
diff
changeset
|
49 |
end |
17c28251fff0
clarified signature: process_result timing from Isabelle/Scala;
wenzelm
parents:
73268
diff
changeset
|
50 |
| _ => raise Fail "Malformed Isabelle/Scala result"); |
73264 | 51 |
|
70050 | 52 |
fun bash_output_check s = |
73275 | 53 |
let val res = bash_process s in |
73277
0110e2e2964c
clarified signature: always trim_line of Process_Result.out/err, uniformly in ML and Scala;
wenzelm
parents:
73275
diff
changeset
|
54 |
if Process_Result.ok res then Process_Result.out res |
0110e2e2964c
clarified signature: always trim_line of Process_Result.out/err, uniformly in ML and Scala;
wenzelm
parents:
73275
diff
changeset
|
55 |
else error (Process_Result.err res) |
73275 | 56 |
end; |
70050 | 57 |
|
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43849
diff
changeset
|
58 |
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
|
59 |
let |
73275 | 60 |
val res = bash_process s; |
73277
0110e2e2964c
clarified signature: always trim_line of Process_Result.out/err, uniformly in ML and Scala;
wenzelm
parents:
73275
diff
changeset
|
61 |
val _ = warning (Process_Result.err res); |
73275 | 62 |
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
|
63 |
|
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43849
diff
changeset
|
64 |
fun bash 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
|
65 |
let |
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
|
66 |
val (out, rc) = bash_output s; |
73277
0110e2e2964c
clarified signature: always trim_line of Process_Result.out/err, uniformly in ML and Scala;
wenzelm
parents:
73275
diff
changeset
|
67 |
val _ = writeln out; |
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
|
68 |
in rc end; |
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43849
diff
changeset
|
69 |
|
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43849
diff
changeset
|
70 |
|
71902
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
71 |
(* bash functions *) |
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
72 |
|
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
73 |
fun bash_functions () = |
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
74 |
bash_output_check "declare -Fx" |
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
75 |
|> split_lines |> map_filter (space_explode " " #> try List.last); |
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
76 |
|
71911 | 77 |
fun check_bash_function ctxt arg = |
71912 | 78 |
Completion.check_entity Markup.bash_functionN |
79 |
(bash_functions () |> map (rpair Position.none)) ctxt arg; |
|
71902
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
80 |
|
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
81 |
|
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
62549
diff
changeset
|
82 |
(* directory operations *) |
40743 | 83 |
|
84 |
fun system_command cmd = |
|
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
62549
diff
changeset
|
85 |
if bash cmd <> 0 then error ("System command failed: " ^ cmd) else (); |
40743 | 86 |
|
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
62549
diff
changeset
|
87 |
fun rm_tree path = system_command ("rm -r -f " ^ File.bash_path path); |
40743 | 88 |
|
72375 | 89 |
fun make_directory path = |
72376 | 90 |
let |
91 |
val _ = |
|
92 |
if File.is_dir path then () |
|
93 |
else |
|
94 |
(bash ("perl -e \"use File::Path make_path; make_path('" ^ File.standard_path path ^ "');\""); |
|
95 |
if File.is_dir path then () else error ("Failed to create directory: " ^ Path.print path)); |
|
96 |
in path end; |
|
40743 | 97 |
|
40785 | 98 |
fun mkdir path = |
99 |
if File.is_dir path then () else OS.FileSys.mkDir (File.platform_path path); |
|
40743 | 100 |
|
101 |
fun copy_dir src dst = |
|
102 |
if File.eq (src, dst) then () |
|
62549
9498623b27f0
File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
60970
diff
changeset
|
103 |
else (system_command ("cp -p -R -f " ^ File.bash_path src ^ "/. " ^ File.bash_path dst); ()); |
40743 | 104 |
|
56533
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
105 |
fun copy_file src0 dst0 = |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
106 |
let |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
107 |
val src = Path.expand src0; |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
108 |
val dst = Path.expand dst0; |
72511
460d743010bc
clarified signature: overloaded "+" for Path.append;
wenzelm
parents:
72376
diff
changeset
|
109 |
val target = if File.is_dir dst then dst + Path.base src else dst; |
56533
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
110 |
in |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
111 |
if File.eq (src, target) then () |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
112 |
else |
62549
9498623b27f0
File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
60970
diff
changeset
|
113 |
ignore (system_command ("cp -p -f " ^ File.bash_path src ^ " " ^ File.bash_path target)) |
56533
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
114 |
end; |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
115 |
|
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
116 |
fun copy_file_base (base_dir, src0) target_dir = |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
117 |
let |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
118 |
val src = Path.expand src0; |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
119 |
val src_dir = Path.dir src; |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
120 |
val _ = |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
121 |
if Path.starts_basic src then () |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
122 |
else error ("Illegal path specification " ^ Path.print src ^ " beyond base directory"); |
72511
460d743010bc
clarified signature: overloaded "+" for Path.append;
wenzelm
parents:
72376
diff
changeset
|
123 |
in copy_file (base_dir + src) (make_directory (target_dir + src_dir)) end; |
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 |
||
41307
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
142 |
fun with_tmp_dir name f = |
72376 | 143 |
let val path = create_tmp_path name "" |
144 |
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
|
145 |
|
72948 | 146 |
|
147 |
(* download file *) |
|
148 |
||
149 |
fun download url = |
|
150 |
with_tmp_file "download" "" (fn path => |
|
73275 | 151 |
let |
152 |
val s = "curl --fail --silent --location " ^ Bash.string url ^ " > " ^ File.bash_path path; |
|
153 |
val res = bash_process s; |
|
154 |
in |
|
155 |
if Process_Result.ok res then File.read path |
|
156 |
else cat_error ("Failed to download " ^ quote url) (Process_Result.err res) |
|
157 |
end); |
|
72948 | 158 |
|
40743 | 159 |
end; |