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

Re: User libraries in the PVS lib directory

Hi Dave,

Thanks for the reply. I need a couple of clarifications on your reply.

> Theories in the lib subdirectory are not extensions to the prelude,
> they are just a convenient repository and don't require a LIBRARY
> clause.

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?

> Look at the documentation for M-x load-prelude-library to see how to
> extend the prelude with a specified context.

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?

I appreciate your help. Thanks. Bye.

> Note that it is not necessary to specifically give IMPORTING clauses for
> things in the prelude - they are imported into the current context anyway.
> 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 David.Stringer-Calvert@sri.com

Best Wishes,
	-- Murali
Murali Rangarajan  #  rmurali@ececs.uc.edu # http://www.ececs.uc.edu/~rmurali
Knowledge Based Software Engineering Lab   #   finger machines : ella, evans
Phone:           R-(513) 872 0878          #          O-(513) 556 0267 

"The most difficult thing in the world is to know how to do a thing and
to watch someone else do it wrong without comment."
                -- Theodore H. White

The safest way to double your money is to fold it over and put it in your 
pocket. -Kin Hubbard