Re: [PVS-Help] Not at a formula declaration

[Sam Owre <owre@xxxxxxxxxxx>]

Hi Jerome,

I'm looking into the webpage problem - it should be fixed
by tomorrow.

Could you give me a bit more information about the 'M-x
prove' bug?  Maybe send me the PVS file(s) involved, where
you put the cursor, and whether there are any bin files
being loaded (they would be in a "pvsbin" subdirectory).

Thanks,
Sam

Jerome <jerome@xxxxxxxxxxxxxx> wrote:

> I put my cursor over a lemma, type 'M-x prove', and get the following
> error in the status buffer: "Not at a formula declaration." I've done
> this several times in the past (even successfully to the file in
> question), so I'm quite certain my cursor is over a forumla. What
> makes this even stranger is that it only happens in two of three files
> in my working directory.
> 
> It looks like BUG 926 addresses this issue, but I can't seem to get
> the webpage to load.
> 
> jerome