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

[Sam Owre <owre@xxxxxxxxxxx>]

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?

Thanks,
Sam

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