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

PVS Bug 939


Synopsis:        Cannot edit proofs with 3.3 release candidate
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           open
Class:           sw-bug
Arrival-Date:    Tue Jan 24 11:40:01 2006
Originator:      Jerry James
Organization:    usu.edu
Release:         PVS 3.3 release candidate
Environment: 
 System:          
 Architecture: 

Description: 
  
  --=-PgZ2xvwP/Rls6W+fPkTZ
  Content-Type: text/plain
  Content-Transfer-Encoding: quoted-printable
  
  With the PVS 3.3 release candidate, I cannot edit proofs successfully on
  a Fedora Core 4 machine.  When I ask to edit a proof, I am shown the
  proof in an Emacs buffer, which I can then edit.  When I attempt to
  install the proof, I am asked if I want to run it.  If I say yes, then I
  am shown the theorem statement, but no proof steps are taken.  M-x
  show-current-proof says only (postpone).  Asking about all proofs for
  the theorem shows that even the original proof is gone.
  
  Regards,
  --=20
  Jerry James, Assistant Professor    Email: Jerry.James@usu.edu
  Computer Science Dept.              Web: http://www.cs.usu.edu/~jerry/
  Utah State University
  
  --=-PgZ2xvwP/Rls6W+fPkTZ
  Content-Type: application/pgp-signature; name=signature.asc
  Content-Description: This is a digitally signed message part
  
  -----BEGIN PGP SIGNATURE-----
  Version: GnuPG v1.4.1 (GNU/Linux)
  
  iD8DBQBDzXKtdXqtoXjUyRoRAv0gAJ9slUC46dvclHHQtFRoGwIEMWdAWACffr61
  5Jbb7PfqkCd5cbehHaxqeNc=
  =Saza
  -----END PGP SIGNATURE-----
  
  --=-PgZ2xvwP/Rls6W+fPkTZ--

How-To-Repeat: 

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