src/Pure/System/isabelle_system.ML
author wenzelm
Mon, 01 Mar 2021 15:09:57 +0100
changeset 73331 d045cdbdf243
parent 73330 0fb889c361e6
child 73333 b70d82358c6d
permissions -rw-r--r--
proper relative path (see also df49ca5da9d0, 5b15eee1a661, etc.);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/System/isabelle_system.ML
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
     3
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
     4
Isabelle system support.
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
     5
*)
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
     6
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
     7
signature ISABELLE_SYSTEM =
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
     8
sig
73275
f0db1e4c89bc clarified signature, following Isabelle/Scala;
wenzelm
parents: 73273
diff changeset
     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
72376
04bce3478688 clarified signature;
wenzelm
parents: 72375
diff changeset
    14
  val make_directory: Path.T -> Path.T
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    15
  val copy_dir: Path.T -> Path.T -> unit
56533
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 56498
diff changeset
    16
  val copy_file: Path.T -> Path.T -> unit
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 56498
diff changeset
    17
  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
    18
  val create_tmp_path: string -> string -> Path.T
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 41944
diff changeset
    19
  val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a
73324
48abb09d49ea more Isabelle/ML/Scala operations;
wenzelm
parents: 73323
diff changeset
    20
  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
    21
  val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
72948
f3d0e4ea492d download as in Isabelle/Scala;
wenzelm
parents: 72511
diff changeset
    22
  val download: string -> string
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    23
end;
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    24
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    25
structure Isabelle_System: ISABELLE_SYSTEM =
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    26
struct
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    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
f0db1e4c89bc clarified signature, following Isabelle/Scala;
wenzelm
parents: 73273
diff changeset
    30
fun bash_process script =
73264
440546ea20e6 clarified modules;
wenzelm
parents: 72951
diff changeset
    31
  Scala.function_thread "bash_process"
440546ea20e6 clarified modules;
wenzelm
parents: 72951
diff changeset
    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
440546ea20e6 clarified modules;
wenzelm
parents: 72951
diff changeset
    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
f0db1e4c89bc clarified signature, following Isabelle/Scala;
wenzelm
parents: 73273
diff changeset
    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
f0db1e4c89bc clarified signature, following Isabelle/Scala;
wenzelm
parents: 73273
diff changeset
    42
            Process_Result.make
f0db1e4c89bc clarified signature, following Isabelle/Scala;
wenzelm
parents: 73273
diff changeset
    43
             {rc = rc,
f0db1e4c89bc clarified signature, following Isabelle/Scala;
wenzelm
parents: 73273
diff changeset
    44
              out_lines = out_lines,
f0db1e4c89bc clarified signature, following Isabelle/Scala;
wenzelm
parents: 73273
diff changeset
    45
              err_lines = err_lines,
f0db1e4c89bc clarified signature, following Isabelle/Scala;
wenzelm
parents: 73273
diff changeset
    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
440546ea20e6 clarified modules;
wenzelm
parents: 72951
diff changeset
    49
73281
22417b631453 clarified signature, following Isabelle/Scala;
wenzelm
parents: 73279
diff changeset
    50
val bash = bash_process #> Process_Result.print #> Process_Result.rc;
22417b631453 clarified signature, following Isabelle/Scala;
wenzelm
parents: 73279
diff changeset
    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
f0db1e4c89bc clarified signature, following Isabelle/Scala;
wenzelm
parents: 73273
diff changeset
    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
f0db1e4c89bc clarified signature, following Isabelle/Scala;
wenzelm
parents: 73273
diff changeset
    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
37aff2142295 clarified signature;
wenzelm
parents: 73277
diff changeset
    62
  bash_process "declare -Fx"
37aff2142295 clarified signature;
wenzelm
parents: 73277
diff changeset
    63
  |> Process_Result.check
37aff2142295 clarified signature;
wenzelm
parents: 73277
diff changeset
    64
  |> Process_Result.out_lines
37aff2142295 clarified signature;
wenzelm
parents: 73277
diff changeset
    65
  |> map_filter (space_explode " " #> try List.last);
71902
1529336eaedc check bash functions against Isabelle settings environment;
wenzelm
parents: 70050
diff changeset
    66
71911
d25093536482 clarified signature;
wenzelm
parents: 71902
diff changeset
    67
fun check_bash_function ctxt arg =
71912
b9fbc93f3a24 clarified markup;
wenzelm
parents: 71911
diff changeset
    68
  Completion.check_entity Markup.bash_functionN
b9fbc93f3a24 clarified markup;
wenzelm
parents: 71911
diff changeset
    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
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73316
diff changeset
    72
(* directory and file operations *)
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73316
diff changeset
    73
73330
0fb889c361e6 tuned signature;
wenzelm
parents: 73324
diff changeset
    74
val absolute_path = Path.implode o File.absolute_path;
0fb889c361e6 tuned signature;
wenzelm
parents: 73324
diff changeset
    75
fun scala_function0 name = ignore o Scala.function name o space_implode "\000";
0fb889c361e6 tuned signature;
wenzelm
parents: 73324
diff changeset
    76
fun scala_function name = scala_function0 name o map absolute_path;
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    77
73322
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73316
diff changeset
    78
fun make_directory path = (scala_function "make_directory" [path]; path);
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    79
73322
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73316
diff changeset
    80
fun copy_dir src dst = scala_function "copy_dir" [src, dst];
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    81
73322
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73316
diff changeset
    82
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
    83
73322
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73316
diff changeset
    84
fun copy_file_base (base_dir, src) target_dir =
73331
d045cdbdf243 proper relative path (see also df49ca5da9d0, 5b15eee1a661, etc.);
wenzelm
parents: 73330
diff changeset
    85
  scala_function0 "copy_file_base"
d045cdbdf243 proper relative path (see also df49ca5da9d0, 5b15eee1a661, etc.);
wenzelm
parents: 73330
diff changeset
    86
    [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
    87
41307
bb8468ae414e slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents: 40785
diff changeset
    88
56498
6437c989a744 tuned comments (see Scala version);
wenzelm
parents: 50843
diff changeset
    89
(* tmp files *)
41307
bb8468ae414e slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents: 40785
diff changeset
    90
42127
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 41944
diff changeset
    91
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
    92
  let
42127
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 41944
diff changeset
    93
    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
    94
    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
    95
      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
    96
  in path end;
bb8468ae414e slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents: 40785
diff changeset
    97
42127
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 41944
diff changeset
    98
fun with_tmp_file name ext f =
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 41944
diff changeset
    99
  let val path = create_tmp_path name ext
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 41944
diff changeset
   100
  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
   101
56498
6437c989a744 tuned comments (see Scala version);
wenzelm
parents: 50843
diff changeset
   102
6437c989a744 tuned comments (see Scala version);
wenzelm
parents: 50843
diff changeset
   103
(* tmp dirs *)
6437c989a744 tuned comments (see Scala version);
wenzelm
parents: 50843
diff changeset
   104
73324
48abb09d49ea more Isabelle/ML/Scala operations;
wenzelm
parents: 73323
diff changeset
   105
fun rm_tree path = scala_function "rm_tree" [path];
48abb09d49ea more Isabelle/ML/Scala operations;
wenzelm
parents: 73323
diff changeset
   106
41307
bb8468ae414e slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents: 40785
diff changeset
   107
fun with_tmp_dir name f =
72376
04bce3478688 clarified signature;
wenzelm
parents: 72375
diff changeset
   108
  let val path = create_tmp_path name ""
04bce3478688 clarified signature;
wenzelm
parents: 72375
diff changeset
   109
  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
   110
72948
f3d0e4ea492d download as in Isabelle/Scala;
wenzelm
parents: 72511
diff changeset
   111
f3d0e4ea492d download as in Isabelle/Scala;
wenzelm
parents: 72511
diff changeset
   112
(* download file *)
f3d0e4ea492d download as in Isabelle/Scala;
wenzelm
parents: 72511
diff changeset
   113
f3d0e4ea492d download as in Isabelle/Scala;
wenzelm
parents: 72511
diff changeset
   114
fun download url =
f3d0e4ea492d download as in Isabelle/Scala;
wenzelm
parents: 72511
diff changeset
   115
  with_tmp_file "download" "" (fn path =>
73330
0fb889c361e6 tuned signature;
wenzelm
parents: 73324
diff changeset
   116
   (scala_function0 "download" [url, absolute_path path];
73323
c2ab1a970e82 more Isabelle/ML/Scala operations;
wenzelm
parents: 73322
diff changeset
   117
    File.read path));
72948
f3d0e4ea492d download as in Isabelle/Scala;
wenzelm
parents: 72511
diff changeset
   118
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
   119
end;