handle huge MaSh requests gracefully
authorblanchet
Tue Oct 08 20:53:37 2013 +0200 (2013-10-08 ago)
changeset 54079cb33b304e743
parent 54078 1d371c3f2703
child 54080 540835cf11ed
handle huge MaSh requests gracefully
src/HOL/Tools/Sledgehammer/MaSh/src/mash.py
src/HOL/Tools/Sledgehammer/MaSh/src/server.py
     1.1 --- a/src/HOL/Tools/Sledgehammer/MaSh/src/mash.py	Tue Oct 08 16:40:03 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/MaSh/src/mash.py	Tue Oct 08 20:53:37 2013 +0200
     1.3 @@ -26,7 +26,19 @@
     1.4      try:
     1.5          sock.connect((host,port))
     1.6          sock.sendall(data)
     1.7 -        received = sock.recv(4194304)
     1.8 +        received = ''
     1.9 +        cont = True
    1.10 +        counter = 0
    1.11 +        while cont and counter < 100000:
    1.12 +            rec = sock.recv(4096)
    1.13 +            if rec == 'stop':
    1.14 +                cont = False
    1.15 +            elif rec.endswith('stop'):
    1.16 +                cont = False
    1.17 +                received += rec[:-4]
    1.18 +            else:
    1.19 +                received += rec
    1.20 +            counter += 1
    1.21      except:
    1.22          logger = logging.getLogger('communicate')
    1.23          logger.warning('Communication with server failed.')
     2.1 --- a/src/HOL/Tools/Sledgehammer/MaSh/src/server.py	Tue Oct 08 16:40:03 2013 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/MaSh/src/server.py	Tue Oct 08 20:53:37 2013 +0200
     2.3 @@ -150,7 +150,7 @@
     2.4          #predictionValues = [str(x) for x in predictionValues[:numberOfPredictions]]
     2.5          #predictionsStringList = ['%s=%s' % (predictionNames[i],predictionValues[i]) for i in range(len(predictionNames))]
     2.6          #predictionsString = string.join(predictionsStringList,' ')
     2.7 -        predictionsString = string.join(predictionNames,' ')
     2.8 +        predictionsString = string.join(predictionNames,' ')        
     2.9          outString = '%s: %s' % (name,predictionsString)
    2.10          self.request.sendall(outString)
    2.11      
    2.12 @@ -164,7 +164,7 @@
    2.13  
    2.14      def handle(self):
    2.15          # self.request is the TCP socket connected to the client
    2.16 -        self.data = self.request.recv(4194304).strip()
    2.17 +        self.data = self.request.recv(134217728).strip()
    2.18          self.server.lock.acquire()
    2.19          try:
    2.20              # Update idle shutdown timer
    2.21 @@ -199,6 +199,7 @@
    2.22              else:
    2.23                  self.request.sendall('Unspecified input format: \n%s',self.data)
    2.24              self.server.callCounter += 1
    2.25 +            self.request.sendall('stop')
    2.26          finally:
    2.27              self.server.lock.release()
    2.28