# HG changeset patch
# User wenzelm
# Date 1300033694 -3600
# Node ID 134131d519c00912696d428e85f7a29adda2df98
# Parent  f9a2e10c49cb53e022d4ce828eeac8805d73804a
clarified ISABELLE_CSDP setting (formerly CSDP_EXE);

diff -r f9a2e10c49cb -r 134131d519c0 NEWS
--- 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 ***
 
diff -r f9a2e10c49cb -r 134131d519c0 etc/settings
--- 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
diff -r f9a2e10c49cb -r 134131d519c0 src/HOL/Library/Sum_of_Squares.thy
--- 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
diff -r f9a2e10c49cb -r 134131d519c0 src/HOL/Library/Sum_of_Squares/etc/settings
--- 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"
+
diff -r f9a2e10c49cb -r 134131d519c0 src/HOL/Library/Sum_of_Squares/sos_wrapper.ML
--- 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 *)