new version of MaSh that really honors the --port option and that checks for file name mismatches
authorblanchet
Tue Oct 01 14:40:25 2013 +0200 (2013-10-01)
changeset 54011427b77238746
parent 54010 5ac1495fed4e
child 54012 7a8263843acb
new version of MaSh that really honors the --port option and that checks for file name mismatches
src/HOL/Tools/Sledgehammer/MaSh/src/mash.py
src/HOL/Tools/Sledgehammer/MaSh/src/server.py
src/HOL/Tools/Sledgehammer/MaSh/src/spawnDaemon.py
     1.1 --- a/src/HOL/Tools/Sledgehammer/MaSh/src/mash.py	Tue Oct 01 14:29:27 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/MaSh/src/mash.py	Tue Oct 01 14:40:25 2013 +0200
     1.3 @@ -39,7 +39,7 @@
     1.4      logger = logging.getLogger('start_server')
     1.5      logger.info('Starting Server.')
     1.6      path = dirname(realpath(__file__))
     1.7 -    spawnDaemon(os.path.join(path,'server.py'))
     1.8 +    spawnDaemon(os.path.join(path,'server.py'),os.path.join(path,'server.py'),host,str(port))
     1.9      serverIsUp=False
    1.10      for _i in range(20):
    1.11          # Test if server is up
    1.12 @@ -91,13 +91,17 @@
    1.13  
    1.14      # If server is not running, start it.
    1.15      startedServer = False
    1.16 -    try:
    1.17 -        sock = socket.socket(socket.AF_INET, socket.SOCK_STREAM)
    1.18 -        sock.connect((args.host,args.port))       
    1.19 -        sock.close()
    1.20 -    except:
    1.21 +    received = communicate(' '.join(('ping',args.modelFile,args.dictsFile)),args.host,args.port)
    1.22 +    if received == -1:
    1.23          startedServer = start_server(args.host,args.port)
    1.24 -        
    1.25 +    elif received.startswith('Files do not match'):
    1.26 +        logger.error('Filesnames do not match!')
    1.27 +        logger.error('Modelfile server: '+ received.split()[-2])
    1.28 +        logger.error('Modelfile argument: '+ args.modelFile)
    1.29 +        logger.error('Dictsfile server: '+ received.split()[-1])
    1.30 +        logger.error('Dictsfile argument: '+ args.dictsFile)
    1.31 +        return
    1.32 +    
    1.33      if args.init or startedServer:
    1.34          logger.info('Initializing Server.')
    1.35          data = "i "+";".join(argv)
     2.1 --- a/src/HOL/Tools/Sledgehammer/MaSh/src/server.py	Tue Oct 01 14:29:27 2013 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/MaSh/src/server.py	Tue Oct 01 14:40:25 2013 +0200
     2.3 @@ -5,7 +5,7 @@
     2.4  #
     2.5  # The MaSh Server.
     2.6  
     2.7 -import SocketServer,os,string,logging
     2.8 +import SocketServer,os,string,logging,sys
     2.9  from multiprocessing import Manager
    2.10  from threading import Timer
    2.11  from time import time
    2.12 @@ -167,6 +167,12 @@
    2.13                  self.shutdown()         
    2.14              elif self.data == 'save':
    2.15                  self.server.save()       
    2.16 +            elif self.data.startswith('ping'):
    2.17 +                mFile, dFile = self.data.split()[1:]
    2.18 +                if mFile == self.server.args.modelFile and dFile == self.server.args.dictsFile:
    2.19 +                    self.request.sendall('All good.')
    2.20 +                else:
    2.21 +                    self.request.sendall('Files do not match '+' '.join((self.server.args.modelFile,self.server.args.dictsFile)))
    2.22              elif self.data.startswith('i'):            
    2.23                  self.init(self.data[2:])
    2.24              elif self.data.startswith('!'):
    2.25 @@ -187,9 +193,10 @@
    2.26              self.server.lock.release()
    2.27  
    2.28  if __name__ == "__main__":
    2.29 -    HOST, PORT = "localhost", 9255
    2.30 +    HOST, PORT = sys.argv[1:]    
    2.31 +    #HOST, PORT = "localhost", 9255
    2.32      SocketServer.TCPServer.allow_reuse_address = True
    2.33 -    server = ThreadingTCPServer((HOST, PORT), MaShHandler)
    2.34 +    server = ThreadingTCPServer((HOST, int(PORT)), MaShHandler)
    2.35      server.serve_forever()        
    2.36  
    2.37  
     3.1 --- a/src/HOL/Tools/Sledgehammer/MaSh/src/spawnDaemon.py	Tue Oct 01 14:29:27 2013 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/MaSh/src/spawnDaemon.py	Tue Oct 01 14:40:25 2013 +0200
     3.3 @@ -28,8 +28,9 @@
     3.4          os._exit(0)
     3.5  
     3.6      # and finally let's execute the executable for the daemon!
     3.7 -    try:
     3.8 -        os.execv(path_to_executable, [path_to_executable])
     3.9 +    try:        
    3.10 +        #os.execv(path_to_executable, [path_to_executable])
    3.11 +        os.execv(path_to_executable, args)
    3.12      except Exception, e:
    3.13          # oops, we're cut off from the world, let's just give up
    3.14          os._exit(255)