[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] Error: No Method Applicable for Generic Function
IMHO this is a better approach:
1. Define the environment variable PVS_LIBRARY_PATH:
PVS_LIBRARY_PATH=:<fooroot>
where <fooroot> is the full path to the root of foo, i.e.,
$ test -d <fooroot>/foo && echo Yes
should print Yes.
2. Remove lib:LIBRARY = "foo/" from theory1 and import theory2 as
follows:
IMPORTING foo@theory2
3. Done.
Cesar
On Wed, 2006-03-08 at 15:36, Nikhil D. Kikkeri wrote:
> Hi--
>
> This seems like a PVS bug, since I saw many other instances of the same
> error on the bug list. I have encountered the same error many times but I
> have somehow found a solution to it until now.
>
> My problem is the following. In a nutshell my theory looks something like
> this
>
> theory1: THEORY
>
> BEGIN
>
> lib: LIBRARY = "foo/"
> IMPORTING lib@theory2, theory3
>
> ...
> ...
> END theory1
>
> Now theory2 that is located in the directory "foo" looks something like this
>
> theory2: THEORY
>
> BEGIN
> IMPORTING theory2a
>
> ...
> ...
>
> END theory2
>
>
> I can successfully typecheck theory2 independently. When I create a dmp file
> , all the dependencies are also included. In short, everything works out
> fine.
>
> However, when I import theory2 into theory1 I get the error that is
> mentioned in the subject line. Also I notice that the dmp file for theory 1
> does not include its dependencies (i.e. theory 2 etc.) even though during
> the typechecking of theory1, the bin files of the import chain are located
> properly.
>
> As a result I cannot even send the complete dmp file of theory1. Any
> suggestions will be greatly appreciated.
>
> Thank you in advance
>
> Rgds
> -Nikhil
>
> ---
> http://engr.smu.edu/~nikhil
>
--
Cesar A. Munoz H., Senior Staff Scientist mailto:munoz@nianet.org
National Institute of Aerospace mailto:C.A.Munoz@larc.nasa.gov
100 Exploration Way http://research.nianet.org/~munoz
Hampton, VA 23666, USA Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988