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

PVS Bug 729


Synopsis:        emacs is busy-waiting for allegro lisp
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           open
Class:           sw-bug
Arrival-Date:    Wed Jan 15 10:30:00 2003
Originator:      Hendrik Tews
Organization:    tcs.inf.tu-dresden.de
Release:         PVS 3.0
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  I have the impression that (in cirtain circumstances) emacs does
  busy-waiting for the background process.
  
  Consider for instance edit-proof on Lemma DIVREM_eq in
  BitvectorTwoComplementDivisionWidenNarrow.pvs in the bitvectors
  library. In a fresh PVS just edit-proof on that lemma takes 18
  seconds on my system (where emacs eats up half of the time, even
  when PVS is garbadge collecting). When I first typecheck and
  issue edit-proof afterwards it only takes 12 seconds.
  
  Commands that invoke the prover (eg. prove) suffer from the same
  problem. 
  
  I tested this on PVS 3.0.
  
  Bye,
  
  Hendrik

How-To-Repeat: 

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