aboutsummaryrefslogtreecommitdiffstats
path: root/configure
diff options
context:
space:
mode:
Diffstat (limited to 'configure')
-rwxr-xr-xconfigure33
1 files changed, 24 insertions, 9 deletions
diff --git a/configure b/configure
index f3967dc7..7e1417bb 100755
--- a/configure
+++ b/configure
@@ -213,7 +213,7 @@ fi
missingtools=false
echo "Testing Coq... " | tr -d '\n'
-coq_ver=`coqc -v | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p'`
+coq_ver=`(coqc -v | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p') 2>/dev/null`
case "$coq_ver" in
8.4pl*)
echo "version $coq_ver -- good!";;
@@ -223,14 +223,14 @@ case "$coq_ver" in
missingtools=true;;
*)
echo "NOT FOUND"
- echo "Error: make sure Coq version 8.4pl4 is installed."
+ echo "Error: make sure Coq version 8.4 pl5 is installed."
missingtools=true;;
esac
echo "Testing OCaml... " | tr -d '\n'
-ocaml_ver=`ocamlc -version`
+ocaml_ver=`ocamlopt -version 2>/dev/null`
case "$ocaml_ver" in
- 4.*)
+ [4-9].*)
echo "version $ocaml_ver -- good!";;
?.*)
echo "version $ocaml_ver -- UNSUPPORTED"
@@ -242,21 +242,35 @@ case "$ocaml_ver" in
missingtools=true;;
esac
+echo "Testing OCaml .opt compilers... " | tr -d '\n'
+ocaml_opt_ver=`ocamlopt.opt -version 2>/dev/null`
+if test "$ocaml_opt_ver" = "$ocaml_ver"; then
+ echo "yes"
+ ocaml_opt_comp=true
+else
+ echo "no, will do without"
+ ocaml_opt_comp=false
+fi
+
echo "Testing Menhir... " | tr -d '\n'
-menhir_ver=`menhir --version | sed -n -e 's/^.*version \([0-9]*\).*$/\1/p'`
+menhir_ver=`(menhir --version | sed -n -e 's/^.*version \([0-9]*\).*$/\1/p') 2>\dev\null`
case "$menhir_ver" in
- 20*)
+ 201[4-9]*|20[2-9]*)
echo "version $menhir_ver -- good!";;
+ ?*)
+ echo "version $menhir_ver -- UNSUPPORTED"
+ echo "Error: CompCert requires Menhir version 20140422 or later."
+ missingtools=true;;
*)
echo "NOT FOUND"
- echo "Error: make sure Menhir is installed."
+ echo "Error: make sure Menhir version 20140422 or later is installed."
missingtools=true;;
esac
-echo "Testing GNU make..." | tr -d '\n'
+echo "Testing GNU make... " | tr -d '\n'
make=''
for mk in make gmake gnumake; do
- make_ver=`$mk -v | head -1 | sed -n -e 's/^GNU Make //p'`
+ make_ver=`($mk -v | head -1 | sed -n -e 's/^GNU Make //p') 2>/dev/null`
case "$make_ver" in
3.8*|3.9*|[4-9].*)
echo "version $make_ver (command '$mk') -- good!"
@@ -299,6 +313,7 @@ PREFIX=$prefix
BINDIR=$bindir
LIBDIR=$libdir
SHAREDIR=$sharedir
+OCAML_OPT_COMP=$ocaml_opt_comp
EOF
if test "$target" != "manual"; then