diff --git a/configure b/configure index 25b854890..ed99c5935 100755 --- a/configure +++ b/configure @@ -30,6 +30,7 @@ clightgen=false install_coqdev=false ignore_coq_version=false ignore_ocaml_version=false +ignore_menhir_version=false library_Flocq=local library_MenhirLib=local @@ -101,6 +102,7 @@ Options: -install-coqdev Also install the Coq development (implied by -clightgen) -ignore-coq-version Accept to use experimental or unsupported versions of Coq -ignore-ocaml-version Accept to use experimental or unsupported versions of OCaml + -ignore-menhir-version Accept to use experimental or unsupported versions of Menhir ' # @@ -140,6 +142,8 @@ while : ; do ignore_coq_version=true;; -ignore-ocaml-version|--ignore-ocaml-version) ignore_ocaml_version=true;; + -ignore-menhir-version|--ignore-menhir-version) + ignore_menhir_version=true;; -install-coqdev|--install-coqdev|-install-coq-dev|--install-coq-dev) install_coqdev=true;; -use-external-Flocq|--use-external-Flocq) @@ -560,7 +564,7 @@ fi MENHIR_REQUIRED=20200624 echo "Testing Menhir... " | tr -d '\n' -menhir_ver=`menhir --version 2>/dev/null | sed -n -e 's/^.*version \([0-9]*\).*$/\1/p'` +menhir_ver=$(menhir --version 2>/dev/null | sed -n -E -e 's/^.*version (unreleased|[0-9]*).*$/\1/p') case "$menhir_ver" in 20[0-9][0-9][0-9][0-9][0-9][0-9]) if test "$menhir_ver" -ge $MENHIR_REQUIRED; then @@ -575,15 +579,38 @@ case "$menhir_ver" in echo "Consider using the OPAM package for Menhir." missingtools=true fi + else + echo "version $menhir_ver -- UNSUPPORTED" + if $ignore_menhir_version; then + echo "Warning: this version of Menhir is unsupported, proceed at your own risks." + else + echo "Error: CompCert requires a version greater or equal to $MENHIR_REQUIRED." + missingtools=true + fi + fi;; + *) + if test -z "$menhir_ver"; then + echo "NOT FOUND" + echo "Error: make sure Menhir version $MENHIR_REQUIRED or later is installed." + missingtools=true + elif $ignore_menhir_version; then + echo "version $menhir_ver -- UNSUPPORTED" + echo "Warning: this version of Menhir is unsupported, proceed at your own risks." + menhir_dir=$(ocamlfind query menhirLib 2>/dev/null) || \ + menhir_dir=$(menhir --suggest-menhirLib) || \ + menhir_dir="" + menhir_dir=$(echo "$menhir_dir" | tr -d '\r' | tr '\\' '/') + if test ! -d "$menhir_dir"; then + echo "Error: cannot determine the location of the Menhir API library." + echo "This can be due to an incorrect Menhir package." + echo "Consider using the OPAM package for Menhir." + missingtools=true + fi else echo "version $menhir_ver -- UNSUPPORTED" echo "Error: CompCert requires a version greater or equal to $MENHIR_REQUIRED." missingtools=true fi;; - *) - echo "NOT FOUND" - echo "Error: make sure Menhir version $MENHIR_REQUIRED or later is installed." - missingtools=true;; esac echo "Testing GNU make... " | tr -d '\n'