src/Pure/System/isabelle_system.ML
author wenzelm
Sat, 27 Feb 2021 17:33:40 +0100
changeset 73316 8664433956b3
parent 73314 87403fde8cc3
child 73322 5b15eee1a661
permissions -rw-r--r--
obsolete;
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
66679
ed8d359d92e4 clarified signature according to Scala version;
wenzelm
parents: 62829
diff changeset
    14
  val rm_tree: Path.T -> unit
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
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
62829
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents: 62549
diff changeset
    72
(* directory operations *)
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    73
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    74
fun system_command cmd =
62829
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents: 62549
diff changeset
    75
  if bash cmd <> 0 then error ("System command failed: " ^ cmd) else ();
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    76
62829
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents: 62549
diff changeset
    77
fun rm_tree path = system_command ("rm -r -f " ^ File.bash_path path);
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    78
72375
e48d93811ed7 clarified signature;
wenzelm
parents: 71912
diff changeset
    79
fun make_directory path =
73314
87403fde8cc3 more direct make_directory in ML and Scala, but ssh still requires perl for Windows UNC paths (see a5dbad753552);
wenzelm
parents: 73281
diff changeset
    80
  (Scala.function "make_directory" (Path.implode (File.absolute_path path)); path);
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    81
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    82
fun copy_dir src dst =
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    83
  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
    84
  else (system_command ("cp -p -R -f " ^ File.bash_path src ^ "/. " ^ File.bash_path dst); ());
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    85
56533
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 56498
diff changeset
    86
fun copy_file src0 dst0 =
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 56498
diff changeset
    87
  let
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 56498
diff changeset
    88
    val src = Path.expand src0;
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 56498
diff changeset
    89
    val dst = Path.expand dst0;
72511
460d743010bc clarified signature: overloaded "+" for Path.append;
wenzelm
parents: 72376
diff changeset
    90
    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
    91
  in
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 56498
diff changeset
    92
    if File.eq (src, target) then ()
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 56498
diff changeset
    93
    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
    94
      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
    95
  end;
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 56498
diff changeset
    96
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 56498
diff changeset
    97
fun copy_file_base (base_dir, src0) target_dir =
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 56498
diff changeset
    98
  let
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 56498
diff changeset
    99
    val src = Path.expand src0;
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 56498
diff changeset
   100
    val src_dir = Path.dir src;
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 56498
diff changeset
   101
    val _ =
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 56498
diff changeset
   102
      if Path.starts_basic src then ()
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 56498
diff changeset
   103
      else error ("Illegal path specification " ^ Path.print src ^ " beyond base directory");
72511
460d743010bc clarified signature: overloaded "+" for Path.append;
wenzelm
parents: 72376
diff changeset
   104
  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
   105
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
(* tmp files *)
41307
bb8468ae414e slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents: 40785
diff changeset
   108
42127
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 41944
diff changeset
   109
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
   110
  let
42127
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 41944
diff changeset
   111
    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
   112
    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
   113
      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
   114
  in path end;
bb8468ae414e slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents: 40785
diff changeset
   115
42127
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 41944
diff changeset
   116
fun with_tmp_file name ext f =
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 41944
diff changeset
   117
  let val path = create_tmp_path name ext
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 41944
diff changeset
   118
  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
   119
56498
6437c989a744 tuned comments (see Scala version);
wenzelm
parents: 50843
diff changeset
   120
6437c989a744 tuned comments (see Scala version);
wenzelm
parents: 50843
diff changeset
   121
(* tmp dirs *)
6437c989a744 tuned comments (see Scala version);
wenzelm
parents: 50843
diff changeset
   122
41307
bb8468ae414e slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents: 40785
diff changeset
   123
fun with_tmp_dir name f =
72376
04bce3478688 clarified signature;
wenzelm
parents: 72375
diff changeset
   124
  let val path = create_tmp_path name ""
04bce3478688 clarified signature;
wenzelm
parents: 72375
diff changeset
   125
  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
   126
72948
f3d0e4ea492d download as in Isabelle/Scala;
wenzelm
parents: 72511
diff changeset
   127
f3d0e4ea492d download as in Isabelle/Scala;
wenzelm
parents: 72511
diff changeset
   128
(* download file *)
f3d0e4ea492d download as in Isabelle/Scala;
wenzelm
parents: 72511
diff changeset
   129
f3d0e4ea492d download as in Isabelle/Scala;
wenzelm
parents: 72511
diff changeset
   130
fun download url =
f3d0e4ea492d download as in Isabelle/Scala;
wenzelm
parents: 72511
diff changeset
   131
  with_tmp_file "download" "" (fn path =>
73275
f0db1e4c89bc clarified signature, following Isabelle/Scala;
wenzelm
parents: 73273
diff changeset
   132
    let
f0db1e4c89bc clarified signature, following Isabelle/Scala;
wenzelm
parents: 73273
diff changeset
   133
      val s = "curl --fail --silent --location " ^ Bash.string url ^ " > " ^ File.bash_path path;
f0db1e4c89bc clarified signature, following Isabelle/Scala;
wenzelm
parents: 73273
diff changeset
   134
      val res = bash_process s;
f0db1e4c89bc clarified signature, following Isabelle/Scala;
wenzelm
parents: 73273
diff changeset
   135
    in
f0db1e4c89bc clarified signature, following Isabelle/Scala;
wenzelm
parents: 73273
diff changeset
   136
      if Process_Result.ok res then File.read path
f0db1e4c89bc clarified signature, following Isabelle/Scala;
wenzelm
parents: 73273
diff changeset
   137
      else cat_error ("Failed to download " ^ quote url) (Process_Result.err res)
f0db1e4c89bc clarified signature, following Isabelle/Scala;
wenzelm
parents: 73273
diff changeset
   138
    end);
72948
f3d0e4ea492d download as in Isabelle/Scala;
wenzelm
parents: 72511
diff changeset
   139
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
   140
end;