more direct invocation of Windows exe: avoid extra bash, cygpath, exec;
authorwenzelm
Mon May 27 15:08:51 2019 +0200 (3 months ago)
changeset 70293c7e9d3a0a681
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
     1.1 --- a/Admin/components/components.sha1	Mon May 27 14:25:00 2019 +0200
     1.2 +++ b/Admin/components/components.sha1	Mon May 27 15:08:51 2019 +0200
     1.3 @@ -22,6 +22,7 @@
     1.4  541eac340464c5d34b70bb163ae277cc8829c40f  cvc4-1.5-2.tar.gz
     1.5  1a44895d2a440091a15cc92d7f77a06a2e432507  cvc4-1.5-3.tar.gz
     1.6  c0d8d5929b00e113752d8bf5d11241cd3bccafce  cvc4-1.5-4.tar.gz
     1.7 +ffb0d4739c10eb098eb092baef13eccf94a79bad  cvc4-1.5-5.tar.gz
     1.8  3682476dc5e915cf260764fa5b86f1ebdab57507  cvc4-1.5.tar.gz
     1.9  a5e02b5e990da4275dc5d4480c3b72fc73160c28  cvc4-1.5pre-1.tar.gz
    1.10  4d9658fd2688ae8ac78da8fdfcbf85960f871b71  cvc4-1.5pre-2.tar.gz
    1.11 @@ -302,5 +303,6 @@
    1.12  06b30757ff23aefbc30479785c212685ffd39f4d  z3-4.3.2pre.tar.gz
    1.13  93e7e4bddc6afcf87fe2b6656cfcb1b1acd0a4f8  z3-4.4.0pre-1.tar.gz
    1.14  b1bc411c2083fc01577070b56b94514676f53854  z3-4.4.0pre-2.tar.gz
    1.15 +4c366ab255d2e9343fb635d44d4d55ddd24c76d0  z3-4.4.0pre-3.tar.gz
    1.16  517ba7b94c1985416c5b411c8ae84456367eb231  z3-4.4.0pre.tar.gz
    1.17  aa20745f0b03e606b1a4149598e0c7572b63c657  z3-4.8.3.tar.gz
     2.1 --- a/Admin/components/main	Mon May 27 14:25:00 2019 +0200
     2.2 +++ b/Admin/components/main	Mon May 27 15:08:51 2019 +0200
     2.3 @@ -2,7 +2,7 @@
     2.4  bash_process-1.2.3
     2.5  bib2xhtml-20190409
     2.6  csdp-6.x
     2.7 -cvc4-1.5-4
     2.8 +cvc4-1.5-5
     2.9  e-2.0-2
    2.10  isabelle_fonts-20190409
    2.11  jdk-11.0.3+7
    2.12 @@ -22,4 +22,4 @@
    2.13  stack-1.9.3
    2.14  vampire-4.2.2
    2.15  xz-java-1.8
    2.16 -z3-4.4.0pre-2
    2.17 +z3-4.4.0pre-3
     3.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Mon May 27 14:25:00 2019 +0200
     3.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Mon May 27 15:08:51 2019 +0200
     3.3 @@ -49,7 +49,8 @@
     3.4  local
     3.5  
     3.6  fun make_command command options problem_path proof_path =
     3.7 -  Bash.strings (command () @ options) ^ " " ^ File.bash_path problem_path ^
     3.8 +  Bash.strings (command () @ options) ^ " " ^
     3.9 +    Bash.string (File.platform_path problem_path) ^
    3.10      " > " ^ File.bash_path proof_path ^ " 2>&1"
    3.11  
    3.12  fun with_trace ctxt msg f x =