[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: PVS file management
Thanks for your reply. I infer from it that the "foo.bin" file should
not be transferred. I still do dot exactly understand what information
the ".pvscontext" file contains. I know that one can safely remove it
from the directory. But can I safely replace this file (say on the Sun)
with the more version available on my Thinkpad, when I decide to
transfer stuff from the Thinkpad to the Sun??
Regarding the orther issue, Sun OS / Solaris, I don't have this problem
since we have moved to the Solaris version, and hence use Allegro 4.3 on
Dave Stringer-Calvert wrote:
> Transfer can be completed by moving foo.pvs and foo.prf to
> the other site. You can use M-x dump-pvs-files, but it's up
> to you as to which is easier in your circumstance.
> Note that there is a peculiarity in the old SunOS version of
> PVS which will *not* prove some true theorems that will prove
> under Linux. This is a problem in the old version (4.2) of
> Allegro Lisp. If you encounter this problem, let me know and
> I can provide a 4.3 version for SunOS. The Solaris version is
> already Allegro 4.3 and does not suffer this problem.
> Dr Dave Stringer-Calvert, Software Engineer, Computer Science Laboratory,
> SRI International, 333 Ravenswood Avenue, Menlo Park, CA 94025-3493, USA.
> Phone: (650) 859-3291 Fax: (650) 859-2844 Email: firstname.lastname@example.org