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

Re: User libraries in the PVS lib directory




> I understand that theories in the lib directory do not require a LIBRARY
> clause. But, do user theories in the lib directory (and NOT in a
> subdirectory) need an IMPORTING clause? Or can they be used without
> importing them?

Yes, they still need an importing clause.

> I tried this, and it worked great. The next time I started PVS from the
> SAME directory, it loaded the theories in the added context automatically.
> But, if I run PVS from a DIFFERENT directory, it did not load the theories
> automatically. Is there any way to have the theories loaded automatically,
> no matter which directory PVS is used in?

Yes, but I wouldn't recommend doing this as it makes things less obvious
as to where the importings are coming from.  If you insist, put the
following in your .pvsemacs

(load-prelude-library "/path/to/my/lib/directory")

Where "/path/to/my/lib/directory" is the context containing the prelude
extensions.

Dave

---
Dr Dave Stringer-Calvert, Sr. Systems Admin, Computer Science Laboratory
SRI International, 333 Ravenswood Avenue, Menlo Park, CA 94025-3493, USA
Phone: (650) 859-3291 Fax: (650) 859-2844 David.Stringer-Calvert@sri.com