# 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 \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 \n") + sys.exit(19) neos=xmlrpclib.Server("http://%s:%d" % (NEOS_HOST, NEOS_PORT)) -inputfile = open(sys.argv[1],"r") xml_pre = "\nsdp\ncsdp\nSPARSE_SDPA\n\n\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)