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

Re: [PVS-Help] theory not found error



Hi

> The file ln_series.pvs is not in lib/analysis with the latest NASA
> release.  It is in lnexp and lnexp_fnd.  Does your theory say:
> 
>   IMPORTING analysis@ln_series
> 
> ?  If so, you will have to change "analysis" to "lnexp" or "lnexp_fnd",
> whichever is appropriate for you.  If not, you may need to remove
> your .bin files and reprove everything.
> 

As I'm not importing the analysis@ln_series theory, then I removed
the .bin files of my theory and the problem persisted, then
I erased the .bin and reprove the files:

lnexp_fnd/ln_series.pvs
lnexp_fnd/ln_approx.pvs
interval/interval_approx.pvs

and the problem is solved

(I imported the theory interval_approx that imports ln_approx and the
last one imports ln_series. When I tried to shows the tccs of those
files, I had the same problem than in my theory file, for that reason I
erased his .bin files and reprove them.)

Thank you

Francisco

-- 
Francisco José Cháves (ENS-LIP) 
mailto: Francisco.Jose.Chaves.Alonso@ens-lyon.fr
http://perso.ens-lyon.fr/francisco.jose.chaves.alonso
ENS de Lyon - 46, allee d'Italie - 69364 Lyon Cedex 07 - FRANCE
Phone: (+33) 4 72 72 84 36