# HG changeset patch # User wenzelm # Date 1459884212 -7200 # Node ID 4764473c9b8ddaace20ed3fbaba1b5ca02bb3724 # Parent 1cec457e0a0375b7db8db6db679f46e57af4c1a1 back to static conditional compilation -- simplified bootstrap; diff -r 1cec457e0a03 -r 4764473c9b8d lib/scripts/isabelle-platform --- a/lib/scripts/isabelle-platform Tue Apr 05 20:51:37 2016 +0200 +++ b/lib/scripts/isabelle-platform Tue Apr 05 21:23:32 2016 +0200 @@ -4,6 +4,7 @@ # # NOTE: The ML system or JVM may have their own idea about the platform! +ISABELLE_WINDOWS_PREFIX="" ISABELLE_PLATFORM_FAMILY="" ISABELLE_PLATFORM32="" ISABELLE_PLATFORM64="" @@ -11,6 +12,7 @@ case $(uname -s) in Linux) ISABELLE_PLATFORM_FAMILY="linux" + ISABELLE_WINDOWS_PREFIX="." case $(uname -m) in i?86) ISABELLE_PLATFORM32=x86-linux @@ -23,6 +25,7 @@ ;; Darwin) ISABELLE_PLATFORM_FAMILY="macos" + ISABELLE_WINDOWS_PREFIX="." case $(uname -m) in i?86) ISABELLE_PLATFORM32=x86-darwin @@ -38,6 +41,7 @@ ;; CYGWIN_NT*) ISABELLE_PLATFORM_FAMILY="windows" + ISABELLE_WINDOWS_PREFIX="windows" case $(uname -m) in i?86 | x86_64) ISABELLE_PLATFORM32=x86-cygwin diff -r 1cec457e0a03 -r 4764473c9b8d src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Tue Apr 05 20:51:37 2016 +0200 +++ b/src/Pure/ROOT.ML Tue Apr 05 21:23:32 2016 +0200 @@ -279,7 +279,7 @@ use "Proof/extraction.ML"; (*Isabelle system*) -use "System/bash.ML"; +use "System/$ISABELLE_WINDOWS_PREFIX/bash.ML"; use "System/isabelle_system.ML"; diff -r 1cec457e0a03 -r 4764473c9b8d src/Pure/System/bash.ML --- a/src/Pure/System/bash.ML Tue Apr 05 20:51:37 2016 +0200 +++ b/src/Pure/System/bash.ML Tue Apr 05 21:23:32 2016 +0200 @@ -1,7 +1,7 @@ (* Title: Pure/System/bash.ML Author: Makarius -GNU bash processes, with propagation of interrupts. +GNU bash processes, with propagation of interrupts -- POSIX version. *) signature BASH = @@ -9,99 +9,6 @@ val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit} end; -if ML_System.platform_is_windows then ML -\ -structure Bash: BASH = -struct - -val process = uninterruptible (fn restore_attributes => fn script => - let - datatype result = Wait | Signal | Result of int; - val result = Synchronized.var "bash_result" Wait; - - val id = serial_string (); - val script_path = File.tmp_path (Path.basic ("bash_script" ^ id)); - val out_path = File.tmp_path (Path.basic ("bash_out" ^ id)); - val err_path = File.tmp_path (Path.basic ("bash_err" ^ id)); - val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id)); - - fun cleanup_files () = - (try File.rm script_path; - try File.rm out_path; - try File.rm err_path; - try File.rm pid_path); - val _ = cleanup_files (); - - val system_thread = - Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () => - Multithreading.with_attributes Multithreading.private_interrupts (fn _ => - let - val _ = File.write script_path script; - val bash_script = - "bash " ^ File.bash_path script_path ^ - " > " ^ File.bash_path out_path ^ - " 2> " ^ File.bash_path err_path; - val bash_process = getenv_strict "ISABELLE_BASH_PROCESS"; - val rc = - Windows.simpleExecute ("", - quote (ML_System.platform_path bash_process) ^ " " ^ - quote (File.platform_path pid_path) ^ " \"\" bash -c " ^ quote bash_script) - |> Windows.fromStatus |> SysWord.toInt; - val res = if rc = 130 orelse rc = 512 then Signal else Result rc; - in Synchronized.change result (K res) end - handle exn => - (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn))); - - fun read_pid 0 = NONE - | read_pid count = - (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of - NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1)) - | some => some); - - fun terminate NONE = () - | terminate (SOME pid) = - let - fun kill s = - let - val cmd = getenv_strict "CYGWIN_ROOT" ^ "\\bin\\bash.exe"; - val arg = "kill -" ^ s ^ " -" ^ string_of_int pid; - in - OS.Process.isSuccess (Windows.simpleExecute ("", quote cmd ^ " -c " ^ quote arg)) - handle OS.SysErr _ => false - end; - - fun multi_kill count s = - count = 0 orelse - (kill s; kill "0") andalso - (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s); - val _ = - multi_kill 10 "INT" andalso - multi_kill 10 "TERM" andalso - multi_kill 10 "KILL"; - in () end; - - fun cleanup () = - (Standard_Thread.interrupt_unsynchronized system_thread; - cleanup_files ()); - in - let - val _ = - restore_attributes (fn () => - Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) (); - - val out = the_default "" (try File.read out_path); - val err = the_default "" (try File.read err_path); - val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc); - val pid = read_pid 1; - val _ = cleanup (); - in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end - handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn) - end); - -end; -\ -else ML -\ structure Bash: BASH = struct @@ -192,4 +99,3 @@ end); end; -\; diff -r 1cec457e0a03 -r 4764473c9b8d src/Pure/System/windows/bash.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/System/windows/bash.ML Tue Apr 05 21:23:32 2016 +0200 @@ -0,0 +1,99 @@ +(* Title: Pure/System/windows/bash.ML + Author: Makarius + +GNU bash processes, with propagation of interrupts -- Windows version. +*) + +signature BASH = +sig + val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit} +end; + +structure Bash: BASH = +struct + +val process = uninterruptible (fn restore_attributes => fn script => + let + datatype result = Wait | Signal | Result of int; + val result = Synchronized.var "bash_result" Wait; + + val id = serial_string (); + val script_path = File.tmp_path (Path.basic ("bash_script" ^ id)); + val out_path = File.tmp_path (Path.basic ("bash_out" ^ id)); + val err_path = File.tmp_path (Path.basic ("bash_err" ^ id)); + val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id)); + + fun cleanup_files () = + (try File.rm script_path; + try File.rm out_path; + try File.rm err_path; + try File.rm pid_path); + val _ = cleanup_files (); + + val system_thread = + Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () => + Multithreading.with_attributes Multithreading.private_interrupts (fn _ => + let + val _ = File.write script_path script; + val bash_script = + "bash " ^ File.bash_path script_path ^ + " > " ^ File.bash_path out_path ^ + " 2> " ^ File.bash_path err_path; + val bash_process = getenv_strict "ISABELLE_BASH_PROCESS"; + val rc = + Windows.simpleExecute ("", + quote (ML_System.platform_path bash_process) ^ " " ^ + quote (File.platform_path pid_path) ^ " \"\" bash -c " ^ quote bash_script) + |> Windows.fromStatus |> SysWord.toInt; + val res = if rc = 130 orelse rc = 512 then Signal else Result rc; + in Synchronized.change result (K res) end + handle exn => + (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn))); + + fun read_pid 0 = NONE + | read_pid count = + (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of + NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1)) + | some => some); + + fun terminate NONE = () + | terminate (SOME pid) = + let + fun kill s = + let + val cmd = getenv_strict "CYGWIN_ROOT" ^ "\\bin\\bash.exe"; + val arg = "kill -" ^ s ^ " -" ^ string_of_int pid; + in + OS.Process.isSuccess (Windows.simpleExecute ("", quote cmd ^ " -c " ^ quote arg)) + handle OS.SysErr _ => false + end; + + fun multi_kill count s = + count = 0 orelse + (kill s; kill "0") andalso + (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s); + val _ = + multi_kill 10 "INT" andalso + multi_kill 10 "TERM" andalso + multi_kill 10 "KILL"; + in () end; + + fun cleanup () = + (Standard_Thread.interrupt_unsynchronized system_thread; + cleanup_files ()); + in + let + val _ = + restore_attributes (fn () => + Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) (); + + val out = the_default "" (try File.read out_path); + val err = the_default "" (try File.read err_path); + val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc); + val pid = read_pid 1; + val _ = cleanup (); + in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end + handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn) + end); + +end;