Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

PVS Bug 506


Synopsis:        reset-pvs confuses PVS
Severity:        serious
Priority:        medium
Responsible:     dave_sc (Dave Stringer-Calvert)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Mon Jan  8 04:00:02 2001
Originator:      Hendrik Tews
Organization:    inf.tu-dresden.de
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  when I do M-x reset-pvs in the middle of a proof the emacs
  interface disables all proof commands because "No proof is
  currently running", but the prover does not exit on reset-pvs.
  
  I use PVS PVS Version 2.3 (patch level 1.2.2.120) with GNU Emacs
  20.7.2 (i386-debian-linux-gnu, X toolkit) of Tue Jun 20 2000 on
  raven on Debian Linux 2.2.18.
  
  Bye,
  
  Hendrik
  

How-To-Repeat: 

Fix: 

 [davesc]
 Improved the synchronization between Emacs and the underlying
 lisp image so that Lisp has time to respond to the (quit) before
 issuing the interrupt.

Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools