--- /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
--- 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
--- 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
--- 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
--- 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;
--- 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" ^