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

PVS Bug 619


Synopsis:        Import with name change => no proof file
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Tue Nov 27 14:14:35 2001
Originator:      Jerry James
Organization:    eecs.ku.edu
Release:         PVS 2.4
Environment: 
 System:          
 Architecture: 

Description: 
  The documentation for import-pvs-file says:
  
    Import a text file as a PVS file
  
    The import-pvs-file command prompts for a source file and a target file
    and copies the former to the latter, and places the file in the current
    context.  In addition, the corresponding proof file is copied.
  
  This works as advertised if you import to a file of the same name as the
  original.  However, if the file name is changed, only the .pvs file is
  copied; the corresponding proof file is not copied.
  
  This happens in both PVS 2.3 and 2.4, on a RedHat Linux 7.1 machine with
  XEmacs 21.1.14.  It is due to this piece of import-pvs-file
  (pvs-cmds.el):
  
    (let* ((nfile (pvs-file-name name))
  	 (pfile (format "%s%s.prf" (pathname-directory file) name))
  	 (npfile (pvs-file-name name "prf")))
   
  The result is that pfile is set to import-path/newname.prf instead of
  import-path/oldname.prf.  To fix it, modify the code to read:
  
    (let* ((nfile (pvs-file-name name))
  	 (pfile (format "%s%s.prf" (pathname-directory file)
  			(pathname-name file)))
  	 (npfile (pvs-file-name name "prf")))
  
  -- 
  Jerry James
  

How-To-Repeat: 

Fix: 
Fairly obvious fix to import-pvs-file in emacs/emacs-src/pvs-cmds.el
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools