more direct invocation of Windows exe: avoid extra bash, cygpath, exec;
authorwenzelm
Mon, 27 May 2019 15:08:51 +0200
changeset 70293 c7e9d3a0a681
parent 70292 bc9d02f916c4
child 70294 742f8e703780
child 70297 67edf0234417
more direct invocation of Windows exe: avoid extra bash, cygpath, exec;
Admin/components/components.sha1
Admin/components/main
src/HOL/Tools/SMT/smt_solver.ML
--- a/Admin/components/components.sha1	Mon May 27 14:25:00 2019 +0200
+++ b/Admin/components/components.sha1	Mon May 27 15:08:51 2019 +0200
@@ -22,6 +22,7 @@
 541eac340464c5d34b70bb163ae277cc8829c40f  cvc4-1.5-2.tar.gz
 1a44895d2a440091a15cc92d7f77a06a2e432507  cvc4-1.5-3.tar.gz
 c0d8d5929b00e113752d8bf5d11241cd3bccafce  cvc4-1.5-4.tar.gz
+ffb0d4739c10eb098eb092baef13eccf94a79bad  cvc4-1.5-5.tar.gz
 3682476dc5e915cf260764fa5b86f1ebdab57507  cvc4-1.5.tar.gz
 a5e02b5e990da4275dc5d4480c3b72fc73160c28  cvc4-1.5pre-1.tar.gz
 4d9658fd2688ae8ac78da8fdfcbf85960f871b71  cvc4-1.5pre-2.tar.gz
@@ -302,5 +303,6 @@
 06b30757ff23aefbc30479785c212685ffd39f4d  z3-4.3.2pre.tar.gz
 93e7e4bddc6afcf87fe2b6656cfcb1b1acd0a4f8  z3-4.4.0pre-1.tar.gz
 b1bc411c2083fc01577070b56b94514676f53854  z3-4.4.0pre-2.tar.gz
+4c366ab255d2e9343fb635d44d4d55ddd24c76d0  z3-4.4.0pre-3.tar.gz
 517ba7b94c1985416c5b411c8ae84456367eb231  z3-4.4.0pre.tar.gz
 aa20745f0b03e606b1a4149598e0c7572b63c657  z3-4.8.3.tar.gz
--- a/Admin/components/main	Mon May 27 14:25:00 2019 +0200
+++ b/Admin/components/main	Mon May 27 15:08:51 2019 +0200
@@ -2,7 +2,7 @@
 bash_process-1.2.3
 bib2xhtml-20190409
 csdp-6.x
-cvc4-1.5-4
+cvc4-1.5-5
 e-2.0-2
 isabelle_fonts-20190409
 jdk-11.0.3+7
@@ -22,4 +22,4 @@
 stack-1.9.3
 vampire-4.2.2
 xz-java-1.8
-z3-4.4.0pre-2
+z3-4.4.0pre-3
--- a/src/HOL/Tools/SMT/smt_solver.ML	Mon May 27 14:25:00 2019 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Mon May 27 15:08:51 2019 +0200
@@ -49,7 +49,8 @@
 local
 
 fun make_command command options problem_path proof_path =
-  Bash.strings (command () @ options) ^ " " ^ File.bash_path problem_path ^
+  Bash.strings (command () @ options) ^ " " ^
+    Bash.string (File.platform_path problem_path) ^
     " > " ^ File.bash_path proof_path ^ " 2>&1"
 
 fun with_trace ctxt msg f x =