# HG changeset patch # User wenzelm # Date 1460057943 -7200 # Node ID 78e03d8bf1c4d85178924e26687b02c3dc2067c5 # Parent f37878ebba65d6c852246b75a104bccabc9ae72a back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space; diff -r f37878ebba65 -r 78e03d8bf1c4 lib/scripts/isabelle-platform --- a/lib/scripts/isabelle-platform Thu Apr 07 21:27:17 2016 +0200 +++ b/lib/scripts/isabelle-platform Thu Apr 07 21:39:03 2016 +0200 @@ -4,7 +4,6 @@ # # NOTE: The ML system or JVM may have their own idea about the platform! -ISABELLE_WINDOWS_PREFIX="" ISABELLE_PLATFORM_FAMILY="" ISABELLE_PLATFORM32="" ISABELLE_PLATFORM64="" @@ -12,7 +11,6 @@ case $(uname -s) in Linux) ISABELLE_PLATFORM_FAMILY="linux" - ISABELLE_WINDOWS_PREFIX="." case $(uname -m) in i?86) ISABELLE_PLATFORM32=x86-linux @@ -25,7 +23,6 @@ ;; Darwin) ISABELLE_PLATFORM_FAMILY="macos" - ISABELLE_WINDOWS_PREFIX="." case $(uname -m) in i?86) ISABELLE_PLATFORM32=x86-darwin @@ -41,7 +38,6 @@ ;; CYGWIN_NT*) ISABELLE_PLATFORM_FAMILY="windows" - ISABELLE_WINDOWS_PREFIX="windows" case $(uname -m) in i?86 | x86_64) ISABELLE_PLATFORM32=x86-cygwin diff -r f37878ebba65 -r 78e03d8bf1c4 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Thu Apr 07 21:27:17 2016 +0200 +++ b/src/Pure/ROOT.ML Thu Apr 07 21:39:03 2016 +0200 @@ -273,7 +273,7 @@ ML_file "Proof/extraction.ML"; (*Isabelle system*) -ML_file "System/$ISABELLE_WINDOWS_PREFIX/bash.ML"; +ML_file "System/bash.ML"; ML_file "System/isabelle_system.ML"; diff -r f37878ebba65 -r 78e03d8bf1c4 src/Pure/System/bash.ML --- a/src/Pure/System/bash.ML Thu Apr 07 21:27:17 2016 +0200 +++ b/src/Pure/System/bash.ML Thu Apr 07 21:39:03 2016 +0200 @@ -9,6 +9,99 @@ 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 = Multithreading.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 @@ -99,3 +192,4 @@ end); end; +\ \ No newline at end of file diff -r f37878ebba65 -r 78e03d8bf1c4 src/Pure/System/windows/bash.ML --- a/src/Pure/System/windows/bash.ML Thu Apr 07 21:27:17 2016 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,99 +0,0 @@ -(* 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 = Multithreading.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;