# HG changeset patch
# User Philipp Meyer
# Date 1249902125 -7200
# Node ID c0c640d86b4e6d5481b6761c5ec91f3fe026d4c2
# Parent  e88b295aae351f732d56b51105b347d7dfc0d8d5
interrupt handler for neos csdp client

diff -r e88b295aae35 -r c0c640d86b4e src/HOL/Library/Sum_Of_Squares/neos_csdp_client
--- a/src/HOL/Library/Sum_Of_Squares/neos_csdp_client	Sat Aug 08 11:40:22 2009 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/neos_csdp_client	Mon Aug 10 13:02:05 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)
 
-
diff -r e88b295aae35 -r c0c640d86b4e src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML
--- a/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML	Sat Aug 08 11:40:22 2009 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML	Mon Aug 10 13:02:05 2009 +0200
@@ -104,7 +104,7 @@
 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)