new version of MaSh program, with proper shutdown

--- a/src/HOL/Tools/Sledgehammer/MaSh/src/ExpandFeatures.py	Sun Sep 22 21:04:53 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/ExpandFeatures.py	Mon Sep 23 09:08:07 2013 +0200
@@ -5,7 +5,7 @@
 '''
 
 from math import log
-from gensim import corpora, models, similarities
+#from gensim import corpora, models, similarities
 
 class ExpandFeatures(object):
 
@@ -16,7 +16,7 @@
         self.featureCounts = {}
         self.counter = 0        
         self.corpus = []
-        self.LSIModel = models.lsimodel.LsiModel(self.corpus,num_topics=500)
+#        self.LSIModel = models.lsimodel.LsiModel(self.corpus,num_topics=500)
 
     def initialize(self,dicts):
         self.dicts = dicts
@@ -79,9 +79,9 @@
         #print features.keys()        
         #tfidfcorpus = [tfidfmodel[x] for x in self.corpus]
         #newFeatures = LSI[[(x,1) for x in features.keys()]]
-        newFeatures = self.LSIModel[[(x,1) for x in features.keys()]]
-        print features
-        print newFeatures
+        #newFeatures = self.LSIModel[[(x,1) for x in features.keys()]]
+        #print features
+        #print newFeatures
         #print newFeatures
         
         """
@@ -154,7 +154,8 @@
         """
         #print 'fold',len(features)
         #print 'fnew',len(newFeatures)
-        return dict(newFeatures)
+        #return dict(newFeatures)
+        return features
 
 if __name__ == "__main__":
     pass

--- a/src/HOL/Tools/Sledgehammer/MaSh/src/mash.py	Sun Sep 22 21:04:53 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/mash.py	Mon Sep 23 09:08:07 2013 +0200
@@ -81,9 +81,10 @@
 
     # Shutdown commands need not start the server fist.
     if args.shutdownServer:
-        logger.info('Shutting down server.')
+        logger.info('Sending shutdown command.')
         try:
-            communicate('shutdown',args.host,args.port)
+            received = communicate('shutdown',args.host,args.port)
+            logger.info(received)
         except:
             pass
         return

--- a/src/HOL/Tools/Sledgehammer/MaSh/src/server.py	Sun Sep 22 21:04:53 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/server.py	Mon Sep 23 09:08:07 2013 +0200
@@ -15,7 +15,7 @@
 from KNN import KNN,euclidean
 from KNNs import KNNAdaptPointFeatures,KNNUrban
 from predefined import Predefined
-#from ExpandFeatures import ExpandFeatures
+from ExpandFeatures import ExpandFeatures
 from stats import Statistics
 
 
@@ -36,7 +36,7 @@
             statsFile = os.path.join(self.args.outputDir,self.args.saveStats)
             self.stats.save(statsFile)   
                
-    def save_and_shutdown(self):     
+    def save_and_shutdown(self): 
         self.save()          
         self.shutdown()
 
@@ -64,9 +64,9 @@
             self.server.model = Predefined(self.server.args.predef)
         else: # Default case
             self.server.model = sparseNBClassifier(self.server.args.NBDefaultPriorWeight,self.server.args.NBPosWeight,self.server.args.NBDefVal)
-#        if self.server.args.expandFeatures:
-#            self.server.expandFeatures = ExpandFeatures(self.server.dicts)
-#            self.server.expandFeatures.initialize(self.server.dicts)
+        if self.server.args.expandFeatures:
+            self.server.expandFeatures = ExpandFeatures(self.server.dicts)
+            self.server.expandFeatures.initialize(self.server.dicts)
         # Create Model
         if os.path.isfile(self.server.args.modelFile):
             self.server.model.load(self.server.args.modelFile)          
@@ -104,8 +104,8 @@
                 self.server.logger.debug('Poor predictions: %s',bp)
             self.server.statementCounter += 1
 
-#        if self.server.args.expandFeatures:
-#            self.server.expandFeatures.update(self.server.dicts.featureDict[problemId],self.server.dicts.dependenciesDict[problemId])
+        if self.server.args.expandFeatures:
+            self.server.expandFeatures.update(self.server.dicts.featureDict[problemId],self.server.dicts.dependenciesDict[problemId])
         # Update Dependencies, p proves p
         self.server.dicts.dependenciesDict[problemId] = [problemId]+self.server.dicts.dependenciesDict[problemId]
         self.server.model.update(problemId,self.server.dicts.featureDict[problemId],self.server.dicts.dependenciesDict[problemId])
@@ -126,8 +126,8 @@
             numberOfPredictions = self.server.args.numberOfPredictions
         if not hints == []:
             self.server.model.update('hints',features,hints)
-#        if self.server.args.expandFeatures:
-#            features = self.server.expandFeatures.expand(features)
+        if self.server.args.expandFeatures:
+            features = self.server.expandFeatures.expand(features)
         # Create predictions
         self.server.logger.debug('Starting computation for line %s',self.server.callCounter)
                 
@@ -148,12 +148,19 @@
         self.request.sendall('Shutting down server.')
         if saveModels:
             self.server.save()
-        self.server.shutdown()
-    
+        self.server.idle_timer.cancel()
+        self.server.idle_timer = Timer(0.5, self.server.shutdown)
+        self.server.idle_timer.start()    
+
     def handle(self):
         # self.request is the TCP socket connected to the client
         self.data = self.request.recv(4194304).strip()
         self.server.lock.acquire()
+        # Update idle shutdown timer
+        self.server.idle_timer.cancel()
+        self.server.idle_timer = Timer(self.server.idle_timeout, self.server.save_and_shutdown)
+        self.server.idle_timer.start()        
+
         self.startTime = time()  
         if self.data == 'shutdown':
             self.shutdown()         
@@ -176,23 +183,15 @@
         else:
             self.request.sendall('Unspecified input format: \n%s',self.data)
         self.server.callCounter += 1
-        # Update idle shutdown timer
-        self.server.idle_timer.cancel()
-        self.server.idle_timer = Timer(self.server.idle_timeout, self.server.save_and_shutdown)
-        self.server.idle_timer.start()        
         self.server.lock.release()
 
 if __name__ == "__main__":
     HOST, PORT = "localhost", 9255
     SocketServer.TCPServer.allow_reuse_address = True
     server = ThreadingTCPServer((HOST, PORT), MaShHandler)
-
-    # Activate the server; this will keep running until you
-    # interrupt the program with Ctrl-C
     server.serve_forever()        
 
 
-
     
     
-    
+    
\ No newline at end of file