[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
RE: [PVS-Help] PVS 4, errors in Proof buffer?
I was at the PVS class in Nov this year and had the same question. The
answer appears to be that CMU-Lisp is the culprit. This message does
not occur with Allegro Lisp.
It's seems to be benign (but disconcerting)...
[mailto:email@example.com] On Behalf
Of Steve Johnson
Sent: Thursday, December 13, 2007 2:53 PM
To: firstname.lastname@example.org; Paul S. Miner
Subject: [PVS-Help] PVS 4, errors in Proof buffer?
Does anyone recognize this symptom?
I'm running PVS 4 on some old sources and get an error in the
The full buffer content is attached, but the last few lines are:
<PVS *proof* buffer>
Help! 12 nested errors. KERNEL:*MAXIMUM-ERROR-DEPTH* exceeded.
Debug (type H for help)
(UNIX::SIGSEGV-HANDLER #<unused-arg> #<unused-arg> #.(SYSTEM:INT-SAP
I removed existing *.pvscontext* and *pvsbin/ *before invoking the
*M-x step-proof* does not generate this error.