author | wenzelm |
Sat, 27 Feb 2021 21:01:07 +0100 | |
changeset 73322 | 5b15eee1a661 |
parent 73316 | 8664433956b3 |
child 73323 | c2ab1a970e82 |
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: 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 |
66679 | 14 |
val rm_tree: Path.T -> unit |
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 |
41307
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
21 |
val with_tmp_dir: string -> (Path.T -> 'a) -> 'a |
72948 | 22 |
val download: string -> string |
40743 | 23 |
end; |
24 |
||
25 |
structure Isabelle_System: ISABELLE_SYSTEM = |
|
26 |
struct |
|
27 |
||
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43849
diff
changeset
|
28 |
(* bash *) |
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43849
diff
changeset
|
29 |
|
73275 | 30 |
fun bash_process script = |
73264 | 31 |
Scala.function_thread "bash_process" |
32 |
("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
|
33 |
|> space_explode "\000" |
c8abfe393c16
more accurate process_result in ML, corresponding to Process_Result in Scala;
wenzelm
parents:
73264
diff
changeset
|
34 |
|> (fn [] => raise Exn.Interrupt |
c8abfe393c16
more accurate process_result in ML, corresponding to Process_Result in Scala;
wenzelm
parents:
73264
diff
changeset
|
35 |
| [err] => error err |
73273
17c28251fff0
clarified signature: process_result timing from Isabelle/Scala;
wenzelm
parents:
73268
diff
changeset
|
36 |
| a :: b :: c :: d :: lines => |
73264 | 37 |
let |
73268
c8abfe393c16
more accurate process_result in ML, corresponding to Process_Result in Scala;
wenzelm
parents:
73264
diff
changeset
|
38 |
val rc = Value.parse_int a; |
73273
17c28251fff0
clarified signature: process_result timing from Isabelle/Scala;
wenzelm
parents:
73268
diff
changeset
|
39 |
val (elapsed, cpu) = apply2 (Time.fromMilliseconds o Value.parse_int) (b, c); |
73275 | 40 |
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
|
41 |
in |
73275 | 42 |
Process_Result.make |
43 |
{rc = rc, |
|
44 |
out_lines = out_lines, |
|
45 |
err_lines = err_lines, |
|
46 |
timing = {elapsed = elapsed, cpu = cpu, gc = Time.zeroTime}} |
|
73273
17c28251fff0
clarified signature: process_result timing from Isabelle/Scala;
wenzelm
parents:
73268
diff
changeset
|
47 |
end |
17c28251fff0
clarified signature: process_result timing from Isabelle/Scala;
wenzelm
parents:
73268
diff
changeset
|
48 |
| _ => raise Fail "Malformed Isabelle/Scala result"); |
73264 | 49 |
|
73281 | 50 |
val bash = bash_process #> Process_Result.print #> Process_Result.rc; |
51 |
||
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43849
diff
changeset
|
52 |
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
|
53 |
let |
73275 | 54 |
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
|
55 |
val _ = warning (Process_Result.err res); |
73275 | 56 |
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
|
57 |
|
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43849
diff
changeset
|
58 |
|
71902
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
59 |
(* bash functions *) |
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
60 |
|
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
61 |
fun bash_functions () = |
73279 | 62 |
bash_process "declare -Fx" |
63 |
|> Process_Result.check |
|
64 |
|> Process_Result.out_lines |
|
65 |
|> map_filter (space_explode " " #> try List.last); |
|
71902
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
66 |
|
71911 | 67 |
fun check_bash_function ctxt arg = |
71912 | 68 |
Completion.check_entity Markup.bash_functionN |
69 |
(bash_functions () |> map (rpair Position.none)) ctxt arg; |
|
71902
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
70 |
|
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
71 |
|
73322 | 72 |
(* directory and file operations *) |
73 |
||
74 |
fun scala_function name args = |
|
75 |
ignore (Scala.function name (space_implode "\000" (map (Path.implode o File.absolute_path) args))); |
|
40743 | 76 |
|
77 |
fun system_command cmd = |
|
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
62549
diff
changeset
|
78 |
if bash cmd <> 0 then error ("System command failed: " ^ cmd) else (); |
40743 | 79 |
|
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
62549
diff
changeset
|
80 |
fun rm_tree path = system_command ("rm -r -f " ^ File.bash_path path); |
40743 | 81 |
|
73322 | 82 |
fun make_directory path = (scala_function "make_directory" [path]; path); |
40743 | 83 |
|
73322 | 84 |
fun copy_dir src dst = scala_function "copy_dir" [src, dst]; |
40743 | 85 |
|
73322 | 86 |
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
|
87 |
|
73322 | 88 |
fun copy_file_base (base_dir, src) target_dir = |
89 |
scala_function "copy_file_base" [base_dir, src, target_dir]; |
|
56533
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
90 |
|
41307
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
91 |
|
56498 | 92 |
(* tmp files *) |
41307
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
93 |
|
42127
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
41944
diff
changeset
|
94 |
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
|
95 |
let |
42127
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
41944
diff
changeset
|
96 |
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
|
97 |
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
|
98 |
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
|
99 |
in path end; |
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
100 |
|
42127
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
41944
diff
changeset
|
101 |
fun with_tmp_file name ext f = |
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
41944
diff
changeset
|
102 |
let val path = create_tmp_path name ext |
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
41944
diff
changeset
|
103 |
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
|
104 |
|
56498 | 105 |
|
106 |
(* tmp dirs *) |
|
107 |
||
41307
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
108 |
fun with_tmp_dir name f = |
72376 | 109 |
let val path = create_tmp_path name "" |
110 |
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
|
111 |
|
72948 | 112 |
|
113 |
(* download file *) |
|
114 |
||
115 |
fun download url = |
|
116 |
with_tmp_file "download" "" (fn path => |
|
73275 | 117 |
let |
118 |
val s = "curl --fail --silent --location " ^ Bash.string url ^ " > " ^ File.bash_path path; |
|
119 |
val res = bash_process s; |
|
120 |
in |
|
121 |
if Process_Result.ok res then File.read path |
|
122 |
else cat_error ("Failed to download " ^ quote url) (Process_Result.err res) |
|
123 |
end); |
|
72948 | 124 |
|
40743 | 125 |
end; |