Description of problem: The method of creating a new proof buffer does not work in emacs. However, it does seem to work in xemacs. Version-Release number of selected component (if applicable): pvs-sbcl-4.2-2.20100104svn.fc12 Steps to Reproduce: 1. Start pvs-sbcl, use "pvs-sbcl -emacs emacs" to ensure that it runs with emacs if both xemacs and emacs are available. 2. Try to create a new buffer: Pressing C-x C-f and typing a file name in the minibuffer that does not yet exist. Actual results: Emacs puts "(No match)" by the file and exits the minibuffer. Expected results: Emacs should create a new buffer with the expected file name, as occurs in xemacs. Additional info: One can work around this by creating files outside of emacs and merely opening them.
I'm not sure what causes the difference in behavior, but note that M-x new-pvs-file is the preferred method. In fact, even though C-x C-f "works" with XEmacs, I'm not sure the new file is added to the theory context.
(In reply to comment #1) > I'm not sure what causes the difference in behavior, but note that M-x > new-pvs-file is the preferred method. In fact, even though C-x C-f "works" > with XEmacs, I'm not sure the new file is added to the theory context. Noted, though I was just going off of the documentation from http://pvs.csl.sri.com/documentation.shtml, which (in "pvs-system-guide") suggested that the two were equally fine. Being a frequent emacs user, I actually just forgot that the other one existed because C-x C-f is so familiar, and the result was surprising. If there's some more updated documentation (the latest version I found in the source tarball for 4.2 seemed to refer to version 3) that might correct my other subtle mistakes, that would potentially also be nice to have in a separate subpackage.
I'll look into the C-x C-f failure. And, no, I'm afraid you have the latest, greatest documentation already in the package. Maybe the M-x new-pvs-file approach is just *my* favored approach because it inserts a template into the buffer. My brain works that way...
I looked into this a little. C-x C-f is bound to find-file in both editors. In XEmacs, find-file calls completing-read with a 4th argument (require-match) of nil, which means "accept any input", which is why it works in that editor. In Emacs, find-file calls completing-read with a 4th argument of 'confirm-after-completion. The confirmation call is bound to (completer-exit) by the ilisp code shipped with PVS, which fails if you don't have an exact match with something that already exists. Unfortunately, I'm still not sure how to fix this. I'll try a few things and see how they explode. :-)
pvs-sbcl-4.2-2.20100126svn.fc12 has been submitted as an update for Fedora 12. http://admin.fedoraproject.org/updates/pvs-sbcl-4.2-2.20100126svn.fc12
pvs-sbcl-4.2-2.20100126svn.fc11 has been submitted as an update for Fedora 11. http://admin.fedoraproject.org/updates/pvs-sbcl-4.2-2.20100126svn.fc11
I took a somewhat brute force method to solving this problem. I essentially told Emacs not to prompt for confirmation when attempting to visit a file that doesn't already exist. This is the root cause of the problem; the prompting code was hooked into by the ilisp code that ships with PVS, and got us into a place where some assumptions were violated. I think this approach will work okay for PVS, but let me know if it causes you any trouble.
pvs-sbcl-4.2-2.20100126svn.fc11 has been pushed to the Fedora 11 testing repository. If problems still persist, please make note of it in this bug report. If you want to test the update, you can install it with su -c 'yum --enablerepo=updates-testing update pvs-sbcl'. You can provide feedback for this update here: http://admin.fedoraproject.org/updates/F11/FEDORA-2010-1226
pvs-sbcl-4.2-2.20100126svn.fc12 has been pushed to the Fedora 12 testing repository. If problems still persist, please make note of it in this bug report. If you want to test the update, you can install it with su -c 'yum --enablerepo=updates-testing update pvs-sbcl'. You can provide feedback for this update here: http://admin.fedoraproject.org/updates/F12/FEDORA-2010-1255
pvs-sbcl-4.2-2.20100126svn.fc11 has been pushed to the Fedora 11 stable repository. If problems still persist, please make note of it in this bug report.
pvs-sbcl-4.2-2.20100126svn.fc12 has been pushed to the Fedora 12 stable repository. If problems still persist, please make note of it in this bug report.