merged

--- a/src/HOL/Library/Sum_Of_Squares/neos_csdp_client	Tue Aug 11 15:53:13 2009 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/neos_csdp_client	Tue Aug 11 20:40:02 2009 +0200
@@ -1,5 +1,6 @@
 #!/usr/bin/env python
 import sys
+import signal
 import xmlrpclib
 import time
 import re
@@ -8,16 +9,37 @@
 NEOS_HOST="neos.mcs.anl.gov"
 NEOS_PORT=3332
 
-if len(sys.argv) < 3 or len(sys.argv) > 3:
-  sys.stderr.write("Usage: NeosCSDPClient <input_filename> <output_filename>\n")
-  sys.exit(1)
+jobNumber = 0
+password = ""
+neos = None
+inputfile = None
+outputfile = None
+# interrupt handler
+def cleanup(signal, frame):
+  sys.stdout.write("Caught interrupt, cleaning up\n")
+  if jobNumber != 0:
+    neos.killJob(jobNumber, password)
+  if inputfile != None:
+    inputfile.close()
+  if outputfile != None:
+    outputfile.close()
+  sys.exit(21)
+
+signal.signal(signal.SIGHUP, cleanup)
+signal.signal(signal.SIGINT, cleanup)
+signal.signal(signal.SIGQUIT, cleanup)
+signal.signal(signal.SIGTERM, cleanup)
+
+if len(sys.argv) <> 3:
+  sys.stderr.write("Usage: neos_csdp_client <input_filename> <output_filename>\n")
+  sys.exit(19)
 
 neos=xmlrpclib.Server("http://%s:%d" % (NEOS_HOST, NEOS_PORT))
 
-inputfile = open(sys.argv[1],"r")
 xml_pre = "<document>\n<category>sdp</category>\n<solver>csdp</solver>\n<inputMethod>SPARSE_SDPA</inputMethod>\n<dat><![CDATA["
 xml_post = "]]></dat>\n</document>\n"
 xml = xml_pre
+inputfile = open(sys.argv[1],"r")
 buffer = 1
 while buffer:
   buffer = inputfile.read()
@@ -50,9 +72,11 @@
 # extract solution
 result = msg.split("Solution:")
 if len(result) > 1:
-  output = open(sys.argv[2],"w")
-  output.write(result[1].strip())
-  output.close()
+  solution = result[1].strip()
+  if solution != "":
+    output = open(sys.argv[2],"w")
+    output.write(solution)
+    output.close()
 
 # extract return code
 p = re.compile(r"^Error: Command exited with non-zero status (\d+)$", re.MULTILINE)
@@ -62,4 +86,3 @@
 else:
   sys.exit(0)
 
-

--- a/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML	Tue Aug 11 15:53:13 2009 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML	Tue Aug 11 20:40:02 2009 +0200
@@ -11,6 +11,8 @@
 
   val setup: theory -> theory
   val destdir: string ref
+  val get_prover_name: unit -> string
+  val set_prover_name: string -> unit
 end
 
 structure SosWrapper : SOS_WRAPPER=
@@ -24,7 +26,7 @@
 (*** output control ***)
 
 fun debug s = if ! Sos.debugging then Output.writeln s else ()
-val write = Output.priority
+val write = Output.warning
 
 (*** calling provers ***)
 
@@ -104,11 +106,18 @@
 fun find_neos_failure rv =
   case rv of
     20 => (Error, "error submitting job")
-  | 21 => (Error, "no solution")
+  | 21 => (Error, "interrupt")
   |  _ => find_csdp_failure rv
 
 val neos_csdp = ("$ISABELLE_SUM_OF_SQUARES/neos_csdp_client", find_neos_failure)
 
+(* default prover *)
+
+val prover_name = ref "remote_csdp"
+
+fun get_prover_name () = CRITICAL (fn () => ! prover_name);
+fun set_prover_name str = CRITICAL (fn () => prover_name := str);
+
 (* save provers in table *)
 
 val provers =
@@ -119,8 +128,9 @@
     SOME prover => prover
   | NONE => error ("unknown prover: " ^ name)
 
-fun call_solver name =
+fun call_solver name_option =
   let
+    val name = the_default (get_prover_name()) name_option
     val (cmd, find_failure) = get_prover name
   in
     run_solver name (Path.explode cmd) find_failure
@@ -128,11 +138,9 @@
 
 (* setup tactic *)
 
-val def_solver = "remote_csdp"
-
 fun sos_solver name = (SIMPLE_METHOD' o (Sos.sos_tac (call_solver name))) 
 
-val sos_method = Scan.optional (Scan.lift OuterParse.xname) def_solver >> sos_solver
+val sos_method = Scan.option (Scan.lift OuterParse.xname) >> sos_solver
 
 val setup = Method.setup @{binding sos} sos_method
   "Prove universal problems over the reals using sums of squares"