[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] proving the prelude?
As it can take a significant amount of time, I moved the proving of the
prelude to the validations I run. These simply invoke
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:
> during building PVS I see the prelude being typechecked but not
> proved. When is the prelude proved?