src/HOL/Library/Sum_of_Squares/neos_csdp_client

simpler proof through custom summation function

#!/usr/bin/env python
import sys
import signal
import xmlrpclib
import time
import re
import os

# Neos server config
neos = xmlrpclib.Server(os.getenv("ISABELLE_NEOS_SERVER"))

jobNumber = 0
password = ""
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)

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()
  xml += buffer
inputfile.close()
xml += xml_post

(jobNumber,password) = neos.submitJob(xml)

if jobNumber == 0:
  sys.stdout.write("error submitting job: %s" % password)
  sys.exit(20)
else:
  sys.stdout.write("jobNumber = %d\tpassword = %s\n" % (jobNumber,password))

offset=0
messages = ""
status="Waiting"
while status == "Running" or status=="Waiting":
  time.sleep(1)
  (msg,offset) = neos.getIntermediateResults(jobNumber,password,offset)
  messages += msg.data
  sys.stdout.write(msg.data)
  status = neos.getJobStatus(jobNumber, password)

msg = neos.getFinalResults(jobNumber, password).data
sys.stdout.write("---------- Begin CSDP Output -------------\n");
sys.stdout.write(msg)

# extract solution
result = msg.split("Solution:")
if len(result) > 1:
  solution = result[1].strip()
  if solution != "":
    outputfile = open(sys.argv[2],"w")
    outputfile.write(solution)
    outputfile.close()

# extract return code
p = re.compile(r"^Error: Command exited with non-zero status (\d+)$", re.MULTILINE)
m = p.search(messages)
if m:
  sys.exit(int(m.group(1)))
else:
  sys.exit(0)