back to static conditional compilation -- simplified bootstrap;
authorwenzelm
Tue Apr 05 21:23:32 2016 +0200 (2016-04-05)
changeset 628794764473c9b8d
parent 62878 1cec457e0a03
child 62880 76e7d9169b54
back to static conditional compilation -- simplified bootstrap;
lib/scripts/isabelle-platform
src/Pure/ROOT.ML
src/Pure/System/bash.ML
src/Pure/System/windows/bash.ML
     1.1 --- a/lib/scripts/isabelle-platform	Tue Apr 05 20:51:37 2016 +0200
     1.2 +++ b/lib/scripts/isabelle-platform	Tue Apr 05 21:23:32 2016 +0200
     1.3 @@ -4,6 +4,7 @@
     1.4  #
     1.5  # NOTE: The ML system or JVM may have their own idea about the platform!
     1.6  
     1.7 +ISABELLE_WINDOWS_PREFIX=""
     1.8  ISABELLE_PLATFORM_FAMILY=""
     1.9  ISABELLE_PLATFORM32=""
    1.10  ISABELLE_PLATFORM64=""
    1.11 @@ -11,6 +12,7 @@
    1.12  case $(uname -s) in
    1.13    Linux)
    1.14      ISABELLE_PLATFORM_FAMILY="linux"
    1.15 +    ISABELLE_WINDOWS_PREFIX="."
    1.16      case $(uname -m) in
    1.17        i?86)
    1.18          ISABELLE_PLATFORM32=x86-linux
    1.19 @@ -23,6 +25,7 @@
    1.20      ;;
    1.21    Darwin)
    1.22      ISABELLE_PLATFORM_FAMILY="macos"
    1.23 +    ISABELLE_WINDOWS_PREFIX="."
    1.24      case $(uname -m) in
    1.25        i?86)
    1.26          ISABELLE_PLATFORM32=x86-darwin
    1.27 @@ -38,6 +41,7 @@
    1.28      ;;
    1.29    CYGWIN_NT*)
    1.30      ISABELLE_PLATFORM_FAMILY="windows"
    1.31 +    ISABELLE_WINDOWS_PREFIX="windows"
    1.32      case $(uname -m) in
    1.33        i?86 | x86_64)
    1.34          ISABELLE_PLATFORM32=x86-cygwin
     2.1 --- a/src/Pure/ROOT.ML	Tue Apr 05 20:51:37 2016 +0200
     2.2 +++ b/src/Pure/ROOT.ML	Tue Apr 05 21:23:32 2016 +0200
     2.3 @@ -279,7 +279,7 @@
     2.4  use "Proof/extraction.ML";
     2.5  
     2.6  (*Isabelle system*)
     2.7 -use "System/bash.ML";
     2.8 +use "System/$ISABELLE_WINDOWS_PREFIX/bash.ML";
     2.9  use "System/isabelle_system.ML";
    2.10  
    2.11  
     3.1 --- a/src/Pure/System/bash.ML	Tue Apr 05 20:51:37 2016 +0200
     3.2 +++ b/src/Pure/System/bash.ML	Tue Apr 05 21:23:32 2016 +0200
     3.3 @@ -1,7 +1,7 @@
     3.4  (*  Title:      Pure/System/bash.ML
     3.5      Author:     Makarius
     3.6  
     3.7 -GNU bash processes, with propagation of interrupts.
     3.8 +GNU bash processes, with propagation of interrupts -- POSIX version.
     3.9  *)
    3.10  
    3.11  signature BASH =
    3.12 @@ -9,99 +9,6 @@
    3.13    val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
    3.14  end;
    3.15  
    3.16 -if ML_System.platform_is_windows then ML
    3.17 -\<open>
    3.18 -structure Bash: BASH =
    3.19 -struct
    3.20 -
    3.21 -val process = uninterruptible (fn restore_attributes => fn script =>
    3.22 -  let
    3.23 -    datatype result = Wait | Signal | Result of int;
    3.24 -    val result = Synchronized.var "bash_result" Wait;
    3.25 -
    3.26 -    val id = serial_string ();
    3.27 -    val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
    3.28 -    val out_path = File.tmp_path (Path.basic ("bash_out" ^ id));
    3.29 -    val err_path = File.tmp_path (Path.basic ("bash_err" ^ id));
    3.30 -    val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id));
    3.31 -
    3.32 -    fun cleanup_files () =
    3.33 -     (try File.rm script_path;
    3.34 -      try File.rm out_path;
    3.35 -      try File.rm err_path;
    3.36 -      try File.rm pid_path);
    3.37 -    val _ = cleanup_files ();
    3.38 -
    3.39 -    val system_thread =
    3.40 -      Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
    3.41 -        Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
    3.42 -          let
    3.43 -            val _ = File.write script_path script;
    3.44 -            val bash_script =
    3.45 -              "bash " ^ File.bash_path script_path ^
    3.46 -                " > " ^ File.bash_path out_path ^
    3.47 -                " 2> " ^ File.bash_path err_path;
    3.48 -            val bash_process = getenv_strict "ISABELLE_BASH_PROCESS";
    3.49 -            val rc =
    3.50 -              Windows.simpleExecute ("",
    3.51 -                quote (ML_System.platform_path bash_process) ^ " " ^
    3.52 -                quote (File.platform_path pid_path) ^  " \"\" bash -c " ^ quote bash_script)
    3.53 -              |> Windows.fromStatus |> SysWord.toInt;
    3.54 -            val res = if rc = 130 orelse rc = 512 then Signal else Result rc;
    3.55 -          in Synchronized.change result (K res) end
    3.56 -          handle exn =>
    3.57 -            (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn)));
    3.58 -
    3.59 -    fun read_pid 0 = NONE
    3.60 -      | read_pid count =
    3.61 -          (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of
    3.62 -            NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1))
    3.63 -          | some => some);
    3.64 -
    3.65 -    fun terminate NONE = ()
    3.66 -      | terminate (SOME pid) =
    3.67 -          let
    3.68 -            fun kill s =
    3.69 -              let
    3.70 -                val cmd = getenv_strict "CYGWIN_ROOT" ^ "\\bin\\bash.exe";
    3.71 -                val arg = "kill -" ^ s ^ " -" ^ string_of_int pid;
    3.72 -              in
    3.73 -                OS.Process.isSuccess (Windows.simpleExecute ("", quote cmd ^ " -c " ^ quote arg))
    3.74 -                  handle OS.SysErr _ => false
    3.75 -              end;
    3.76 -
    3.77 -            fun multi_kill count s =
    3.78 -              count = 0 orelse
    3.79 -                (kill s; kill "0") andalso
    3.80 -                (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s);
    3.81 -            val _ =
    3.82 -              multi_kill 10 "INT" andalso
    3.83 -              multi_kill 10 "TERM" andalso
    3.84 -              multi_kill 10 "KILL";
    3.85 -          in () end;
    3.86 -
    3.87 -    fun cleanup () =
    3.88 -     (Standard_Thread.interrupt_unsynchronized system_thread;
    3.89 -      cleanup_files ());
    3.90 -  in
    3.91 -    let
    3.92 -      val _ =
    3.93 -        restore_attributes (fn () =>
    3.94 -          Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) ();
    3.95 -
    3.96 -      val out = the_default "" (try File.read out_path);
    3.97 -      val err = the_default "" (try File.read err_path);
    3.98 -      val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
    3.99 -      val pid = read_pid 1;
   3.100 -      val _ = cleanup ();
   3.101 -    in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end
   3.102 -    handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn)
   3.103 -  end);
   3.104 -
   3.105 -end;
   3.106 -\<close>
   3.107 -else ML
   3.108 -\<open>
   3.109  structure Bash: BASH =
   3.110  struct
   3.111  
   3.112 @@ -192,4 +99,3 @@
   3.113    end);
   3.114  
   3.115  end;
   3.116 -\<close>;
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/System/windows/bash.ML	Tue Apr 05 21:23:32 2016 +0200
     4.3 @@ -0,0 +1,99 @@
     4.4 +(*  Title:      Pure/System/windows/bash.ML
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +GNU bash processes, with propagation of interrupts -- Windows version.
     4.8 +*)
     4.9 +
    4.10 +signature BASH =
    4.11 +sig
    4.12 +  val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
    4.13 +end;
    4.14 +
    4.15 +structure Bash: BASH =
    4.16 +struct
    4.17 +
    4.18 +val process = uninterruptible (fn restore_attributes => fn script =>
    4.19 +  let
    4.20 +    datatype result = Wait | Signal | Result of int;
    4.21 +    val result = Synchronized.var "bash_result" Wait;
    4.22 +
    4.23 +    val id = serial_string ();
    4.24 +    val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
    4.25 +    val out_path = File.tmp_path (Path.basic ("bash_out" ^ id));
    4.26 +    val err_path = File.tmp_path (Path.basic ("bash_err" ^ id));
    4.27 +    val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id));
    4.28 +
    4.29 +    fun cleanup_files () =
    4.30 +     (try File.rm script_path;
    4.31 +      try File.rm out_path;
    4.32 +      try File.rm err_path;
    4.33 +      try File.rm pid_path);
    4.34 +    val _ = cleanup_files ();
    4.35 +
    4.36 +    val system_thread =
    4.37 +      Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
    4.38 +        Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
    4.39 +          let
    4.40 +            val _ = File.write script_path script;
    4.41 +            val bash_script =
    4.42 +              "bash " ^ File.bash_path script_path ^
    4.43 +                " > " ^ File.bash_path out_path ^
    4.44 +                " 2> " ^ File.bash_path err_path;
    4.45 +            val bash_process = getenv_strict "ISABELLE_BASH_PROCESS";
    4.46 +            val rc =
    4.47 +              Windows.simpleExecute ("",
    4.48 +                quote (ML_System.platform_path bash_process) ^ " " ^
    4.49 +                quote (File.platform_path pid_path) ^  " \"\" bash -c " ^ quote bash_script)
    4.50 +              |> Windows.fromStatus |> SysWord.toInt;
    4.51 +            val res = if rc = 130 orelse rc = 512 then Signal else Result rc;
    4.52 +          in Synchronized.change result (K res) end
    4.53 +          handle exn =>
    4.54 +            (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn)));
    4.55 +
    4.56 +    fun read_pid 0 = NONE
    4.57 +      | read_pid count =
    4.58 +          (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of
    4.59 +            NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1))
    4.60 +          | some => some);
    4.61 +
    4.62 +    fun terminate NONE = ()
    4.63 +      | terminate (SOME pid) =
    4.64 +          let
    4.65 +            fun kill s =
    4.66 +              let
    4.67 +                val cmd = getenv_strict "CYGWIN_ROOT" ^ "\\bin\\bash.exe";
    4.68 +                val arg = "kill -" ^ s ^ " -" ^ string_of_int pid;
    4.69 +              in
    4.70 +                OS.Process.isSuccess (Windows.simpleExecute ("", quote cmd ^ " -c " ^ quote arg))
    4.71 +                  handle OS.SysErr _ => false
    4.72 +              end;
    4.73 +
    4.74 +            fun multi_kill count s =
    4.75 +              count = 0 orelse
    4.76 +                (kill s; kill "0") andalso
    4.77 +                (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s);
    4.78 +            val _ =
    4.79 +              multi_kill 10 "INT" andalso
    4.80 +              multi_kill 10 "TERM" andalso
    4.81 +              multi_kill 10 "KILL";
    4.82 +          in () end;
    4.83 +
    4.84 +    fun cleanup () =
    4.85 +     (Standard_Thread.interrupt_unsynchronized system_thread;
    4.86 +      cleanup_files ());
    4.87 +  in
    4.88 +    let
    4.89 +      val _ =
    4.90 +        restore_attributes (fn () =>
    4.91 +          Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) ();
    4.92 +
    4.93 +      val out = the_default "" (try File.read out_path);
    4.94 +      val err = the_default "" (try File.read err_path);
    4.95 +      val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
    4.96 +      val pid = read_pid 1;
    4.97 +      val _ = cleanup ();
    4.98 +    in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end
    4.99 +    handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn)
   4.100 +  end);
   4.101 +
   4.102 +end;