# HG changeset patch # User wenzelm # Date 1633605053 -7200 # Node ID 9333a6ee57ba0b495613eca70a186a8153fc1ef3 # Parent d8015e659e15ce65287f874d0e48c1ba729e4888 proper platform_path for executables run from Java; diff -r d8015e659e15 -r 9333a6ee57ba src/Doc/Nitpick/document/root.tex --- a/src/Doc/Nitpick/document/root.tex Thu Oct 07 13:04:15 2021 +0200 +++ b/src/Doc/Nitpick/document/root.tex Thu Oct 07 13:10:53 2021 +0200 @@ -2196,9 +2196,6 @@ the 2010 SAT Race. To use CryptoMiniSat, set the environment variable \texttt{CRYPTO\-MINISAT\_}\discretionary{}{}{}\texttt{HOME} to the directory that contains the \texttt{crypto\-minisat} executable.% -\footnote{Important note for Cygwin users: The path must be specified using -native Windows syntax. Make sure to escape backslashes properly.% -\label{cygwin-paths}} The \cpp{} sources and executables for Crypto\-Mini\-Sat are available at \url{http://planete.inrialpes.fr/~soos/}\allowbreak\url{CryptoMiniSat2/index.php}. Nitpick has been tested with version 2.51. @@ -2212,7 +2209,6 @@ written in \cpp{}. To use MiniSat, set the environment variable \texttt{MINISAT\_HOME} to the directory that contains the \texttt{minisat} executable.% -\footref{cygwin-paths} The \cpp{} sources and executables for MiniSat are available at \url{http://minisat.se/MiniSat.html}. Nitpick has been tested with versions 1.14 and 2.2. @@ -2226,7 +2222,6 @@ \item[\labelitemi] \textbf{\textit{Riss3g}:} Riss3g is an efficient solver written in \cpp{}. To use Riss3g, set the environment variable \texttt{RISS3G\_HOME} to the directory that contains the \texttt{riss3g} executable.% -\footref{cygwin-paths} The \cpp{} sources for Riss3g are available at \url{http://tools.computational-logic.org/content/riss3g.php}. Nitpick has been tested with the SAT Competition 2013 version. @@ -2234,7 +2229,6 @@ \item[\labelitemi] \textbf{\textit{zChaff}:} zChaff is an older solver written in \cpp{}. To use zChaff, set the environment variable \texttt{ZCHAFF\_HOME} to the directory that contains the \texttt{zchaff} executable.% -\footref{cygwin-paths} The \cpp{} sources and executables for zChaff are available at \url{http://www.princeton.edu/~chaff/zchaff.html}. Nitpick has been tested with versions 2004-05-13, 2004-11-15, and 2007-03-12. @@ -2242,7 +2236,6 @@ \item[\labelitemi] \textbf{\textit{RSat}:} RSat is an efficient solver written in \cpp{}. To use RSat, set the environment variable \texttt{RSAT\_HOME} to the directory that contains the \texttt{rsat} executable.% -\footref{cygwin-paths} The \cpp{} sources for RSat are available at \url{http://reasoning.cs.ucla.edu/rsat/}. Nitpick has been tested with version 2.01. @@ -2250,7 +2243,7 @@ \item[\labelitemi] \textbf{\textit{BerkMin}:} BerkMin561 is an efficient solver written in C. To use BerkMin, set the environment variable \texttt{BERKMIN\_HOME} to the directory that contains the \texttt{BerkMin561} -executable.\footref{cygwin-paths} +executable. The BerkMin executables are available at \url{http://eigold.tripod.com/BerkMin.html}. @@ -2259,7 +2252,6 @@ version of BerkMin, set the environment variable \texttt{BERKMINALLOY\_HOME} to the directory that contains the \texttt{berkmin} executable.% -\footref{cygwin-paths} \item[\labelitemi] \textbf{\textit{SAT4J}:} SAT4J is a reasonably efficient solver written in Java that can be used incrementally. It is bundled with Kodkodi and diff -r d8015e659e15 -r 9333a6ee57ba src/HOL/Tools/Nitpick/kodkod_sat.ML --- a/src/HOL/Tools/Nitpick/kodkod_sat.ML Thu Oct 07 13:04:15 2021 +0200 +++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML Thu Oct 07 13:10:53 2021 +0200 @@ -51,22 +51,19 @@ fun dynamic_entry_for_external name dev home exec args markers = let - fun make_args dir () = + fun make_args () = let val serial_str = serial_string () val base = name ^ serial_str val out_file = base ^ ".out" - val dir_sep = - if String.isSubstring "\\" dir andalso not (String.isSubstring "/" dir) - then "\\" else "/" + val exe = Path.variable home + Path.platform_exe (Path.basic exec) in - [if null markers then "External" else "ExternalV2", - dir ^ dir_sep ^ exec, base ^ ".cnf"] @ - (if null markers then [] - else [if dev = ToFile then out_file else ""]) @ markers @ + [if null markers then "External" else "ExternalV2"] @ + [File.platform_path exe, base ^ ".cnf"] @ + (if null markers then [] else [if dev = ToFile then out_file else ""]) @ markers @ (if dev = ToFile then [out_file] else []) @ args end - in case getenv home of "" => NONE | dir => SOME (name, make_args dir) end + in if getenv home = "" then NONE else SOME (name, make_args) end fun dynamic_entry_for_info incremental (name, Internal (Java, mode, ss)) = if incremental andalso mode = Batch then NONE else SOME (name, K ss)