src/Pure/System/isabelle_system.ML
author wenzelm
Sat, 19 Dec 2020 00:00:58 +0100
changeset 72948 f3d0e4ea492d
parent 72511 460d743010bc
child 72951 74339f1a5dd7
permissions -rw-r--r--
download as in Isabelle/Scala;
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
71902
1529336eaedc check bash functions against Isabelle settings environment;
wenzelm
parents: 70050
diff changeset
     9
  val bash_output_check: string -> string
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
40745
1dabcda202c3 more basic Isabelle_System.mkdir;
wenzelm
parents: 40743
diff changeset
    16
  val mkdir: Path.T -> unit
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    17
  val copy_dir: Path.T -> Path.T -> unit
56533
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 56498
diff changeset
    18
  val copy_file: Path.T -> Path.T -> unit
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 56498
diff changeset
    19
  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
    20
  val create_tmp_path: string -> string -> Path.T
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 41944
diff changeset
    21
  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
    22
  val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
72948
f3d0e4ea492d download as in Isabelle/Scala;
wenzelm
parents: 72511
diff changeset
    23
  val download: string -> string
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    24
end;
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    25
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    26
structure Isabelle_System: ISABELLE_SYSTEM =
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    27
struct
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    28
43850
7f2cbc713344 moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents: 43849
diff changeset
    29
(* bash *)
7f2cbc713344 moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents: 43849
diff changeset
    30
70050
5b66e6672ccf tuned signature: more operations;
wenzelm
parents: 66679
diff changeset
    31
fun bash_output_check s =
5b66e6672ccf tuned signature: more operations;
wenzelm
parents: 66679
diff changeset
    32
  (case Bash.process s of
5b66e6672ccf tuned signature: more operations;
wenzelm
parents: 66679
diff changeset
    33
    {rc = 0, out, ...} => (trim_line out)
5b66e6672ccf tuned signature: more operations;
wenzelm
parents: 66679
diff changeset
    34
  | {err, ...} => error (trim_line err));
5b66e6672ccf tuned signature: more operations;
wenzelm
parents: 66679
diff changeset
    35
43850
7f2cbc713344 moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents: 43849
diff changeset
    36
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
    37
  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
    38
    val {out, err, rc, ...} = Bash.process s;
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
    39
    val _ = warning (trim_line err);
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
    40
  in (out, rc) end;
43850
7f2cbc713344 moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents: 43849
diff changeset
    41
7f2cbc713344 moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents: 43849
diff changeset
    42
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
    43
  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
    44
    val (out, rc) = bash_output s;
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
    45
    val _ = writeln (trim_line out);
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
    46
  in rc end;
43850
7f2cbc713344 moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents: 43849
diff changeset
    47
7f2cbc713344 moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents: 43849
diff changeset
    48
71902
1529336eaedc check bash functions against Isabelle settings environment;
wenzelm
parents: 70050
diff changeset
    49
(* bash functions *)
1529336eaedc check bash functions against Isabelle settings environment;
wenzelm
parents: 70050
diff changeset
    50
1529336eaedc check bash functions against Isabelle settings environment;
wenzelm
parents: 70050
diff changeset
    51
fun bash_functions () =
1529336eaedc check bash functions against Isabelle settings environment;
wenzelm
parents: 70050
diff changeset
    52
  bash_output_check "declare -Fx"
1529336eaedc check bash functions against Isabelle settings environment;
wenzelm
parents: 70050
diff changeset
    53
  |> split_lines |> map_filter (space_explode " " #> try List.last);
1529336eaedc check bash functions against Isabelle settings environment;
wenzelm
parents: 70050
diff changeset
    54
71911
d25093536482 clarified signature;
wenzelm
parents: 71902
diff changeset
    55
fun check_bash_function ctxt arg =
71912
b9fbc93f3a24 clarified markup;
wenzelm
parents: 71911
diff changeset
    56
  Completion.check_entity Markup.bash_functionN
b9fbc93f3a24 clarified markup;
wenzelm
parents: 71911
diff changeset
    57
    (bash_functions () |> map (rpair Position.none)) ctxt arg;
71902
1529336eaedc check bash functions against Isabelle settings environment;
wenzelm
parents: 70050
diff changeset
    58
1529336eaedc check bash functions against Isabelle settings environment;
wenzelm
parents: 70050
diff changeset
    59
62829
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents: 62549
diff changeset
    60
(* directory operations *)
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    61
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    62
fun system_command cmd =
62829
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents: 62549
diff changeset
    63
  if bash cmd <> 0 then error ("System command failed: " ^ cmd) else ();
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    64
62829
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents: 62549
diff changeset
    65
fun rm_tree path = system_command ("rm -r -f " ^ File.bash_path path);
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    66
72375
e48d93811ed7 clarified signature;
wenzelm
parents: 71912
diff changeset
    67
fun make_directory path =
72376
04bce3478688 clarified signature;
wenzelm
parents: 72375
diff changeset
    68
  let
04bce3478688 clarified signature;
wenzelm
parents: 72375
diff changeset
    69
    val _ =
04bce3478688 clarified signature;
wenzelm
parents: 72375
diff changeset
    70
      if File.is_dir path then ()
04bce3478688 clarified signature;
wenzelm
parents: 72375
diff changeset
    71
      else
04bce3478688 clarified signature;
wenzelm
parents: 72375
diff changeset
    72
       (bash ("perl -e \"use File::Path make_path; make_path('" ^ File.standard_path path ^ "');\"");
04bce3478688 clarified signature;
wenzelm
parents: 72375
diff changeset
    73
        if File.is_dir path then () else error ("Failed to create directory: " ^ Path.print path));
04bce3478688 clarified signature;
wenzelm
parents: 72375
diff changeset
    74
  in path end;
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    75
40785
c755df0f7062 more permissive Isabelle_System.mkdir;
wenzelm
parents: 40745
diff changeset
    76
fun mkdir path =
c755df0f7062 more permissive Isabelle_System.mkdir;
wenzelm
parents: 40745
diff changeset
    77
  if File.is_dir path then () else OS.FileSys.mkDir (File.platform_path path);
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    78
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    79
fun copy_dir src dst =
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    80
  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
    81
  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
    82
56533
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 56498
diff changeset
    83
fun copy_file src0 dst0 =
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 56498
diff changeset
    84
  let
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 56498
diff changeset
    85
    val src = Path.expand src0;
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 56498
diff changeset
    86
    val dst = Path.expand dst0;
72511
460d743010bc clarified signature: overloaded "+" for Path.append;
wenzelm
parents: 72376
diff changeset
    87
    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
    88
  in
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 56498
diff changeset
    89
    if File.eq (src, target) then ()
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 56498
diff changeset
    90
    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
    91
      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
    92
  end;
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 56498
diff changeset
    93
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 56498
diff changeset
    94
fun copy_file_base (base_dir, src0) target_dir =
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 56498
diff changeset
    95
  let
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 56498
diff changeset
    96
    val src = Path.expand src0;
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 56498
diff changeset
    97
    val src_dir = Path.dir src;
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 56498
diff changeset
    98
    val _ =
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 56498
diff changeset
    99
      if Path.starts_basic src then ()
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 56498
diff changeset
   100
      else error ("Illegal path specification " ^ Path.print src ^ " beyond base directory");
72511
460d743010bc clarified signature: overloaded "+" for Path.append;
wenzelm
parents: 72376
diff changeset
   101
  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
   102
41307
bb8468ae414e slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents: 40785
diff changeset
   103
56498
6437c989a744 tuned comments (see Scala version);
wenzelm
parents: 50843
diff changeset
   104
(* tmp files *)
41307
bb8468ae414e slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents: 40785
diff changeset
   105
42127
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 41944
diff changeset
   106
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
   107
  let
42127
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 41944
diff changeset
   108
    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
   109
    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
   110
      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
   111
  in path end;
bb8468ae414e slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents: 40785
diff changeset
   112
42127
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 41944
diff changeset
   113
fun with_tmp_file name ext f =
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 41944
diff changeset
   114
  let val path = create_tmp_path name ext
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 41944
diff changeset
   115
  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
   116
56498
6437c989a744 tuned comments (see Scala version);
wenzelm
parents: 50843
diff changeset
   117
6437c989a744 tuned comments (see Scala version);
wenzelm
parents: 50843
diff changeset
   118
(* tmp dirs *)
6437c989a744 tuned comments (see Scala version);
wenzelm
parents: 50843
diff changeset
   119
41307
bb8468ae414e slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents: 40785
diff changeset
   120
fun with_tmp_dir name f =
72376
04bce3478688 clarified signature;
wenzelm
parents: 72375
diff changeset
   121
  let val path = create_tmp_path name ""
04bce3478688 clarified signature;
wenzelm
parents: 72375
diff changeset
   122
  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
   123
72948
f3d0e4ea492d download as in Isabelle/Scala;
wenzelm
parents: 72511
diff changeset
   124
f3d0e4ea492d download as in Isabelle/Scala;
wenzelm
parents: 72511
diff changeset
   125
(* download file *)
f3d0e4ea492d download as in Isabelle/Scala;
wenzelm
parents: 72511
diff changeset
   126
f3d0e4ea492d download as in Isabelle/Scala;
wenzelm
parents: 72511
diff changeset
   127
fun download url =
f3d0e4ea492d download as in Isabelle/Scala;
wenzelm
parents: 72511
diff changeset
   128
  with_tmp_file "download" "" (fn path =>
f3d0e4ea492d download as in Isabelle/Scala;
wenzelm
parents: 72511
diff changeset
   129
    ("curl --fail --silent --location " ^ Bash.string url ^ " > " ^ File.bash_path path)
f3d0e4ea492d download as in Isabelle/Scala;
wenzelm
parents: 72511
diff changeset
   130
    |> Bash.process
f3d0e4ea492d download as in Isabelle/Scala;
wenzelm
parents: 72511
diff changeset
   131
    |> (fn {rc = 0, ...} => File.read path
f3d0e4ea492d download as in Isabelle/Scala;
wenzelm
parents: 72511
diff changeset
   132
         | {err, ...} => cat_error ("Failed to download " ^ quote url) err));
f3d0e4ea492d download as in Isabelle/Scala;
wenzelm
parents: 72511
diff changeset
   133
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
   134
end;