diff options
Diffstat (limited to 'configure')
| -rwxr-xr-x | configure | 61 |
1 files changed, 48 insertions, 13 deletions
@@ -18,6 +18,7 @@ libdir='$(PREFIX)/lib/compcert' toolprefix='' target='' has_runtime_lib=true +build_checklink=true usage='Usage: ./configure [options] target @@ -64,6 +65,8 @@ while : ; do toolprefix="$2"; shift;; -no-runtime-lib) has_runtime_lib=false; shift;; + -no-checklink) + build_checklink=false; shift;; *) if test -n "$target"; then echo "$usage" 1>&2; exit 2; fi target="$1";; @@ -89,7 +92,7 @@ case "$target" in casmruntime="${toolprefix}gcc -c -Wa,-mregnames" clinker="${toolprefix}gcc" libmath="-lm" - cchecklink=true;; + cchecklink=${build_checklink};; powerpc-eabi-diab|ppc-eabi-diab) arch="powerpc" model="standard" @@ -101,7 +104,7 @@ case "$target" in asm_supports_cfi=false clinker="${toolprefix}dcc" libmath="-lm" - cchecklink=true;; + cchecklink=${build_checklink};; arm*-*) arch="arm" case "$target" in @@ -154,7 +157,7 @@ case "$target" in abi="standard" system="macosx" cc="${toolprefix}gcc -arch i386" - cprepro="${toolprefix}gcc -arch i386 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' -E" + cprepro="${toolprefix}gcc -arch i386 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' -E" casm="${toolprefix}gcc -arch i386 -c" case `uname -r` in [1-9].*|10.*|11.*) # up to MacOS 10.7 included @@ -213,7 +216,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 +226,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 +245,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 +318,7 @@ PREFIX=$prefix BINDIR=$bindir LIBDIR=$libdir SHAREDIR=$sharedir +OCAML_OPT_COMP=$ocaml_opt_comp EOF if test "$target" != "manual"; then @@ -368,9 +405,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 +437,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. |