src/Pure/System/isabelle_system.ML
author wenzelm
Wed, 08 Aug 2012 12:33:40 +0200
changeset 48731 a45ba78abcc1
parent 47499 4b0daca2bf88
child 50843 1465521b92a1
permissions -rw-r--r--
more casual exit back to ML toplevel, to accomodate commit in SML/NJ which continues at the saved point;
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
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
     9
  val isabelle_tool: string -> string -> int
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    10
  val mkdirs: Path.T -> unit
40745
1dabcda202c3 more basic Isabelle_System.mkdir;
wenzelm
parents: 40743
diff changeset
    11
  val mkdir: Path.T -> unit
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    12
  val copy_dir: Path.T -> Path.T -> unit
42127
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 41944
diff changeset
    13
  val create_tmp_path: string -> string -> Path.T
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 41944
diff changeset
    14
  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
    15
  val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
43849
00f4b305687d access to process output stream via auxiliary fifo;
wenzelm
parents: 43606
diff changeset
    16
  val with_tmp_fifo: (Path.T -> 'a) -> 'a
43851
f7f8cf0a1536 clarified bash_output_fifo;
wenzelm
parents: 43850
diff changeset
    17
  val bash_output_fifo: string -> (Path.T -> 'a) -> 'a
43850
7f2cbc713344 moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents: 43849
diff changeset
    18
  val bash_output: string -> string * int
7f2cbc713344 moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents: 43849
diff changeset
    19
  val bash: string -> int
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    20
end;
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    21
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    22
structure Isabelle_System: ISABELLE_SYSTEM =
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    23
struct
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    24
43850
7f2cbc713344 moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents: 43849
diff changeset
    25
(* bash *)
7f2cbc713344 moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents: 43849
diff changeset
    26
7f2cbc713344 moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents: 43849
diff changeset
    27
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
    28
  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
    29
    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
    30
    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
    31
  in (out, rc) end;
43850
7f2cbc713344 moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents: 43849
diff changeset
    32
7f2cbc713344 moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents: 43849
diff changeset
    33
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
    34
  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
    35
    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
    36
    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
    37
  in rc end;
43850
7f2cbc713344 moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents: 43849
diff changeset
    38
7f2cbc713344 moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents: 43849
diff changeset
    39
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    40
(* system commands *)
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    41
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    42
fun isabelle_tool name args =
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    43
  (case space_explode ":" (getenv "ISABELLE_TOOLS") |> get_first (fn dir =>
43606
e1a09c2a6248 prefer Isabelle path algebra;
wenzelm
parents: 42127
diff changeset
    44
      let val path = File.platform_path (Path.append (Path.explode dir) (Path.basic name)) in
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    45
        if can OS.FileSys.modTime path andalso
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    46
          not (OS.FileSys.isDir path) andalso
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    47
          OS.FileSys.access (path, [OS.FileSys.A_READ, OS.FileSys.A_EXEC])
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    48
        then SOME path
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    49
        else NONE
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    50
      end handle OS.SysErr _ => NONE) of
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    51
    SOME path => bash (File.shell_quote path ^ " " ^ args)
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
    52
  | NONE => (warning ("Unknown Isabelle tool: " ^ name); 2));
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    53
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    54
fun system_command cmd =
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    55
  if bash cmd <> 0 then error ("System command failed: " ^ cmd)
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    56
  else ();
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    57
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    58
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    59
(* directory operations *)
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    60
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    61
fun mkdirs path = system_command ("mkdir -p " ^ File.shell_path path);
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    62
40785
c755df0f7062 more permissive Isabelle_System.mkdir;
wenzelm
parents: 40745
diff changeset
    63
fun mkdir path =
c755df0f7062 more permissive Isabelle_System.mkdir;
wenzelm
parents: 40745
diff changeset
    64
  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
    65
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    66
fun copy_dir src dst =
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    67
  if File.eq (src, dst) then ()
46502
3d43d4d4d071 more uniform / portable representation of the idea of "copy_dir" (NB: cp -f dereferences symlinks on GNU/Linux, but does not on old-school Unixen including BSD/Mac OS X);
wenzelm
parents: 45199
diff changeset
    68
  else (system_command ("cp -p -R -f " ^ File.shell_path src ^ "/. " ^ File.shell_path dst); ());
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    69
41307
bb8468ae414e slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents: 40785
diff changeset
    70
bb8468ae414e slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents: 40785
diff changeset
    71
(* unique tmp files *)
bb8468ae414e slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents: 40785
diff changeset
    72
42127
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 41944
diff changeset
    73
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
    74
  let
42127
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 41944
diff changeset
    75
    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
    76
    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
    77
      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
    78
  in path end;
bb8468ae414e slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents: 40785
diff changeset
    79
42127
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 41944
diff changeset
    80
fun with_tmp_file name ext f =
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 41944
diff changeset
    81
  let val path = create_tmp_path name ext
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 41944
diff changeset
    82
  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
    83
42127
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 41944
diff changeset
    84
fun rm_tree path = system_command ("rm -r -f " ^ File.shell_path path);
41307
bb8468ae414e slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents: 40785
diff changeset
    85
bb8468ae414e slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents: 40785
diff changeset
    86
fun with_tmp_dir name f =
bb8468ae414e slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents: 40785
diff changeset
    87
  let
42127
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 41944
diff changeset
    88
    val path = create_tmp_path name "";
41307
bb8468ae414e slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents: 40785
diff changeset
    89
    val _ = mkdirs path;
41352
87adb55fb0fb make SML/NJ and Poly/ML agree on the type of "before";
wenzelm
parents: 41307
diff changeset
    90
  in Exn.release (Exn.capture f 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
    91
43850
7f2cbc713344 moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents: 43849
diff changeset
    92
43851
f7f8cf0a1536 clarified bash_output_fifo;
wenzelm
parents: 43850
diff changeset
    93
(* fifo *)
43850
7f2cbc713344 moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents: 43849
diff changeset
    94
43849
00f4b305687d access to process output stream via auxiliary fifo;
wenzelm
parents: 43606
diff changeset
    95
fun with_tmp_fifo f =
00f4b305687d access to process output stream via auxiliary fifo;
wenzelm
parents: 43606
diff changeset
    96
  with_tmp_file "isabelle-fifo-" ""
00f4b305687d access to process output stream via auxiliary fifo;
wenzelm
parents: 43606
diff changeset
    97
    (fn path =>
00f4b305687d access to process output stream via auxiliary fifo;
wenzelm
parents: 43606
diff changeset
    98
      (case bash_output ("mkfifo -m 600 " ^ File.shell_path path) of
00f4b305687d access to process output stream via auxiliary fifo;
wenzelm
parents: 43606
diff changeset
    99
        (_, 0) => f path
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
   100
      | (out, _) => error (trim_line out)));
43849
00f4b305687d access to process output stream via auxiliary fifo;
wenzelm
parents: 43606
diff changeset
   101
45199
42316b81ef49 tuned comment;
wenzelm
parents: 44109
diff changeset
   102
(* FIXME blocks on Cygwin 1.7.x *)
42316b81ef49 tuned comment;
wenzelm
parents: 44109
diff changeset
   103
(* See also http://cygwin.com/ml/cygwin/2010-08/msg00459.html *)
42316b81ef49 tuned comment;
wenzelm
parents: 44109
diff changeset
   104
fun bash_output_fifo script f =
43849
00f4b305687d access to process output stream via auxiliary fifo;
wenzelm
parents: 43606
diff changeset
   105
  with_tmp_fifo (fn fifo =>
00f4b305687d access to process output stream via auxiliary fifo;
wenzelm
parents: 43606
diff changeset
   106
    uninterruptible (fn restore_attributes => fn () =>
43850
7f2cbc713344 moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents: 43849
diff changeset
   107
      (case Bash.process (script ^ " > " ^ File.shell_path fifo ^ " &") of
43849
00f4b305687d access to process output stream via auxiliary fifo;
wenzelm
parents: 43606
diff changeset
   108
        {rc = 0, terminate, ...} =>
43851
f7f8cf0a1536 clarified bash_output_fifo;
wenzelm
parents: 43850
diff changeset
   109
          (restore_attributes f fifo handle exn => (terminate (); reraise exn))
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
   110
      | {out, ...} => error (trim_line out))) ());
43849
00f4b305687d access to process output stream via auxiliary fifo;
wenzelm
parents: 43606
diff changeset
   111
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
   112
end;
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
   113