fixed configuration/installation with PVS

parent f0db2b2a
......@@ -4,7 +4,7 @@
* [GTK sourceview] why.lang renamed to why3.lang
version 0.81, March 25, 2013
==========================
============================
o [prover] experimental support for SPASS >= 3.8 (with types)
o [prover] support for Z3 4.3.*
......
......@@ -958,11 +958,9 @@ PVSLIBS_LIST = $(addprefix lib/pvs/int/, $(PVSLIBS_LIST_FILES))
PVSLIBS_NUMBER_FILES = # Divisibility Gcd Parity Prime
PVSLIBS_NUMBER = $(addprefix lib/pvs/number/, $(PVSLIBS_NUMBER_FILES))
ifeq (@enable_pvs_nasa_libs@,yes)
PVSLIBS_FP_FILES = Rounding SingleFormat Single DoubleFormat Double
PVSLIBS_FP_ALL_FILES = GenFloat $(PVSLIBS_FP_FILES)
PVSLIBS_FP = $(addprefix lib/pvs/floating_point/, $(PVSLIBS_FP_ALL_FILES))
endif
PVSLIBS_FILES = $(PVSLIBS_INT) $(PVSLIBS_REAL) $(PVSLIBS_LIST) \
$(PVSLIBS_NUMBER) $(PVSLIBS_FP)
......@@ -989,10 +987,8 @@ install_no_local::
mkdir -p $(LIBDIR)/why3/pvs/real
cp $(addsuffix .pvs, $(PVSLIBS_REAL)) $(LIBDIR)/why3/pvs/real/
cp $(addsuffix .prf, $(PVSLIBS_REAL)) $(LIBDIR)/why3/pvs/real/
ifeq (@enable_pvs_nasa_libs@,yes)
mkdir -p $(LIBDIR)/why3/pvs/floating_point/
cp $(PVSLIBS_FP) $(LIBDIR)/why3/pvs/
endif
cp drivers/pvs-realizations.aux $(DATADIR)/why3/drivers/
install_local: drivers/pvs-realizations.aux
......@@ -1481,6 +1477,7 @@ DISTRIB_FILES = Version Makefile.in configure.in configure \
theories/*.why \
modules/*.mlw \
lib/coq/*.v lib/coq/*/*.v lib/coq-tactic/*.v \
lib/pvs/*/*.pvs lib/pvs/*/*.prf \
share/provers-detection-data.conf.in \
share/why3session.dtd \
share/javascript/*.js share/javascript/*.css \
......
......@@ -513,16 +513,16 @@ if test "$enable_pvs_support" = no; then
fi
if test "$enable_pvs_libs" = yes; then
AC_MSG_CHECKING([for NASA libraries])
enable_pvs_nasa_libs=no
reason_pvs_nasa_libs=" (not in PVS_LIBRARY_PATH)"
AC_MSG_CHECKING([for NASA PVS library])
enable_pvs_libs=no
reason_pvs_libs=" (no NASA PVS library in PVS_LIBRARY_PATH)"
for dir in ${PVS_LIBRARY_PATH//:/ }; do
if test -f $dir/nasalib-version; then
enable_pvs_nasa_libs=yes
reason_pvs_nasa_libs=""
enable_pvs_libs=yes
reason_pvs_libs=""
fi
done
AC_MSG_RESULT($enable_pvs_nasa_libs)
AC_MSG_RESULT($enable_pvs_libs)
fi
# hypothesis_selection
......@@ -633,7 +633,6 @@ AC_SUBST(COQLIB)
AC_SUBST(COQVERSION)
AC_SUBST(enable_pvs_libs)
AC_SUBST(enable_pvs_nasa_libs)
AC_SUBST(PVS)
AC_SUBST(PVSVERSION)
......@@ -708,9 +707,6 @@ if test "$enable_pvs_support" = yes ; then
echo " Version : $PVSVERSION"
echo " Library path : $PVSLIB"
echo " Realization support : $enable_pvs_libs$reason_pvs_libs"
if test "$enable_pvs_libs" = yes ; then
echo " NASA libraries : $enable_pvs_nasa_libs$reason_pvs_nasa_libs"
fi
fi
echo "Frama-C support : $enable_frama_c$reason_frama_c"
if test "$enable_frama_c" = yes ; then
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment