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

Re: [PVS-Help] theory not found error


If you type 
$  find . -name ln_series.pvs -print
in the PVS lib directory you will see that ln_series.pvs appears in
lnexp and lnexp_fnd. 

If I remember correctly, ln_series along with logarithm and exponential
were originally in the directory analysis. Since then, we have moved
them to the directory lnexp (the axiomatic version) and lnexp_fnd (the
foundational version). The binaries of your development are probably

As usual, the best way to solve this kind of problems is just to remove
the pvsbin directory in your context and type-check your files again. If
this doesn't solve the problem, you have to provide more information
about your theories. 

Your question brings the issue of why providing two different versions
of a library. The main reason is to avoid the massive type checking of
foundational libraries.  The problem is that we haven't yet found a
satisfactory way to handle axiomatic and foundational versions of a
library. In the ideal case, the foundational one could be simply defined
as a theory interpretation of the axiomatic one, and this should be
transparent to the user who only needs to import one theory. However, I
was not able to do this in the current version of PVS (I haven't tried
this yet on PVS 3.3). The temporally solution is two have two libraries
that provide roughly the same functionality (common definition names,
common lemma names), but that have to be imported using different names.
Once you take this road, everything you develop on top of one of these
libraries has to be duplicated. In particular, the Interval package uses
the foundational libraries. If you want to use the axiomatic version,
you have to modify the IMPORTING clauses of the Interval PVS files to
import the axiomatic libraries instead of the foundational ones. Then
you have to retype-check the package.

On Thu, 2006-02-09 at 12:24, Francisco Jose CHAVES ALONSO wrote:
> Hi
> I reinstall pvs 3.2 with the NASA libraries. When I try to prove one of
> my theories (that I could prove before) emacs opens one empty file
> ln_series.pvs in the PVS directory lib/analysis/
> and appears the PVS Error message 
> Can't find file for theory real_fun_preds
> Thanks in advance,
> Francisco
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