From b0fdbb0e88d6decd068709ea673dbe51fd6727b0 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavierleroy@users.noreply.github.com>
Date: Wed, 5 Feb 2020 18:33:13 +0100
Subject: Support Coq 8.11.0 (#212)

Update configure.
Ignore and clean up .vok and .vos files, which Coq 8.11.0 generates.
---
 configure | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'configure')

diff --git a/configure b/configure
index b964c124..d91bfebf 100755
--- a/configure
+++ b/configure
@@ -530,7 +530,7 @@ 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.8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10.0|8.10.1|8.10.2)
+  8.8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10.0|8.10.1|8.10.2|8.11.0)
         echo "version $coq_ver -- good!";;
   ?*)
         echo "version $coq_ver -- UNSUPPORTED"
-- 
cgit 


From 6950ac8fb096768cb3811ae7f89d0db080bf965a Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavierleroy@users.noreply.github.com>
Date: Wed, 5 Feb 2020 18:36:08 +0100
Subject: Revised menhirLib autoconfiguration (#331)

Since Menhir version 20200123, we need to link with menhirLib.cmxa
instead of menhirLib.cmx.

This commit chooses automatically the file to link with:
menhirLib.cmxa if it exists in the menhirLib installation directory,
menhirLib.cmx otherwise.

To reliably find the installation directory, configure was changed
to record the menhirLib directory in Makefile.config, variable MENHIR_DIR,
instead of a pre-cooked command-line option MENHIR_INCLUDES.

Makefile.extr was adapted accordingly.

Fixes: #329
Closes: #330
---
 configure | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'configure')

diff --git a/configure b/configure
index d91bfebf..a8efb551 100755
--- a/configure
+++ b/configure
@@ -582,8 +582,8 @@ 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
           echo "version $menhir_ver -- good!"
-          menhir_include_dir=$(menhir --suggest-menhirLib | tr -d '\r' | tr '\\' '/')
-          if test -z "$menhir_include_dir"; then
+          menhir_dir=$(menhir --suggest-menhirLib | tr -d '\r' | tr '\\' '/')
+          if test -z "$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."
@@ -677,7 +677,7 @@ MANDIR=$sharedir/man
 SHAREDIR=$sharedir
 COQDEVDIR=$coqdevdir
 OCAML_OPT_COMP=$ocaml_opt_comp
-MENHIR_INCLUDES=-I "$menhir_include_dir"
+MENHIR_DIR=$menhir_dir
 COMPFLAGS=-bin-annot
 EOF
 
-- 
cgit 


From d5435a34169d92a96f1436128f3e90df7f4f9e9a Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavierleroy@users.noreply.github.com>
Date: Thu, 6 Feb 2020 17:27:05 +0100
Subject: Compatibility with OCaml 4.10 (#214)

debug/DwarfPrinter.mli: unused functor parameter trigger warning 69,
  replace by non-dependent functor type.
Makefile.extr: turn warning 69 (unused functor parameter) off
  for extracted code
configure: accept OCaml versions above 4.09
configure: update messages for unsupported versions of OCaml and Coq
---
 configure | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'configure')

diff --git a/configure b/configure
index a8efb551..6bd7ed0e 100755
--- a/configure
+++ b/configure
@@ -537,7 +537,7 @@ case "$coq_ver" in
         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"
+            echo "Error: CompCert requires one of the following Coq versions: 8.11.0, 8.10.2, 8.10.1, 8.10.0, 8.9.1, 8.9.0, 8.8.2, 8.8.1, 8.8.0"
             missingtools=true
         fi;;
   "")
@@ -553,15 +553,15 @@ case "$ocaml_ver" in
         echo "version $ocaml_ver -- UNSUPPORTED"
         echo "Error: CompCert requires OCaml version 4.05 or later."
         missingtools=true;;
-  4.0*)
+  4.*)
         echo "version $ocaml_ver -- good!";;
   ?.*)
         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;;
   *)
         echo "NOT FOUND"
-        echo "Error: make sure OCaml version 4.02 or later is installed."
+        echo "Error: make sure OCaml version 4.05 or later is installed."
         missingtools=true;;
 esac
 
-- 
cgit