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

Re: PVS file management



Dave:

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
Solaris only.

Thanks,

   Paul

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.
> 
> Dave
> 
> ---
> 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: dave_sc@csl.sri.com

-- 
    pyg