src/Pure/System/isabelle_system.ML
author wenzelm
Mon, 12 Apr 2021 18:10:13 +0200
changeset 73565 1aa92bc4d356
parent 73547 a7aabdf889b7
child 73566 4e6b31ed7197
permissions -rw-r--r--
clarified signature for Scala functions;
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
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
04bce3478688 clarified signature;
wenzelm
parents: 72375
diff changeset
    15
  val make_directory: Path.T -> Path.T
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    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
48abb09d49ea more Isabelle/ML/Scala operations;
wenzelm
parents: 73323
diff changeset
    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
73336
ff7ce802be52 clarified signature, according to Isabelle/Scala;
wenzelm
parents: 73334
diff changeset
    23
  val download: string -> Path.T -> unit
73523
2cd23d587db9 further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents: 73434
diff changeset
    24
  val isabelle_id: unit -> string
2cd23d587db9 further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents: 73434
diff changeset
    25
  val isabelle_identifier: unit -> string option
2cd23d587db9 further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents: 73434
diff changeset
    26
  val isabelle_heading: unit -> string
2cd23d587db9 further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents: 73434
diff changeset
    27
  val isabelle_name: unit -> string
73547
a7aabdf889b7 clarified signature;
wenzelm
parents: 73523
diff changeset
    28
  val identification: unit -> string
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    29
end;
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    30
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    31
structure Isabelle_System: ISABELLE_SYSTEM =
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    32
struct
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    33
43850
7f2cbc713344 moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents: 43849
diff changeset
    34
(* bash *)
7f2cbc713344 moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents: 43849
diff changeset
    35
73275
f0db1e4c89bc clarified signature, following Isabelle/Scala;
wenzelm
parents: 73273
diff changeset
    36
fun bash_process script =
73419
22f3f2117ed7 clarified signature: function_thread is determined in Isabelle/Scala, not Isabelle/ML;
wenzelm
parents: 73336
diff changeset
    37
  Scala.function "bash_process"
73565
1aa92bc4d356 clarified signature for Scala functions;
wenzelm
parents: 73547
diff changeset
    38
    ["export ISABELLE_TMP=" ^ Bash.string (getenv "ISABELLE_TMP"), script]
73268
c8abfe393c16 more accurate process_result in ML, corresponding to Process_Result in Scala;
wenzelm
parents: 73264
diff changeset
    39
  |> (fn [] => raise Exn.Interrupt
c8abfe393c16 more accurate process_result in ML, corresponding to Process_Result in Scala;
wenzelm
parents: 73264
diff changeset
    40
      | [err] => error err
73273
17c28251fff0 clarified signature: process_result timing from Isabelle/Scala;
wenzelm
parents: 73268
diff changeset
    41
      | a :: b :: c :: d :: lines =>
73264
440546ea20e6 clarified modules;
wenzelm
parents: 72951
diff changeset
    42
          let
73268
c8abfe393c16 more accurate process_result in ML, corresponding to Process_Result in Scala;
wenzelm
parents: 73264
diff changeset
    43
            val rc = Value.parse_int a;
73273
17c28251fff0 clarified signature: process_result timing from Isabelle/Scala;
wenzelm
parents: 73268
diff changeset
    44
            val (elapsed, cpu) = apply2 (Time.fromMilliseconds o Value.parse_int) (b, c);
73275
f0db1e4c89bc clarified signature, following Isabelle/Scala;
wenzelm
parents: 73273
diff changeset
    45
            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
    46
          in
73275
f0db1e4c89bc clarified signature, following Isabelle/Scala;
wenzelm
parents: 73273
diff changeset
    47
            Process_Result.make
f0db1e4c89bc clarified signature, following Isabelle/Scala;
wenzelm
parents: 73273
diff changeset
    48
             {rc = rc,
f0db1e4c89bc clarified signature, following Isabelle/Scala;
wenzelm
parents: 73273
diff changeset
    49
              out_lines = out_lines,
f0db1e4c89bc clarified signature, following Isabelle/Scala;
wenzelm
parents: 73273
diff changeset
    50
              err_lines = err_lines,
f0db1e4c89bc clarified signature, following Isabelle/Scala;
wenzelm
parents: 73273
diff changeset
    51
              timing = {elapsed = elapsed, cpu = cpu, gc = Time.zeroTime}}
73273
17c28251fff0 clarified signature: process_result timing from Isabelle/Scala;
wenzelm
parents: 73268
diff changeset
    52
         end
17c28251fff0 clarified signature: process_result timing from Isabelle/Scala;
wenzelm
parents: 73268
diff changeset
    53
      | _ => raise Fail "Malformed Isabelle/Scala result");
73264
440546ea20e6 clarified modules;
wenzelm
parents: 72951
diff changeset
    54
73281
22417b631453 clarified signature, following Isabelle/Scala;
wenzelm
parents: 73279
diff changeset
    55
val bash = bash_process #> Process_Result.print #> Process_Result.rc;
22417b631453 clarified signature, following Isabelle/Scala;
wenzelm
parents: 73279
diff changeset
    56
43850
7f2cbc713344 moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents: 43849
diff changeset
    57
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
    58
  let
73275
f0db1e4c89bc clarified signature, following Isabelle/Scala;
wenzelm
parents: 73273
diff changeset
    59
    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
    60
    val _ = warning (Process_Result.err res);
73275
f0db1e4c89bc clarified signature, following Isabelle/Scala;
wenzelm
parents: 73273
diff changeset
    61
  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
    62
7f2cbc713344 moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents: 43849
diff changeset
    63
71902
1529336eaedc check bash functions against Isabelle settings environment;
wenzelm
parents: 70050
diff changeset
    64
(* bash functions *)
1529336eaedc check bash functions against Isabelle settings environment;
wenzelm
parents: 70050
diff changeset
    65
1529336eaedc check bash functions against Isabelle settings environment;
wenzelm
parents: 70050
diff changeset
    66
fun bash_functions () =
73279
37aff2142295 clarified signature;
wenzelm
parents: 73277
diff changeset
    67
  bash_process "declare -Fx"
37aff2142295 clarified signature;
wenzelm
parents: 73277
diff changeset
    68
  |> Process_Result.check
37aff2142295 clarified signature;
wenzelm
parents: 73277
diff changeset
    69
  |> Process_Result.out_lines
37aff2142295 clarified signature;
wenzelm
parents: 73277
diff changeset
    70
  |> map_filter (space_explode " " #> try List.last);
71902
1529336eaedc check bash functions against Isabelle settings environment;
wenzelm
parents: 70050
diff changeset
    71
71911
d25093536482 clarified signature;
wenzelm
parents: 71902
diff changeset
    72
fun check_bash_function ctxt arg =
71912
b9fbc93f3a24 clarified markup;
wenzelm
parents: 71911
diff changeset
    73
  Completion.check_entity Markup.bash_functionN
b9fbc93f3a24 clarified markup;
wenzelm
parents: 71911
diff changeset
    74
    (bash_functions () |> map (rpair Position.none)) ctxt arg;
71902
1529336eaedc check bash functions against Isabelle settings environment;
wenzelm
parents: 70050
diff changeset
    75
1529336eaedc check bash functions against Isabelle settings environment;
wenzelm
parents: 70050
diff changeset
    76
73322
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73316
diff changeset
    77
(* directory and file operations *)
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73316
diff changeset
    78
73330
0fb889c361e6 tuned signature;
wenzelm
parents: 73324
diff changeset
    79
val absolute_path = Path.implode o File.absolute_path;
73565
1aa92bc4d356 clarified signature for Scala functions;
wenzelm
parents: 73547
diff changeset
    80
fun scala_function0 name = ignore o Scala.function1 name o cat_strings0;
73330
0fb889c361e6 tuned signature;
wenzelm
parents: 73324
diff changeset
    81
fun scala_function name = scala_function0 name o map absolute_path;
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    82
73322
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73316
diff changeset
    83
fun make_directory path = (scala_function "make_directory" [path]; path);
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    84
73322
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73316
diff changeset
    85
fun copy_dir src dst = scala_function "copy_dir" [src, dst];
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    86
73322
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73316
diff changeset
    87
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
    88
73322
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73316
diff changeset
    89
fun copy_file_base (base_dir, src) target_dir =
73331
d045cdbdf243 proper relative path (see also df49ca5da9d0, 5b15eee1a661, etc.);
wenzelm
parents: 73330
diff changeset
    90
  scala_function0 "copy_file_base"
d045cdbdf243 proper relative path (see also df49ca5da9d0, 5b15eee1a661, etc.);
wenzelm
parents: 73330
diff changeset
    91
    [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
    92
41307
bb8468ae414e slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents: 40785
diff changeset
    93
56498
6437c989a744 tuned comments (see Scala version);
wenzelm
parents: 50843
diff changeset
    94
(* tmp files *)
41307
bb8468ae414e slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents: 40785
diff changeset
    95
42127
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 41944
diff changeset
    96
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
    97
  let
42127
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 41944
diff changeset
    98
    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
    99
    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
   100
      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
   101
  in path end;
bb8468ae414e slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents: 40785
diff changeset
   102
42127
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 41944
diff changeset
   103
fun with_tmp_file name ext f =
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 41944
diff changeset
   104
  let val path = create_tmp_path name ext
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 41944
diff changeset
   105
  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
   106
56498
6437c989a744 tuned comments (see Scala version);
wenzelm
parents: 50843
diff changeset
   107
6437c989a744 tuned comments (see Scala version);
wenzelm
parents: 50843
diff changeset
   108
(* tmp dirs *)
6437c989a744 tuned comments (see Scala version);
wenzelm
parents: 50843
diff changeset
   109
73324
48abb09d49ea more Isabelle/ML/Scala operations;
wenzelm
parents: 73323
diff changeset
   110
fun rm_tree path = scala_function "rm_tree" [path];
48abb09d49ea more Isabelle/ML/Scala operations;
wenzelm
parents: 73323
diff changeset
   111
41307
bb8468ae414e slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents: 40785
diff changeset
   112
fun with_tmp_dir name f =
72376
04bce3478688 clarified signature;
wenzelm
parents: 72375
diff changeset
   113
  let val path = create_tmp_path name ""
04bce3478688 clarified signature;
wenzelm
parents: 72375
diff changeset
   114
  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
   115
72948
f3d0e4ea492d download as in Isabelle/Scala;
wenzelm
parents: 72511
diff changeset
   116
f3d0e4ea492d download as in Isabelle/Scala;
wenzelm
parents: 72511
diff changeset
   117
(* download file *)
f3d0e4ea492d download as in Isabelle/Scala;
wenzelm
parents: 72511
diff changeset
   118
73336
ff7ce802be52 clarified signature, according to Isabelle/Scala;
wenzelm
parents: 73334
diff changeset
   119
fun download url file =
73565
1aa92bc4d356 clarified signature for Scala functions;
wenzelm
parents: 73547
diff changeset
   120
  ignore (Scala.function "download" [url, absolute_path file]);
72948
f3d0e4ea492d download as in Isabelle/Scala;
wenzelm
parents: 72511
diff changeset
   121
73523
2cd23d587db9 further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents: 73434
diff changeset
   122
2cd23d587db9 further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents: 73434
diff changeset
   123
(* Isabelle distribution identification *)
2cd23d587db9 further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents: 73434
diff changeset
   124
73565
1aa92bc4d356 clarified signature for Scala functions;
wenzelm
parents: 73547
diff changeset
   125
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
   126
2cd23d587db9 further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents: 73434
diff changeset
   127
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
   128
2cd23d587db9 further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents: 73434
diff changeset
   129
fun isabelle_heading () =
2cd23d587db9 further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents: 73434
diff changeset
   130
  (case isabelle_identifier () of
2cd23d587db9 further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents: 73434
diff changeset
   131
    NONE => ""
2cd23d587db9 further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents: 73434
diff changeset
   132
  | SOME version => " (" ^ version ^ ")");
2cd23d587db9 further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents: 73434
diff changeset
   133
2cd23d587db9 further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents: 73434
diff changeset
   134
fun isabelle_name () = getenv_strict "ISABELLE_NAME";
2cd23d587db9 further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents: 73434
diff changeset
   135
73547
a7aabdf889b7 clarified signature;
wenzelm
parents: 73523
diff changeset
   136
fun identification () = "Isabelle/" ^ isabelle_id () ^ isabelle_heading ();
a7aabdf889b7 clarified signature;
wenzelm
parents: 73523
diff changeset
   137
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
   138
end;