Add (almost) compatibility with camlp4, without breaking support for camlp5

The choice between camlp4/5 is done during configure with flags
 -usecamlp5 (default for the moment) vs. -usecamlp4.

 Currently, to have a full camlp4 compatibility, you need to change
 all "EXTEND" and "GEXTEND Gram" into "EXTEND Gram", and change "EOI"
 into "`EOI" in grammar entries. I've a sed script that does that
 (actually the converse), but I prefer to re-think it and check a few
 things before branching this sed into the build mechanism.

 lib/compat.ml4 is heavily used to hide incompatibilities between camlp4/5
 and try to propose a common interface (cf LexerSig / GrammarSig).
 A few incompatible quotations have been turned into underlying code
 manually, in order to make the IFDEF CAMLP5 THEN ... ELSE ... END
 parsable by both camlp4 and 5. See in particular the fate of
 <:str_item< declare ... end >>

 Stdpp isn't used anymore, but rather Ploc (hidden behind local module Loc).
 This forces to use camlp5 > 5.01.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13019 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 65 insertions, 50 deletions

diff --git a/configure b/configure
index 69a900b3bf..a12adf36e4 100755
--- a/configure
+++ b/configure
@@ -57,6 +57,10 @@ usage () {
     printf "\tSpecifies the path to the OCaml library\n"
     echo "-lablgtkdir"
     printf "\tSpecifies the path to the Lablgtk library\n"
+    echo "-usecamlp5"
+    printf "\tSpecifies to use camlp5 instead of camlp4\n"
+    echo "-usecamlp4"
+    printf "\tSpecifies to use camlp4 instead of camlp5\n"
     echo "-camlp5dir"
     printf "\tSpecifies where to look for the Camlp5 library and tells to use it\n"
     echo "-arch"
@@ -141,6 +145,7 @@ with_doc=all
 with_doc_spec=no
 force_caml_version=no
 force_caml_version_spec=no
+usecamlp5=yes
 
 COQSRC=`pwd`
 
@@ -193,7 +198,12 @@ while : ; do
     -lablgtkdir|--lablgtkdir) lablgtkdir_spec=yes
 	                lablgtkdir="$2"
 			shift;;
+    -usecamlp5|--usecamlp5)
+	                usecamlp5=yes;;
+    -usecamlp4|--usecamlp4)
+	                usecamlp5=no;;
     -camlp5dir|--camlp5dir)
+                        usecamlp5=yes
 	                camlp5dir="$2"
 			shift;;
     -arch|--arch) arch_spec=yes
@@ -479,77 +489,81 @@ esac
 
 # Camlp4 / Camlp5 configuration
 
-if [ "$camlp5dir" != "" ]; then
+# Assume that camlp(4|5) binaries are at the same place as ocaml ones
+# (this should become configurable some day)
+CAMLP4BIN=${CAMLBIN}
+
+if [ "$usecamlp5" = "yes" ]; then
     CAMLP4=camlp5
-    CAMLP4LIB=$camlp5dir
-    if [ ! -f $camlp5dir/camlp5.cma ]; then
-	echo "Cannot find camlp5 libraries in $camlp5dir (camlp5.cma not found)."
+    CAMLP4MOD=gramlib
+    if [ "$camlp5dir" != "" ]; then
+	if [ -f "$camlp5dir/${CAMLP4MOD}.cma" ]; then
+	    CAMLP4LIB=$camlp5dir
+	    FULLCAMLP4LIB=$camlp5dir
+	else
+	    echo "Cannot find camlp5 libraries in $camlp5dir (camlp5.cma not found)."
+	    echo "Configuration script failed!"
+	    exit 1
+	fi
+    elif [ -f "${CAMLLIB}/camlp5/${CAMLP4MOD}.cma" ]; then
+        CAMLP4LIB=+camlp5
+	FULLCAMLP4LIB=${CAMLLIB}/camlp5
+    elif [ -f "${CAMLLIB}/site-lib/${CAMLP4MOD}.cma" ]; then
+        CAMLP4LIB=+site-lib/camlp5
+	FULLCAMLP4LIB=${CAMLLIB}/site-lib/camlp5
+    else
+	echo "Objective Caml $CAMLVERSION found but no Camlp5 installed."
 	echo "Configuration script failed!"
 	exit 1
     fi
+
     camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'`
-    if [ `$camlp4oexec -pmode 2>&1` = "strict" ]; then 
-	echo "Error: Camlp5 found, but in strict mode!"
-	echo "Please compile Camlp5 in transitional mode."
+    if [ "`$camlp4oexec -pmode 2>&1`" != "transitional" ]; then
+	echo "Error: $camlp4oexec not found, or not in transitional mode!"
+	echo "Configuration script failed!"
 	exit 1
     fi
-else
-    case $CAMLTAG in
-        OCAML31*)
-            if [ -x "${CAMLLIB}/camlp5" ]; then
-                CAMLP4LIB=+camlp5
-            elif [ -x "${CAMLLIB}/site-lib/camlp5" ]; then
-                CAMLP4LIB=+site-lib/camlp5
-            else
-	        echo "Objective Caml $CAMLVERSION found but no Camlp5 installed."
-	        echo "Configuration script failed!"
-	        exit 1
-            fi
-            CAMLP4=camlp5
-            camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'`
-            if [ `$camlp4oexec -pmode 2>&1` = "strict" ]; then
-	        echo "Error: Camlp5 found, but in strict mode!"
-	        echo "Please compile Camlp5 in transitional mode."
-	        exit 1
-            fi
-            ;;
-        *)
-            CAMLP4=camlp4
-            CAMLP4LIB=+camlp4
-            ;;
+    case `$camlp4oexec -v 2>&1` in
+	*4.0*|*5.00*)
+	    echo "Camlp5 version < 5.01 not supported."
+	    echo "Configuration script failed!"
+	    exit 1;;
     esac
-fi
-
-if [ "$CAMLP4" = "camlp5" ] && `$camlp4oexec -v 2>&1 | grep -q 5.00`; then
-    echo "Camlp5 version 5.00 not supported: versions 4.0x or >= 5.01 are OK."
-    echo "Configuration script failed!"
-    exit 1
-fi
 
+else # let's use camlp4
+    CAMLP4=camlp4
+    CAMLP4MOD=camlp4lib
+    CAMLP4LIB=+camlp4
+    FULLCAMLP4LIB=${CAMLLIB}/camlp4
 
-case $CAMLP4LIB in
-    +*) FULLCAMLP4LIB=$CAMLLIB/`echo $CAMLP4LIB | cut -b 2-`;;
-    *)  FULLCAMLP4LIB=$CAMLP4LIB;;
-esac
+    if [ ! -f "${FULLCAMLP4LIB}/${CAMLP4MOD}.cma" ]; then
+	echo "Objective Caml $CAMLVERSION found but no Camlp4 installed."
+	echo "Configuration script failed!"
+	exit 1
+    fi
 
-# Assume that camlp(4|5) binaries are at the same place as ocaml ones
-# (this should become configurable some day) 
-CAMLP4BIN=${CAMLBIN}
+    camlp4oexec=${camlp4oexec}rf
+    if [ "`$camlp4oexec 2>&1`" != "" ]; then
+	echo "Error: $camlp4oexec not found or not executable."
+	echo "Configuration script failed!"
+	exit 1
+    fi
+fi
 
 # do we have a native compiler: test of ocamlopt and its version
 
 if [ "$best_compiler" = "opt" ] ; then
   if test -e "$nativecamlc" || test -e "`which $nativecamlc`"; then
       CAMLOPTVERSION=`"$nativecamlc" -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `
-      if [ ! -f $FULLCAMLP4LIB/gramlib.cmxa ]; then
+      if [ ! -f "${FULLCAMLP4LIB}/${CAMLP4MOD}.cmxa" ]; then
 	  best_compiler=byte
 	  echo "Cannot find native-code $CAMLP4,"
 	  echo "only the bytecode version of Coq will be available."
       else
-        if [ "$CAMLOPTVERSION" != "$CAMLVERSION" ] ; then
-	  echo "Native and bytecode compilers do not have the same version!"
-        fi
-        echo "You have native-code compilation. Good!"
+          if [ "$CAMLOPTVERSION" != "$CAMLVERSION" ] ; then
+	      echo "Native and bytecode compilers do not have the same version!"
+          fi
+          echo "You have native-code compilation. Good!"
       fi
   else
       best_compiler=byte
@@ -1049,6 +1063,7 @@ sed -e "s|LOCALINSTALLATION|$local|" \
     -e "s|OSDEPENDENTP4OPTFLAGS|$OSDEPP4OPTFLAGS|" \
     -e "s|CAMLLIBDIRECTORY|$CAMLLIB|" \
     -e "s|CAMLTAG|$CAMLTAG|" \
+    -e "s|CAMLP4VARIANT|$CAMLP4|" \
     -e "s|CAMLP4BINDIRECTORY|$CAMLP4BIN|" \
     -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIB|" \
     -e "s|CAMLP4TOOL|$camlp4oexec|" \