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;
authorwenzelm
Mon Apr 16 23:07:40 2012 +0200 (2012-04-16)
changeset 474994b0daca2bf88
parent 47498 e3fc50c7da13
child 47500 5024b37c489c
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;
src/HOL/Tools/ATP/atp_systems.ML
src/Pure/Concurrent/bash.ML
src/Pure/Concurrent/bash_sequential.ML
src/Pure/System/isabelle_system.ML
src/Pure/library.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Apr 16 21:53:11 2012 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Apr 16 23:07:40 2012 +0200
     1.3 @@ -542,7 +542,7 @@
     1.4    | (output, _) =>
     1.5      error (case extract_known_failure known_perl_failures output of
     1.6               SOME failure => string_for_failure failure
     1.7 -           | NONE => perhaps (try (unsuffix "\n")) output ^ ".")
     1.8 +           | NONE => trim_line output ^ ".")
     1.9  
    1.10  fun find_system name [] systems =
    1.11      find_first (String.isPrefix (name ^ "---")) systems
     2.1 --- a/src/Pure/Concurrent/bash.ML	Mon Apr 16 21:53:11 2012 +0200
     2.2 +++ b/src/Pure/Concurrent/bash.ML	Mon Apr 16 23:07:40 2012 +0200
     2.3 @@ -6,7 +6,7 @@
     2.4  
     2.5  signature BASH =
     2.6  sig
     2.7 -  val process: string -> {output: string, rc: int, terminate: unit -> unit}
     2.8 +  val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
     2.9  end;
    2.10  
    2.11  structure Bash: BASH =
    2.12 @@ -19,7 +19,8 @@
    2.13  
    2.14      val id = serial_string ();
    2.15      val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
    2.16 -    val output_path = File.tmp_path (Path.basic ("bash_output" ^ id));
    2.17 +    val out_path = File.tmp_path (Path.basic ("bash_out" ^ id));
    2.18 +    val err_path = File.tmp_path (Path.basic ("bash_err" ^ id));
    2.19      val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id));
    2.20  
    2.21      val system_thread =
    2.22 @@ -31,8 +32,9 @@
    2.23                OS.Process.system
    2.24                  ("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^
    2.25                    File.shell_path pid_path ^ " script \"exec bash " ^
    2.26 -                  File.shell_path script_path ^ " > " ^
    2.27 -                  File.shell_path output_path ^ "\"");
    2.28 +                  File.shell_path script_path ^
    2.29 +                  " > " ^ File.shell_path out_path ^
    2.30 +                  " 2> " ^ File.shell_path err_path ^ "\"");
    2.31              val res =
    2.32                (case Posix.Process.fromStatus status of
    2.33                  Posix.Process.W_EXITED => Result 0
    2.34 @@ -75,7 +77,8 @@
    2.35      fun cleanup () =
    2.36       (Simple_Thread.interrupt_unsynchronized system_thread;
    2.37        try File.rm script_path;
    2.38 -      try File.rm output_path;
    2.39 +      try File.rm out_path;
    2.40 +      try File.rm err_path;
    2.41        try File.rm pid_path);
    2.42    in
    2.43      let
    2.44 @@ -83,11 +86,12 @@
    2.45          restore_attributes (fn () =>
    2.46            Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) ();
    2.47  
    2.48 -      val output = the_default "" (try File.read output_path);
    2.49 +      val out = the_default "" (try File.read out_path);
    2.50 +      val err = the_default "" (try File.read err_path);
    2.51        val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
    2.52        val pid = get_pid ();
    2.53        val _ = cleanup ();
    2.54 -    in {output = output, rc = rc, terminate = fn () => terminate pid} end
    2.55 +    in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end
    2.56      handle exn => (terminate (get_pid ()); cleanup (); reraise exn)
    2.57    end);
    2.58  
     3.1 --- a/src/Pure/Concurrent/bash_sequential.ML	Mon Apr 16 21:53:11 2012 +0200
     3.2 +++ b/src/Pure/Concurrent/bash_sequential.ML	Mon Apr 16 23:07:40 2012 +0200
     3.3 @@ -7,7 +7,7 @@
     3.4  
     3.5  signature BASH =
     3.6  sig
     3.7 -  val process: string -> {output: string, rc: int, terminate: unit -> unit}
     3.8 +  val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
     3.9  end;
    3.10  
    3.11  structure Bash: BASH =
    3.12 @@ -17,16 +17,18 @@
    3.13    let
    3.14      val id = serial_string ();
    3.15      val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
    3.16 -    val output_path = File.tmp_path (Path.basic ("bash_output" ^ id));
    3.17 -    fun cleanup () = (try File.rm script_path; try File.rm output_path);
    3.18 +    val out_path = File.tmp_path (Path.basic ("bash_out" ^ id));
    3.19 +    val err_path = File.tmp_path (Path.basic ("bash_err" ^ id));
    3.20 +    fun cleanup () = (try File.rm script_path; try File.rm out_path; try File.rm err_path);
    3.21    in
    3.22      let
    3.23        val _ = File.write script_path script;
    3.24        val status =
    3.25          OS.Process.system
    3.26            ("exec \"$ISABELLE_HOME/lib/scripts/process\" no_group /dev/null" ^
    3.27 -            " script \"exec bash " ^ File.shell_path script_path ^ " > " ^
    3.28 -            File.shell_path output_path ^ "\"");
    3.29 +            " script \"exec bash " ^ File.shell_path script_path ^
    3.30 +            " > " ^ File.shell_path out_path ^
    3.31 +            " 2> " ^ File.shell_path err_path ^ "\"");
    3.32        val rc =
    3.33          (case Posix.Process.fromStatus status of
    3.34            Posix.Process.W_EXITED => 0
    3.35 @@ -34,9 +36,10 @@
    3.36          | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s)
    3.37          | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s));
    3.38  
    3.39 -      val output = the_default "" (try File.read output_path);
    3.40 +      val out = the_default "" (try File.read out_path);
    3.41 +      val err = the_default "" (try File.read err_path);
    3.42        val _ = cleanup ();
    3.43 -    in {output = output, rc = rc, terminate = fn () => ()} end
    3.44 +    in {out = out, err = err, rc = rc, terminate = fn () => ()} end
    3.45      handle exn => (cleanup (); reraise exn)
    3.46    end;
    3.47  
     4.1 --- a/src/Pure/System/isabelle_system.ML	Mon Apr 16 21:53:11 2012 +0200
     4.2 +++ b/src/Pure/System/isabelle_system.ML	Mon Apr 16 23:07:40 2012 +0200
     4.3 @@ -25,13 +25,16 @@
     4.4  (* bash *)
     4.5  
     4.6  fun bash_output s =
     4.7 -  let val {output, rc, ...} = Bash.process s
     4.8 -  in (output, rc) end;
     4.9 +  let
    4.10 +    val {out, err, rc, ...} = Bash.process s;
    4.11 +    val _ = warning (trim_line err);
    4.12 +  in (out, rc) end;
    4.13  
    4.14  fun bash s =
    4.15 -  (case bash_output s of
    4.16 -    ("", rc) => rc
    4.17 -  | (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc));
    4.18 +  let
    4.19 +    val (out, rc) = bash_output s;
    4.20 +    val _ = writeln (trim_line out);
    4.21 +  in rc end;
    4.22  
    4.23  
    4.24  (* system commands *)
    4.25 @@ -46,7 +49,7 @@
    4.26          else NONE
    4.27        end handle OS.SysErr _ => NONE) of
    4.28      SOME path => bash (File.shell_quote path ^ " " ^ args)
    4.29 -  | NONE => (writeln ("Unknown Isabelle tool: " ^ name); 2));
    4.30 +  | NONE => (warning ("Unknown Isabelle tool: " ^ name); 2));
    4.31  
    4.32  fun system_command cmd =
    4.33    if bash cmd <> 0 then error ("System command failed: " ^ cmd)
    4.34 @@ -94,7 +97,7 @@
    4.35      (fn path =>
    4.36        (case bash_output ("mkfifo -m 600 " ^ File.shell_path path) of
    4.37          (_, 0) => f path
    4.38 -      | (out, _) => error (perhaps (try (unsuffix "\n")) out)));
    4.39 +      | (out, _) => error (trim_line out)));
    4.40  
    4.41  (* FIXME blocks on Cygwin 1.7.x *)
    4.42  (* See also http://cygwin.com/ml/cygwin/2010-08/msg00459.html *)
    4.43 @@ -104,7 +107,7 @@
    4.44        (case Bash.process (script ^ " > " ^ File.shell_path fifo ^ " &") of
    4.45          {rc = 0, terminate, ...} =>
    4.46            (restore_attributes f fifo handle exn => (terminate (); reraise exn))
    4.47 -      | {output, ...} => error (perhaps (try (unsuffix "\n")) output))) ());
    4.48 +      | {out, ...} => error (trim_line out))) ());
    4.49  
    4.50  end;
    4.51  
     5.1 --- a/src/Pure/library.ML	Mon Apr 16 21:53:11 2012 +0200
     5.2 +++ b/src/Pure/library.ML	Mon Apr 16 23:07:40 2012 +0200
     5.3 @@ -150,6 +150,7 @@
     5.4    val suffix: string -> string -> string
     5.5    val unprefix: string -> string -> string
     5.6    val unsuffix: string -> string -> string
     5.7 +  val trim_line: string -> string
     5.8    val replicate_string: int -> string -> string
     5.9    val translate_string: (string -> string) -> string -> string
    5.10    val match_string: string -> string -> bool
    5.11 @@ -755,6 +756,8 @@
    5.12    if String.isSuffix sffx s then String.substring (s, 0, size s - size sffx)
    5.13    else raise Fail "unsuffix";
    5.14  
    5.15 +val trim_line = perhaps (try (unsuffix "\n"));
    5.16 +
    5.17  fun replicate_string (0: int) _ = ""
    5.18    | replicate_string 1 a = a
    5.19    | replicate_string k a =