[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS-Help] Error: "Restarts:"

Hi Jerome,

I need more information, as almost any lisp problem could lead to this
behavior.  Could you send me a tar dump of your directory?


Jerome <jerome@xxxxxxxxxxxxxx> wrote:

> I have several PVS files in a particular directory that I'm unable to
> operate on. When I have the file open in PVS and try to typecheck or
> prove/show-proof a lemma, PVS creates a new emacs buffer above the
> theory and displays "Restarts:". In the lower buffer I have the
> following options:
>  SPC-scroll, I-ignore, K-keep, A-abort sends and keep or B-break:
> What does this mean and why am I seeing it (all of a sudden)?
> jerome