Improving the PVS FAQ
You can contribute to this in several ways:
- by adding new questions that you feel belong here, even if you don't know the answer
- putting yourself on the watch list so that you can contribute answers to new questions
- expanding on or correcting the answers to existing questions
- reorganizing the FAQ page(s) to make it easier to find information
What does PVS stand for?
Prototype Verification System.
Kubuntu 11.04, Linux 3.0.0-12, KDE 4.7.2 429: emacs: not found
I have xemacs21 installed. I changed the pvs startup script to refer to $HOME/.xemacs rather than $HOME/.emacs, but I don't think that should be necessary and it didn't fix my problem anyway. Any suggestions? I had a two-part solution to this problem. First was, I had /sbin/pvs in my system, which was linked to /sbin/lvm. I renamed /sbin/pvs to /sbin/svp, and I have never used it anyway so it didn't matter. Once that was done, I ran "pvs -emacs xemacs" and it worked, so I created environment variable PVSEMACS = ".xemacs" and everything works very smoothly now.
MacOSX: emacs: standard input is not a tty
The pvs startup script uses the DISPLAY environment variable to decide how PVS is invoked. The default emacs on the Mac doesn't handle this correctly. The best solution is to install a different Emacs (Aqua macs is quite popular). For a quick workaround, use the -nw flag.
PVS Allegro won't start because of SELinux
The Allegro version of PVS needs an allegro library that requires text relocation, which is forbidden when SELinux is set to 'Enforcing'. The fix is to set it to 'Permissive' or 'Disabled' in /etc/selinux/config. See the man page for selinux for details.
PVS problems with Fedora Core 5, Redhat 9, or Enterprise
PVS 3.1 was developed under Redhat 7.3, and has some incompatibilities with the libraries of Redhat 9 and Enterprise that mean PVS will not start up. To fix this, you need to set some environment variables before starting PVS, and to disable ICS: The basic problem has something to do with the Posix thread library, supported in newer kernels. This is controlled by LD_ASSUME_KERNEL. For Redhat 9, the addition of the line
into the pvs shell script seemed to fix the problem. But this broke again in FC5, where setting this causes problems. The best solution I've come up with so far is to add
uname -a > /dev/null 2>&1 || unset LD_ASSUME_KERNEL
This works, because even uname stops working properly with LD_ASSUME_KERNEL set in FC5, and in that case it is unset. If someone comes up with a better explanation or solution, please add it here.
Emacs reports "Cannot open doc string file"
Your emacs is incorrectly installed, and missing the documentation strings. (A raw installation of an early version of Redhat (5.1) is known to suffer this problem.) Solution: install emacs properly (see the download page for links to Emacs sites).
When will PVS be available for other platforms?
PVS 4.0 is available for Linux, Sun, and MacOSX machines. The one obviously missing is windows. I don't use windows much, so I have no direct interest in this port. Hopefully someone else will work on it.
PVS 4.0 hangs on startup or enters the emacs debugger with an error about a Key sequence
Can be caused by an ilisp package, which is incompatible with the one provided by PVS and which is loaded on emacs startup, for instance on Debian Etch with the Debian ilisp package installed.
Fix: Deinstall ilisp or prevent by other means that it is loaded on emacs startup. On Debian Etch an empty ~/.ilisp will prevent ilisp from being loaded on startup (see /etc/emacs/site-start.d/50ilisp.el).
Strange completion behavior
Emacs 23 changed the code for minibuffer completion in a way that is incompatible with ILISP's completer.el. To work around this, run M-x completer-toggle. A permanent fix is to add
(defcustom completer-disable t "If t, disable partial completion")
to your ~/.emacs file.
Sometimes PVS asks a question, then proceeds as if I typed 'yes'
This is controlled by the PVS Emacs variable pvs-default-timeout, which is the number of seconds to wait before using the default answer. The reason for this is that it is very natural to start a long proof, then go to lunch and see the result after. It is then a little disheartening to return, and see that PVS has been waiting to see if you want to rerun the existing proof. The default is to wait 10 seconds, but you can set this to any value you want, for example, 100 seconds, by adding
(setq pvs-default-timeout 100)
to your ~/.pvsemacs file. It must be set to an integer value; just set it to a large number if you effectively don't want a timeout.
Trivial arithmetic facts not recognized
Sometimes assert does not recognize trivial facts such as 2 <= 14. This is a known problem with the current decision procedures, which are heavily modified versions of Shostak's original code. This problem will not be solved until we integrate a new decision procedure. The basic problem is that the decision procedures are sensitive to the order assertions are made, and occasionally miss assertions such as these. The workaround is to use the :flush? argument to assert, which clears the decision procedure database (for this sequent) before asserting everything once again.
Proof Commands take Forever
In many cases, there is nothing that can be done about this, but here are some suggestions that may help
Use the flush? flag
Sometimes the decision procedure database gets overloaded with irrelevant facts, and bogs down. Running (assert :flush? t) clears the database for the current branch of the proof tree. Note that this means that hidden formulas are no longer in the database, so make sure all relevant formulas are still in the sequent when using this.