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

Re: [PVS-Help] proving the prelude?

Hi Hendrik,

As it can take a significant amount of time, I moved the proving of the
prelude to the validations I run.  These simply invoke

(prove-prelude t)

which you can do yourself in the *pvs* buffer.

If you think it's a good idea, you could add this option to the
Makefile, (e.g., Make test) but I don't think it's a good idea to invoke
as part of normal builds, because it can take a long time (especially on
our old Suns).


Hendrik Tews <H.Tews@cs.ru.nl> wrote:

> Hi,
> during building PVS I see the prelude being typechecked but not
> proved. When is the prelude proved?
> Bye,
> Hendrik