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

PVS Bug 1078


Synopsis:        Problems with X display of proof trees
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Thu Oct 13 18:40:00 -0700 2011
Originator:      Victor Luchangco
Release:         PVS 5.0
Organization:    oracle.com
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  I'm trying to switch from PVS 4.2 to PVS 5.0, and although the changes to the
  proofs themselves have been minimal and straightforward, I'm having some trou
 ble with the "tools" aspects.  In particular, I can't seem to get the X displa
 ys of proof trees (i.e., using x-show-proof and x-show-current-proof).  For ex
 ample, I have a lemma that has been proved (I ran the proof in PVS 5.0), but w
 hen I call x-show-proof on it (plain show-proof works fine), I get the followi
 ng error message:
  
    error in process filter: Symbol's function definition is void: set-process-
 query-on-exit-flag
  
  It also pops up a small window titled pvs, but with nothing inside.
  
  If I call x-show-current-proof while proving a lemma, I get the following err
 or message:
  
    error in process filter: No Tcl process; see variable `inferior-tcl-buffer'
  
  and again, a small empty window titled pvs pops up, but then the prover seems
  wedged, and won't do anything.  I have to quit the proof (but not the prover)
 , and then it seems to work again.
  
  I also get a possibly related error message when I try to change context (i.e
 ., M-x change-context):
  
    Symbol's function definition is void: read-directory-name
  
  These error messages suggest that perhaps I've done something wrong in the se
 t up, but I don't know what.  Everything seems to work fine with PVS 4.2 (thou
 gh of course, it doesn't run with the new .prf files).
  
  I tried on both the SBCL and the CMU Common Lisp versions (32-bit Linux), whi
 ch I just downloaded from the site, and I get the same behavior with both.  (I
  also tried the 64-bit version, but requires /lib64/libc.so, and on my file sy
 stem, that is at /lib/64/libc.so.)  Here's the system information requested:
  
  PVS Version 5.0 - SBCL 1.0.45
  PVS Version 5.0 - CMU Common Lisp 20b (20B Unicode) 
  
  GNU Emacs 21.4.1 (x86_64-redhat-linux-gnu, X toolkit, Xaw3d scroll bars) of <
 date and machine name>
  
  Linux <machine name> 2.6.18-194.el5 #1 SMP <date/time> x86_64 x86_64 x86_64 G
 NU/Linux
  
  I also have a ~/.pvs.lisp file containing a patch I got from you on May 24, 2
 011.
  
  I'd appreciate any help you can give, since I'm excited to exploit some of th
 e new features of PVS 5.0, particularly ProofLite.
  
  - Victor
  

How-To-Repeat: 

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