Bug 553023

Summary:	Cannot create new proof buffer when run with Emacs
Product:	[Fedora] Fedora	Reporter:	Alan Dunn <amdunn>
Component:	pvs-sbcl	Assignee:	Jerry James <loganjerry>
Status:	CLOSED ERRATA	QA Contact:	Fedora Extras Quality Assurance <extras-qa>
Severity:	medium	Docs Contact:
Priority:	low
Version:	12	CC:	loganjerry
Target Milestone:	---
Target Release:	---
Hardware:	All
OS:	Linux
Whiteboard:
Fixed In Version:	4.2-2.20100126svn.fc12	Doc Type:	Bug Fix
Doc Text:		Story Points:	---
Clone Of:		Environment:
Last Closed:	2010-02-06 00:03:30 UTC	Type:	---
Regression:	---	Mount Type:	---
Documentation:	---	CRM:
Verified Versions:		Category:	---
oVirt Team:	---	RHEL 7.3 requirements from Atomic Host:
Cloudforms Team:	---	Target Upstream Version:
Embargoed:

Description Alan Dunn 2010-01-06 20:52:47 UTC

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.

Comment 1 Jerry James 2010-01-08 20:54:53 UTC

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.

Comment 2 Alan Dunn 2010-01-08 21:33:41 UTC

(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.

Comment 3 Jerry James 2010-01-08 22:12:58 UTC

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...

Comment 4 Jerry James 2010-01-28 23:05:22 UTC

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. :-)

Comment 5 Fedora Update System 2010-01-29 23:22:23 UTC

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

Comment 6 Fedora Update System 2010-01-29 23:22:28 UTC

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

Comment 7 Jerry James 2010-01-29 23:25:20 UTC

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.

Comment 8 Fedora Update System 2010-02-01 01:00:11 UTC

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

Comment 9 Fedora Update System 2010-02-01 01:09:58 UTC

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

Comment 10 Fedora Update System 2010-02-06 00:03:26 UTC

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.

Comment 11 Fedora Update System 2010-02-06 00:04:11 UTC

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.