# HG changeset patch # User wenzelm # Date 1440014973 -7200 # Node ID 213bae1c075700902ad15c3345c6084ed9d281a4 # Parent 6a6f15d8fbc49acc612c9c2f1da77fbc5dd8bc61# Parent fb3a641bc914ffe1b636ea18cd72267567d398c2 merged diff -r 6a6f15d8fbc4 -r 213bae1c0757 Admin/polyml/INSTALL-MinGW --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/polyml/INSTALL-MinGW Wed Aug 19 22:09:33 2015 +0200 @@ -0,0 +1,29 @@ +MinGW for native Windows support +================================ + +- always "Run as administrator ..." + +- http://sourceforge.net/projects/msys2 + + target c:\msys32 or c:\msys64 + +- http://sourceforge.net/projects/mingw-w64 + + mingw-w64-install.exe + + i686-4.9.3-win32-dwarf-rt_v4-rev0 + + target c:\msys32 or c:\msys64 + +- within msys shell: + + pacman --needed -Sy bash pacman pacman-mirrors msys2-runtime + + after restart of msys shell: + + pacman -Su + pacman -S make diffutils texinfo gmp-devel mingw-w64-i686-gmp + +- build (as regular user) e.g. on vmbroy9 + + isabelle/repos/Admin/polyml/build polyml-git x86-windows --build=i686-pc-msys --with-gmp diff -r 6a6f15d8fbc4 -r 213bae1c0757 Admin/polyml/build --- a/Admin/polyml/build Wed Aug 19 19:18:19 2015 +0100 +++ b/Admin/polyml/build Wed Aug 19 22:09:33 2015 +0200 @@ -96,7 +96,7 @@ peflags -x8192000 -z500 "$TARGET/poly.exe" ;; x86-windows) - for X in libgcc_s_dw2-1.dll libgmp-10.dll libstdc++-6.dll libwinpthread-1.dll + for X in libgcc_s_dw2-1.dll libgmp-10.dll libstdc++-6.dll do cp "/mingw32/bin/$X" "$TARGET/." done diff -r 6a6f15d8fbc4 -r 213bae1c0757 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Wed Aug 19 19:18:19 2015 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Wed Aug 19 22:09:33 2015 +0200 @@ -167,7 +167,11 @@ SOME var => let val pref = getenv var ^ "/" - val paths = map (Path.explode o prefix pref) (snd exec) + val paths = + map (Path.explode o prefix pref) + (if ML_System.platform_is_windows then + map (suffix ".exe") (snd exec) @ snd exec + else snd exec); in (case find_first File.exists paths of SOME path => path diff -r 6a6f15d8fbc4 -r 213bae1c0757 src/Pure/Concurrent/bash.ML --- a/src/Pure/Concurrent/bash.ML Wed Aug 19 19:18:19 2015 +0100 +++ b/src/Pure/Concurrent/bash.ML Wed Aug 19 22:09:33 2015 +0200 @@ -1,7 +1,7 @@ (* Title: Pure/Concurrent/bash.ML Author: Makarius -GNU bash processes, with propagation of interrupts. +GNU bash processes, with propagation of interrupts -- POSIX version. *) signature BASH = @@ -67,18 +67,15 @@ fun terminate NONE = () | terminate (SOME pid) = let - val sig_test = Posix.Signal.fromWord 0w0; - - fun kill_group pid s = + fun kill s = (Posix.Process.kill (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)), s); true) handle OS.SysErr _ => false; - fun kill s = (kill_group pid s; kill_group pid sig_test); - fun multi_kill count s = count = 0 orelse - kill s andalso (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s); + (kill s; kill (Posix.Signal.fromWord 0w0)) andalso + (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s); val _ = multi_kill 10 Posix.Signal.int andalso multi_kill 10 Posix.Signal.term andalso diff -r 6a6f15d8fbc4 -r 213bae1c0757 src/Pure/Concurrent/bash_windows.ML --- a/src/Pure/Concurrent/bash_windows.ML Wed Aug 19 19:18:19 2015 +0100 +++ b/src/Pure/Concurrent/bash_windows.ML Wed Aug 19 22:09:33 2015 +0200 @@ -1,7 +1,7 @@ -(* Title: Pure/Concurrent/bash.ML +(* Title: Pure/Concurrent/bash_windows.ML Author: Makarius -GNU bash processes, with propagation of interrupts -- on native Windows (MinGW). +GNU bash processes, with propagation of interrupts -- Windows version. *) signature BASH = @@ -12,6 +12,83 @@ structure Bash: BASH = struct -fun process _ = raise Fail "FIXME"; +fun cygwin_bash arg = + let val cmd = getenv_strict "CYGWIN_ROOT" ^ "\\bin\\bash.exe" + in Windows.simpleExecute (cmd, quote cmd ^ " -c " ^ quote arg) end; + +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 = + Simple_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 rc = + cygwin_bash + ("echo $$ > " ^ File.shell_path pid_path ^ "; exec bash " ^ + File.shell_path script_path ^ + " > " ^ File.shell_path out_path ^ + " 2> " ^ File.shell_path err_path) + |> 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); 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 = + OS.Process.isSuccess (cygwin_bash ("kill -" ^ s ^ " -" ^ string_of_int pid)) + handle OS.SysErr _ => false; + 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 () = + (Simple_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 (); reraise exn) + end); end; diff -r 6a6f15d8fbc4 -r 213bae1c0757 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Wed Aug 19 19:18:19 2015 +0100 +++ b/src/Pure/Thy/thy_info.ML Wed Aug 19 22:09:33 2015 +0200 @@ -291,7 +291,8 @@ val name = Path.implode (Path.base path); val node_name = File.full_path dir (Resources.thy_path path); fun check_entry (Task (node_name', _, _)) = - if node_name = node_name' then () + if op = (apply2 File.platform_path (node_name, node_name')) + then () else error ("Incoherent imports for theory " ^ quote name ^ Position.here require_pos ^ ":\n" ^