aboutsummaryrefslogtreecommitdiffstats
path: root/configure
diff options
context:
space:
mode:
Diffstat (limited to 'configure')
-rwxr-xr-xconfigure52
1 files changed, 42 insertions, 10 deletions
diff --git a/configure b/configure
index 80cb2bcd..10b2c2f1 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 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p'`
case "$coq_ver" in
8.4pl*)
echo "version $coq_ver -- good!";;
@@ -223,12 +223,12 @@ 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.*)
echo "version $ocaml_ver -- good!";;
@@ -242,17 +242,50 @@ 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 2>/dev/null | sed -n -e 's/^.*version \([0-9]*\).*$/\1/p'`
case "$menhir_ver" in
- 20*)
- echo "version $menhir_ver -- good!";;
+ 20[0-9][0-9][0-9][0-9][0-9][0-9])
+ if test "$menhir_ver" -ge 20140422; then
+ echo "version $menhir_ver -- good!"
+ else
+ echo "version $menhir_ver -- UNSUPPORTED"
+ echo "Error: CompCert requires Menhir version 20140422 or later."
+ missingtools=true
+ fi;;
*)
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'
+make=''
+for mk in make gmake gnumake; do
+ make_ver=`$mk -v 2>/dev/null | head -1 | sed -n -e 's/^GNU Make //p'`
+ case "$make_ver" in
+ 3.8*|3.9*|[4-9].*)
+ echo "version $make_ver (command '$mk') -- good!"
+ make="$mk"
+ break;;
+ esac
+done
+if test -z "$make"; then
+ echo "NOT FOUND"
+ echo "Error: make sure GNU Make version 3.80 or later is installed."
+ missingtools=true
+fi
+
if $missingtools; then
echo "One or several required tools are missing or too old. Aborting."
exit 2
@@ -282,6 +315,7 @@ PREFIX=$prefix
BINDIR=$bindir
LIBDIR=$libdir
SHAREDIR=$sharedir
+OCAML_OPT_COMP=$ocaml_opt_comp
EOF
if test "$target" != "manual"; then
@@ -368,9 +402,6 @@ EOF
fi
-# Avoid re-building cparser/Parser.v on the first run
-touch cparser/Parser.v
-
# Summarize configuration
if test "$target" = "manual"; then
@@ -403,6 +434,7 @@ CompCert configuration:
Runtime library provided...... $has_runtime_lib
Library files installed in.... $libdirexp
cchecklink tool supported..... $cchecklink
+ Build command to use.......... $make
If anything above looks wrong, please edit file ./Makefile.config to correct.