fixed installation and distribution of PVS support

Makefile.in

@@ -1052,6 +1052,7 @@ clean::
 
 install_no_local::
 	cp -f bin/why3-cpulimit$(EXE) $(BINDIR)/why3-cpulimit$(EXE)
+	cp -f bin/why3-call-pvs $(BINDIR)/why3-call-pvs
 
 #########
 # why3doc
@@ -1462,6 +1463,7 @@ DISTRIB_FILES = Version Makefile.in configure.in configure \
       src/*.ml* src/*.dep src/*/*.ml* src/*/*.dep src/*/*.c \
       plugins/printer/.keepme plugins/*/*.ml* plugins/*/*.dep \
       lib/why3/META.in lib/why3/why3.ml \
+      bin/why3-call-pvs \
       doc/version.tex.in doc/manual.pdf \
       drivers/*.drv drivers/*.gen \
       examples/*.mlw examples/logic/*.why \

bin/db

-set arguments ../tests/test-pgm-jcf.mlw
-dir ..
-dir ../src
-dir ../src/util
-dir ../src/core
-dir ../src/programs
-load_printer "str.cma"
-load_printer "nums.cma"
-load_printer "why.cma"
-

bin/why3-call-pvs

-#!/bin/bash
+#!/bin/sh
 
 if test -z "$PVS_LIBRARY_PATH"; then
     export PVS_LIBRARY_PATH=$1/pvs
 else
     export PVS_LIBRARY_PATH=$1/pvs:$PVS_LIBRARY_PATH
 fi
-exec pvs $2
-
-
-
+shift
+exec "$@"

bin/why3-check-pvs

-#!/bin/bash
-
-if test -z "$PVS_LIBRARY_PATH"; then
-    export PVS_LIBRARY_PATH=$1/pvs
-else
-    export PVS_LIBRARY_PATH=$1/pvs:$PVS_LIBRARY_PATH
-fi
-cd `dirname $2`
-exec proveit -q `basename $2`
-
-
-

configure.in

@@ -516,7 +516,7 @@ if test "$enable_pvs_libs" = yes; then
    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
+   for dir in  `echo $PVS_LIBRARY_PATH | tr ':' ' '`; do
        if test -f $dir/nasalib-version; then
           enable_pvs_libs=yes
           reason_pvs_libs=""

share/provers-detection-data.conf.in

@@ -378,14 +378,14 @@ version_switch = "-version"
 version_regexp = "PVS Version \\([^ \n]+\\)"
 version_ok = "6.0"
 version_bad = "^[0-5]\..+$"
-command = "'@LOCALBIN@why3-cpulimit' 0 %m -s @LOCALBIN@why3-check-pvs %l %f"
+command = "'@LOCALBIN@why3-cpulimit' 0 %m -s @LOCALBIN@why3-call-pvs %l proveit -f %f"
 driver = "drivers/pvs.drv"
 in_place = true
 editor = "pvs"
 
 [editor pvs]
 name = "PVS"
-command = "@LOCALBIN@why3-call-pvs %l %f"
+command = "@LOCALBIN@why3-call-pvs %l pvs %f"
 
 [editor coqide]
 name = "CoqIDE"