aboutsummaryrefslogtreecommitdiffstats
path: root/configure
diff options
context:
space:
mode:
authorBernhard Schommer <bschommer@users.noreply.github.com>2019-10-31 11:49:42 +0100
committerXavier Leroy <xavierleroy@users.noreply.github.com>2019-10-31 11:49:42 +0100
commit029329c8adc955d9ebe9030074cce0df9dcfa5f7 (patch)
treeaa4710f853f74020f6cb108114884b177ce61ebd /configure
parenta0844a9b6eb88f9e75f7305e8d1505cf502fb81a (diff)
downloadcompcert-kvx-029329c8adc955d9ebe9030074cce0df9dcfa5f7.tar.gz
compcert-kvx-029329c8adc955d9ebe9030074cce0df9dcfa5f7.zip
Raise minimal required versions for OCaml and Coq (#203)
At least OCaml 4.05 is now required as well as Coq 8.8.
Diffstat (limited to 'configure')
-rwxr-xr-xconfigure13
1 files changed, 4 insertions, 9 deletions
diff --git a/configure b/configure
index cb2747be..8604a1d9 100755
--- a/configure
+++ b/configure
@@ -530,14 +530,14 @@ missingtools=false
echo "Testing Coq... " | tr -d '\n'
coq_ver=$(${COQBIN}coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p')
case "$coq_ver" in
- 8.7.0|8.7.1|8.7.2|8.8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10.0|8.10.1)
+ 8.8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10.0|8.10.1)
echo "version $coq_ver -- good!";;
?*)
echo "version $coq_ver -- UNSUPPORTED"
if $ignore_coq_version; then
echo "Warning: this version of Coq is unsupported, proceed at your own risks."
else
- echo "Error: CompCert requires one of the following Coq versions: 8.10.1, 8.10.0, 8.9.1, 8.9.0, 8.8.2, 8.8.1, 8.8.0, 8.7.2, 8.7.1, 8.7.0"
+ echo "Error: CompCert requires one of the following Coq versions: 8.10.1, 8.10.0, 8.9.1, 8.9.0, 8.8.2, 8.8.1, 8.8.0"
missingtools=true
fi;;
"")
@@ -549,15 +549,10 @@ esac
echo "Testing OCaml... " | tr -d '\n'
ocaml_ver=`ocamlopt -version 2>/dev/null`
case "$ocaml_ver" in
- 4.00.*|4.01.*)
+ 4.00.*|4.01.*| 4.02.*|4.03.*|4.04.*)
echo "version $ocaml_ver -- UNSUPPORTED"
- echo "Error: CompCert requires OCaml version 4.02 or later."
+ echo "Error: CompCert requires OCaml version 4.05 or later."
missingtools=true;;
- 4.02.*|4.03.*|4.04.*)
- echo "version $ocaml_ver -- good!"
- echo "WARNING: some Intel processors of the Skylake and Kaby Lake generations"
- echo "have a hardware bug that can be triggered by this version of OCaml."
- echo "To avoid this risk, it is recommended to use OCaml 4.05 or later.";;
4.0*)
echo "version $ocaml_ver -- good!";;
?.*)