Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

1 files changed, 179 insertions, 109 deletions

diff --git a/configure b/configure
index 2cfbf7c4..59cfcb9f 100755
--- a/configure
+++ b/configure
@@ -6,8 +6,8 @@
 # 
 ##################################
 
-VERSION=8.1pl3
-DATE="Dec. 2007"
+VERSION=8.2beta3
+DATE="Jun. 2008"
 
 # a local which command for sh
 which () {
@@ -23,53 +23,54 @@ done
 }
 
 usage () {
-    echo -e "Available options for configure are:\n"
+    echo "Available options for configure are:\n"
     echo "-help"
-    echo -e "\tDisplays this help page\n"
+    printf "\tDisplays this help page\n"
     echo "-prefix <dir>"
-    echo -e "\tSet installation directory to <dir>\n"
+    printf "\tSet installation directory to <dir>\n"
     echo "-local"
-    echo -e "\tSet installation directory to the current source tree\n"
+    printf "\tSet installation directory to the current source tree\n"
     echo "-src"
-    echo -e "\tSpecifies the source directory\n"
+    printf "\tSpecifies the source directory\n"
     echo "-bindir"
     echo "-libdir"
     echo "-mandir"
-    echo -e "\tSpecifies where to install bin/lib/man files resp.\n"
+    echo "-docdir"
+    printf "\tSpecifies where to install bin/lib/man/doc files resp.\n"
     echo "-emacslib"
     echo "-emacs"
-    echo -e "\tSpecifies where emacs files are to be installed\n"
+    printf "\tSpecifies where emacs files are to be installed\n"
     echo "-coqdocdir"
-    echo -e "\tSpecifies where Coqdoc style files are to be installed\n"
+    printf "\tSpecifies where Coqdoc style files are to be installed\n"
     echo "-camldir"
-    echo -e "\tSpecifies the path to the OCaml library\n"
+    printf "\tSpecifies the path to the OCaml library\n"
     echo "-lablgtkdir"
-    echo -e "\tSpecifies the path to the Lablgtk library\n"
+    printf "\tSpecifies the path to the Lablgtk library\n"
     echo "-camlp5dir"
-    echo -e "\tSpecifies where to look for the Camlp5 library and tells to use it\n"
+    printf "\tSpecifies where to look for the Camlp5 library and tells to use it\n"
     echo "-arch"
-    echo -e "\tSpecifies the architecture\n"
+    printf "\tSpecifies the architecture\n"
     echo "-opt"
-    echo -e "\tSpecifies whether or not to generate optimized executables\n"
+    printf "\tSpecifies whether or not to generate optimized executables\n"
     echo "-fsets (all|basic)"
     echo "-reals (all|basic)"
-    echo -e "Specifies whether or not to compile full FSets/Reals library\n"
+    printf "\tSpecifies whether or not to compile full FSets/Reals library\n"
     echo "-coqide (opt|byte|no)"
-    echo -e "\tSpecifies whether or not to compile Coqide\n"
+    printf "\tSpecifies whether or not to compile Coqide\n"
     echo "-with-geoproof (yes|no)"
-    echo -e "\tSpecifies whether or not to use Geoproof binding\n"
+    printf "\tSpecifies whether or not to use Geoproof binding\n"
     echo "-with-cc <file>"
     echo "-with-ar <file>"
     echo "-with-ranlib <file>"
-    echo -e "\tTells configure where to find gcc/ar/ranlib executables\n"
+    printf "\tTells configure where to find gcc/ar/ranlib executables\n"
     echo "-byte-only"
-    echo -e "\tCompiles only bytecode version of Coq\n"
+    printf "\tCompiles only bytecode version of Coq\n"
     echo "-debug"
-    echo -e "\tAdd debugging information in the Coq executables\n"
+    printf "\tAdd debugging information in the Coq executables\n"
     echo "-profile"
-    echo -e "\tAdd profiling information in the Coq executables\n"
+    printf "\tAdd profiling information in the Coq executables\n"
     echo "-annotate"
-    echo -e "\tCompiles Coq with -dtypes option"
+    printf "\tCompiles Coq with -dtypes option\n"
 }
 
 
@@ -86,9 +87,9 @@ camlp4oexec=camlp4o
 
 
 coq_debug_flag=
+coq_debug_flag_opt=
 coq_profile_flag=
 coq_annotate_flag=
-coq_inline_flag=
 best_compiler=opt
 cflags="-fno-defer-pop -Wall -Wno-unused"
 
@@ -102,14 +103,13 @@ prefix_spec=no
 bindir_spec=no
 libdir_spec=no
 mandir_spec=no
+docdir_spec=no
 emacslib_spec=no
 emacs_spec=no
 camldir_spec=no
 lablgtkdir_spec=no
 coqdocdir_spec=no
-fsets_opt=no
 fsets=all
-reals_opt=no
 reals=all
 arch_spec=no
 coqide_spec=no
@@ -127,9 +127,7 @@ while : ; do
     -prefix|--prefix) prefix_spec=yes
                       prefix="$2"
 		      shift;;
-    -local|--local) local=true
-		    reals_opt=yes
-		    reals=all;;
+    -local|--local) local=true;;
     -src|--src) src_spec=yes
                 COQSRC="$2"
 	        shift;;
@@ -142,6 +140,9 @@ while : ; do
     -mandir|--mandir) mandir_spec=yes
                       mandir="$2"
 		      shift;;
+    -docdir|--docdir) docdir_spec=yes
+                      docdir="$2"
+		      shift;;
     -emacslib|--emacslib) emacslib_spec=yes
                           emacslib="$2"
 			  shift;;
@@ -166,14 +167,12 @@ while : ; do
     -opt|--opt) bytecamlc=ocamlc.opt
                 camlp4oexec=camlp4o  # can't add .opt since dyn load'll be required
                 nativecamlc=ocamlopt.opt;;
-    -fsets|--fsets) fsets_opt=yes
-                    case "$2" in
+    -fsets|--fsets) case "$2" in
 			yes|all) fsets=all;;
 			*) fsets=basic
 		    esac
 		    shift;;
-    -reals|--reals) reals_opt=yes
-	            case "$2" in
+    -reals|--reals) case "$2" in
 			yes|all) reals=all;;
 			*) reals=basic
 		    esac
@@ -229,27 +228,29 @@ esac
 # Architecture
 
 case $arch_spec in
-    no) if test -x /bin/arch ; then
-	    ARCH=`/bin/arch`
-	elif test -x /usr/bin/arch ; then
-	    ARCH=`/usr/bin/arch`
-	elif test -x /usr/ucb/arch ; then
-	    ARCH=`/usr/ucb/arch`
-	elif test -x /bin/uname && (/bin/uname -s | grep -q -i CYGWIN) ; then
-	    ARCH=win32
-	    # cygwin returns a name of the form /cygdrive/c/... 
-	    # that coqc does not understand; need to transform it
-	    COQTOP=`echo $COQTOP | sed -e "s#.*cygdrive.\(.\)#\1:#"`
-	elif test -x /bin/uname ; then
-	    ARCH=`/bin/uname -s`
-	elif test -x /usr/bin/uname ; then
-	    ARCH=`/usr/bin/uname -s`
+    no) 
+    # First we test if we are running a Cygwin system
+    if [ `uname -s | cut -c -6` = "CYGWIN" ] ; then
+	ARCH="win32"
+    else
+	# If not, we determine the architecture
+	if test -x /bin/arch ; then
+ 	    ARCH=`/bin/arch`
+ 	elif test -x /usr/bin/arch ; then
+ 	    ARCH=`/usr/bin/arch`
+ 	elif test -x /usr/ucb/arch ; then
+ 	    ARCH=`/usr/ucb/arch`
+ 	elif test -x /bin/uname ; then
+ 	    ARCH=`/bin/uname -s`
+ 	elif test -x /usr/bin/uname ; then
+ 	    ARCH=`/usr/bin/uname -s`
 	else
 	    echo "I can not automatically find the name of your architecture"
 	    echo -n\
-              "Give me a name, please [win32 for Win95, Win98 or WinNT]: "
+		"Give me a name, please [win32 for Win95, Win98 or WinNT]: "
 	    read ARCH
-	fi;;
+	fi
+    fi;;
     yes) ARCH=$arch
 esac
 
@@ -267,20 +268,59 @@ case $ARCH in
 	# true -> strip : it exists under cygwin !
 	STRIPCOMMAND="strip";; 
     *)
-    if [ "$coq_profile_flag" = "-p" ] ; then
+    if [ "$coq_profile_flag" = "-p" ] || [ "$coq_debug_flag" = "-g" ]; then
 	STRIPCOMMAND="true"
     else
 	STRIPCOMMAND="strip"
     fi
 esac
 
-# Is the source tree checked out from svn ?
+# Is the source tree checked out from a recognised
+# version control system ?
 if test -e .svn/entries ; then 
-    checkedout=1
-else 
+    checkedout=svn
+elif [ -d '{arch}' ]; then
+    checkedout=gnuarch
+elif [ -z "${GIT_DIR}" ] && [ -d .git ] || [ -d "${GIT_DIR}" ]; then
+    checkedout=git
+else
     checkedout=0
 fi
 
+# make command
+
+MAKE=`which make`
+if [ "$MAKE" != "" ]; then
+  MAKEVERSION=`$MAKE -v | head -1`
+  case $MAKEVERSION in
+    "GNU Make 3.81") 
+      echo "You have GNU Make 3.81. Good!";;
+    *)
+      OK="no"
+      if [ -x ./make ]; then
+	  MAKEVERSION=`./make -v | head -1`
+	  if [ "$MAKEVERSION" == "GNU Make 3.81" ]; then OK="yes"; fi
+      fi
+      if [ $OK = "no" ]; then
+	  echo "GNU Make >= 3.81 is needed"
+	  echo "Make 3.81 can be downloaded from ftp://ftp.gnu.org/gnu/make/make-3.81.tar.gz"
+	  echo "then locally installed on a Unix-style system by issuing:"
+	  echo "  tar xzvf make-3.81.tar.gz"
+	  echo "  cd make-3.81"
+          echo "  ./configure"
+          echo "  make"
+          echo "  mv make .."
+	  echo "  cd .."
+	  echo "Restart then the configure script and later use ./make instead of make"
+	  exit 1
+      else
+	  echo "You have locally installed GNU Make 3.81. Good!"
+      fi
+  esac
+else
+  echo "Cannot find GNU Make 3.81"
+fi
+
 #########################################
 # Objective Caml programs
 
@@ -340,12 +380,7 @@ case $CAMLVERSION in
 	fi
 	echo "Configuration script failed!"
 	exit 1;;
-    3.07*)
-        cflags="$cflags -DOCAML_307"
-	coq_inline_flag="-inline 0"
-	echo "You have Objective-Caml $CAMLVERSION. Good!";;
-    3.08*)
-	coq_inline_flag="-inline 0"
+    3.07*|3.08*)
 	echo "You have Objective-Caml $CAMLVERSION. Good!";;
     ?*)
 	CAMLP4COMPAT="-loc loc" 
@@ -359,29 +394,6 @@ esac
 
 CAMLTAG=OCAML`echo $CAMLVERSION | sed -e "s/\([1-9]\)\.\([0-9]*\).*/\1\2/g"`
 
-# do we have a native compiler: test of ocamlopt and its version
-
-if [ "$best_compiler" = "opt" ] ; then
-  if test -e `which "$nativecamlc"` ; then
-      CAMLOPTVERSION=`"$nativecamlc" -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `
-      if [ "`uname -s`" = "Darwin" -a "$ARCH" = "i386" ]; then
-	  case $CAMLOPTVERSION in
-	      3.09.3|3.1?*) ;;
-	      *) echo "Native compilation on MacOS X Pentium requires Objective-Caml >= 3.09.3,"
-		 best_compiler=byte
-		 echo "only the bytecode version of Coq will be available."
-	  esac
-      elif [ "$CAMLOPTVERSION" != "$CAMLVERSION" ] ; then
-	  echo "Native and bytecode compilers do not have the same version!";
-      fi
-      echo "You have native-code compilation. Good!"
-  else
-      best_compiler=byte
-      echo "You have only bytecode compilation."
-  fi
-fi
-
-
 # For coqmktop & bytecode compiler
 
 case $ARCH in
@@ -389,16 +401,35 @@ case $ARCH in
       CAMLLIB=`"$CAMLC" -where | sed -e 's/^\(.*\)$/\1/'` ;;
     *)
       CAMLLIB=`"$CAMLC" -where`
-  esac
-  
+esac
+
+# We need to set va special flag for OCaml 3.07
+case  $CAMLVERSION in 
+	3.07*)
+	  cflags="$cflags -DOCAML_307";;
+esac
+
+if [ "$CAMLTAG" = "OCAML310" ] && [ "$coq_debug_flag" = "-g" ]; then
+    # Compilation debug flag
+    coq_debug_flag_opt="-g"
+fi
 
 # Camlp4 / Camlp5 configuration
-# Very basic for the moment: if camlp5 exists, we use it...
 
 if [ "$camlp5dir" != "" ]; then
     CAMLP4=camlp5
     CAMLP4LIB=$camlp5dir
+    if [ ! -f $camlp5dir/camlp5.cma ]; then
+	echo "Cannot find camlp5 libraries in $camlp5dir (camlp5.cma not found)"
+	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."
+	exit 1
+    fi
 elif [ "$CAMLTAG" = "OCAML310" ]; then
     if [ -x "${CAMLLIB}/camlp5" ]; then 
         CAMLP4LIB=+camlp5
@@ -411,6 +442,11 @@ elif [ "$CAMLTAG" = "OCAML310" ]; then
     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
 else 
     CAMLP4=camlp4
     CAMLP4LIB=+camlp4
@@ -432,6 +468,33 @@ esac
 # (this should become configurable some day) 
 CAMLP4BIN=${CAMLBIN}
 
+# 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 [ "`uname -s`" = "Darwin" -a "$ARCH" = "i386" ]; then
+	  case $CAMLOPTVERSION in
+	      3.09.3|3.1?*) ;;
+	      *) echo "Native compilation on MacOS X Pentium requires Objective-Caml >= 3.09.3,"
+		 best_compiler=byte
+		 echo "only the bytecode version of Coq will be available."
+	  esac
+      elif [ ! -f $FULLCAMLP4LIB/gramlib.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!"
+      fi
+  else
+      best_compiler=byte
+      echo "You have only bytecode compilation."
+  fi
+fi
 
 # OS dependent libraries
 
@@ -518,7 +581,7 @@ case $ARCH in
 	# true -> strip : it exists under cygwin !
 	STRIPCOMMAND="strip";; 
     *)
-    if [ "$coq_profile_flag" = "-p" ] ; then
+    if [ "$coq_profile_flag" = "-p" ] || [ "$coq_debug_flag" = "-g" ]; then
 	STRIPCOMMAND="true"
     else
 	STRIPCOMMAND="strip"
@@ -532,7 +595,7 @@ esac
 #esac
 
 ###########################################
-# bindir, libdir, mandir, etc.
+# bindir, libdir, mandir, docdir, etc.
 
 case $src_spec in
   no) COQTOP=${COQSRC}
@@ -548,14 +611,16 @@ case $ARCH in
 	 bindir_def='C:\coq\bin'
 	 libdir_def='C:\coq\lib'
 	 mandir_def='C:\coq\man'
+	 docdir_def='C:\coq\doc'
 	 emacslib_def='C:\coq\emacs'
          coqdocdir_def='C:\coq\latex';;
   *)
 	 bindir_def=/usr/local/bin
 	 libdir_def=/usr/local/lib/coq
 	 mandir_def=/usr/local/man
-	 emacslib_def=/usr/share/emacs/site-lisp
-         coqdocdir_def=/usr/share/texmf/tex/latex/misc;;
+	 docdir_def=/usr/local/share/doc
+	 emacslib_def=/usr/local/share/emacs/site-lisp
+         coqdocdir_def=/usr/local/share/texmf/tex/latex/misc;;
 esac
 
 emacs_def=emacs
@@ -600,6 +665,18 @@ case $mandir_spec/$prefix_spec/$local in
 	esac;;
 esac
 
+case $docdir_spec/$prefix_spec/$local in
+    yes/*/*) DOCDIR=$docdir;;
+    */yes/*) DOCDIR=$prefix/share/doc ;;
+    */*/true) DOCDIR=$COQTOP/man ;;
+    *)  echo "Where should I install the Coq documentation [$docdir_def] ?"
+        read DOCDIR
+	case $DOCDIR in
+	    "") DOCDIR=$docdir_def;;
+	    *) true;;
+	esac;;
+esac
+
 case $emacslib_spec/$prefix_spec/$local in
     yes/*/*) EMACSLIB=$emacslib;;
     */yes/*)
@@ -632,18 +709,6 @@ case $coqdocdir_spec/$prefix_spec/$local in
 	esac;;
 esac
 
-case $reals_opt in
-    no) echo "Should I compile the complete theory of real analysis [Y/N, default is Y] ?"
-	read reals_ans
-
-	case $reals_ans in
-	    "N"|"n"|"No"|"NO"|"no")
-		    reals=basic;;
-		*) reals=all;;
-	esac;;
-    yes) true;;
-esac
-
 # case $emacs_spec in
 #     no) echo "Which Emacs command should I use to compile coq.el [$emacs_def] ?"
 #         read EMACS
@@ -686,10 +751,11 @@ echo "  CoqIde                            : $COQIDE"
 echo ""
 
 echo "  Paths for true installation:"
-echo "    binaries   will be copied in $BINDIR"
-echo "    library    will be copied in $LIBDIR"
-echo "    man pages  will be copied in $MANDIR"
-echo "    emacs mode will be copied in $EMACSLIB"
+echo "    binaries      will be copied in $BINDIR"
+echo "    library       will be copied in $LIBDIR"
+echo "    man pages     will be copied in $MANDIR"
+echo "    documentation will be copied in $MANDIR"
+echo "    emacs mode    will be copied in $EMACSLIB"
 echo ""
 
 #####################################################
@@ -712,6 +778,7 @@ case $ARCH in
 	ESCCAMLDIR=`echo $CAMLBIN |sed -e 's|\\\|\\\\\\\|g'`
 	ESCCAMLLIB=`echo $CAMLLIB |sed -e 's|\\\|\\\\\\\|g'`
   	ESCMANDIR=`echo $MANDIR |sed -e 's|\\\|\\\\\\\|g'`
+  	ESCDOCDIR=`echo $DOCDIR |sed -e 's|\\\|\\\\\\\|g'`
    	ESCEMACSLIB=`echo $EMACSLIB |sed -e 's|\\\|\\\\\\\|g'`
    	ESCCOQDOCDIR=`echo $COQDOCDIR |sed -e 's|\\\|\\\\\\\|g'`
    	ESCCAMLP4BIN=`echo $CAMLP4BIN |sed -e 's|\\\|\\\\\\\|g'`
@@ -725,6 +792,7 @@ case $ARCH in
 	ESCCAMLDIR="$CAMLBIN"
 	ESCCAMLLIB="$CAMLLIB"
   	ESCMANDIR="$MANDIR"
+  	ESCDOCDIR="$DOCDIR"
    	ESCEMACSLIB="$EMACSLIB"
    	ESCCOQDOCDIR="$COQDOCDIR"
    	ESCCAMLP4BIN="$CAMLP4BIN"
@@ -763,7 +831,7 @@ PRINTF=`which printf`
 
 # Subdirectories of theories/ added in coq_config.ml
 subdirs () {
-    (cd $1; find * -type d ! -name .svn -exec $PRINTF "\"%s\";\n" {} \; | grep -v extraction/test | grep -v correctness >> "$mlconfig_file")
+    (cd $1; find * \( -name .svn -prune \) -o \( -type d -exec $PRINTF "\"%s\";\n" {} \; \) | grep -v correctness >> "$mlconfig_file")
 }
 
 echo "let theories_dirs = [" >> "$mlconfig_file"
@@ -789,6 +857,7 @@ sed -e "s|LOCALINSTALLATION|$local|" \
     -e "s|BINDIRDIRECTORY|$ESCBINDIR|" \
     -e "s|COQLIBDIRECTORY|$ESCLIBDIR|" \
     -e "s|MANDIRDIRECTORY|$ESCMANDIR|" \
+    -e "s|DOCDIRDIRECTORY|$ESCDOCDIR|" \
     -e "s|EMACSLIBDIRECTORY|$ESCEMACSLIB|" \
     -e "s|EMACSCOMMAND|$EMACS|" \
     -e "s|COQDOCDIRECTORY|$ESCCOQDOCDIR|" \
@@ -803,15 +872,16 @@ sed -e "s|LOCALINSTALLATION|$local|" \
     -e "s|CAMLP4TOOL|$camlp4oexec|" \
     -e "s|CAMLP4COMPATFLAGS|$CAMLP4COMPAT|" \
     -e "s|LABLGTKINCLUDES|$ESCLABLGTKINCLUDES|" \
+    -e "s|COQDEBUGFLAGOPT|$coq_debug_flag_opt|" \
     -e "s|COQDEBUGFLAG|$coq_debug_flag|" \
     -e "s|COQPROFILEFLAG|$coq_profile_flag|" \
-    -e "s|COQINLINEFLAG|$coq_inline_flag|" \
     -e "s|CAMLANNOTATEFLAG|$coq_annotate_flag|" \
     -e "s|CCOMPILEFLAGS|$cflags|" \
     -e "s|BESTCOMPILER|$best_compiler|" \
     -e "s|EXECUTEEXTENSION|$EXE|" \
     -e "s|BYTECAMLC|$bytecamlc|" \
     -e "s|NATIVECAMLC|$nativecamlc|" \
+    -e "s|OCAMLEXEC|$ocamlexec|" \
     -e "s|OCAMLDEPEXEC|$ocamldepexec|" \
     -e "s|OCAMLDOCEXEC|$ocamldocexec|" \
     -e "s|OCAMLLEXEXEC|$ocamllexexec|" \
@@ -866,4 +936,4 @@ echo
 echo "*Warning* To compile the system for a new architecture"
 echo "          don't forget to do a 'make archclean' before './configure'."
 
-# $Id: configure 10375 2007-12-13 15:02:01Z notin $
+# $Id: configure 11181 2008-06-27 07:35:45Z notin $