Merge pull request #6 from ApolloLiZhaoyu/master

Fix a small bug when there are shelved_goals and given_up_goals.

eval_env.py

@@ -72,7 +72,7 @@ def step(self, command):
                 self.num_tactics_left -= 1
                 command = 'timeout %d (%s).' % (time_left, command[:-1])
             responses, _ = self.serapi.execute(command)
-            self.serapi.pull()  # delete the saved state if no error
+            states_cnt = self.serapi.pull()  # delete the saved state if no error
         except CoqExn as ex: 
             self.serapi.pop()  # restore the state
             return self.feedback('ERROR', error=ex)
@@ -97,7 +97,7 @@ def step(self, command):
             self.success = True
             return self.feedback('SUCCESS')
         elif shelved_goals + given_up_goals != []:
-            self.serapi.pop()
+            self.serapi.pop_n(states_cnt)
             return self.feedback('ERROR', error=(shelved_goals, given_up_goals))
         else:
             return self.feedback('PROVING', fg_goals=fg_goals, bg_goals=bg_goals, 

serapi.py

@@ -358,13 +358,21 @@ def pull(self):
         'remove a checkpoint created by push'
         states = self.states_stack.pop()
         self.states_stack[-1].extend(states)
+        return len(states)
 
 
     def pop(self):
         'rollback to a checkpoint created by push'
         self.cancel(self.states_stack.pop())
 
 
+    def pop_n(self, cnt):
+        states = []
+        for i in range(cnt):
+            states.append(self.states_stack[-1].pop())
+        self.cancel(states)
+
+
     def clean(self):
         self.proc.sendeof()
         self.proc.wait()