--- a/NEWS Sun Mar 13 16:52:59 2011 +0100
+++ b/NEWS Sun Mar 13 17:28:14 2011 +0100
@@ -21,6 +21,13 @@
The global load path (such as src/HOL/Library) is has been
discontinued. INCOMPATIBILITY.
+* Various optional external tools are referenced more robustly and
+uniformly by explicit Isabelle settings as follows, without automated
+detection from the shell environment or path (potential
+INCOMPATIBILITY):
+
+ ISABELLE_CSDP (formerly CSDP_EXE)
+
*** HOL ***
--- a/etc/settings Sun Mar 13 16:52:59 2011 +0100
+++ b/etc/settings Sun Mar 13 17:28:14 2011 +0100
@@ -238,9 +238,6 @@
# Jerusat 1.3 (SAT Solver, cf. Isabelle/src/HOL/Tools/sat_solver.ML)
#JERUSAT_HOME=/usr/local/bin
-# CSDP (SDP Solver, cf. Isabelle/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML)
-#CSDP_EXE=csdp
-
# For configuring HOL/Matrix/cplex
# LP_SOLVER is the default solver. It can be changed during runtime via Cplex.set_solver.
# First option: use the commercial cplex solver
--- a/src/HOL/Library/Sum_of_Squares.thy Sun Mar 13 16:52:59 2011 +0100
+++ b/src/HOL/Library/Sum_of_Squares.thy Sun Mar 13 17:28:14 2011 +0100
@@ -16,16 +16,26 @@
begin
text {*
- In order to use the method sos, call it with @{text "(sos
- remote_csdp)"} to use the remote solver. Or install CSDP
- (https://projects.coin-or.org/Csdp), configure the Isabelle setting
- @{text CSDP_EXE}, and call it with @{text "(sos csdp)"}. By
- default, sos calls @{text remote_csdp}. This can take of the order
- of a minute for one sos call, because sos calls CSDP repeatedly. If
- you install CSDP locally, sos calls typically takes only a few
- seconds.
- sos generates a certificate which can be used to repeat the proof
- without calling an external prover.
+ Proof method sos invocations:
+ \begin{itemize}
+
+ \item remote solver: @{text "(sos remote_csdp)"}
+
+ \item local solver: @{text "(sos csdp)"}
+
+ The latter requires a local executable from
+ https://projects.coin-or.org/Csdp and the Isabelle settings variable
+ variable @{text ISABELLE_CSDP} pointing to it.
+
+ \end{itemize}
+
+ By default, method sos calls @{text remote_csdp}. This can take of
+ the order of a minute for one sos call, because sos calls CSDP
+ repeatedly. If you install CSDP locally, sos calls typically takes
+ only a few seconds.
+
+ The sos method generates a certificate which can be used to repeat
+ the proof without calling an external prover.
*}
setup Sum_of_Squares.setup
--- a/src/HOL/Library/Sum_of_Squares/etc/settings Sun Mar 13 16:52:59 2011 +0100
+++ b/src/HOL/Library/Sum_of_Squares/etc/settings Sun Mar 13 17:28:14 2011 +0100
@@ -3,3 +3,6 @@
ISABELLE_SUM_OF_SQUARES="$COMPONENT"
ISABELLE_NEOS_SERVER="http://neos-server.org:3332"
+# local SDP Solver, cf. https://projects.coin-or.org/Csdp
+#ISABELLE_CSDP="/usr/local/bin/csdp"
+
--- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Sun Mar 13 16:52:59 2011 +0100
+++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Sun Mar 13 17:28:14 2011 +0100
@@ -38,7 +38,7 @@
else error ("No such directory: " ^ dir)
end
-fun run_solver ctxt name cmd find_failure input =
+fun run_solver ctxt name exe find_failure input =
let
val _ = warning ("Calling solver: " ^ name)
@@ -51,10 +51,9 @@
val output_file = filename dir "sos_out"
val (output, rv) =
bash_output
- (if File.exists cmd then
- space_implode " "
- [File.shell_path cmd, File.shell_path input_file, File.shell_path output_file]
- else error ("Bad executable: " ^ File.platform_path cmd))
+ (if File.exists exe then
+ space_implode " " (map File.shell_path [exe, input_file, output_file])
+ else error ("Bad executable: " ^ File.platform_path exe))
(* read and analyze output *)
val (res, res_msg) = find_failure rv
@@ -98,7 +97,7 @@
| 9 => (Failure, "Detected NaN or Inf values")
| _ => (Error, "return code is " ^ string_of_int rv)
-val csdp = ("$CSDP_EXE", find_csdp_failure)
+val csdp = (Path.explode "$ISABELLE_CSDP", find_csdp_failure)
(* remote neos server *)
@@ -109,7 +108,7 @@
| 21 => (Error, "interrupt")
| _ => find_csdp_failure rv
-val neos_csdp = ("$ISABELLE_SUM_OF_SQUARES/neos_csdp_client", find_neos_failure)
+val neos_csdp = (Path.explode "$ISABELLE_SUM_OF_SQUARES/neos_csdp_client", find_neos_failure)
(* named provers *)
@@ -123,8 +122,8 @@
fun call_solver ctxt opt_name =
let
val name = the_default (Config.get ctxt prover_name) opt_name
- val (cmd, find_failure) = prover name
- in run_solver ctxt name (Path.explode cmd) find_failure end
+ val (exe, find_failure) = prover name
+ in run_solver ctxt name exe find_failure end
(* certificate output *)