Imported Upstream version 8.1~gammaupstream/8.1.gamma

1 files changed, 184 insertions, 59 deletions

diff --git a/configure b/configure
index 71217486..1db98577 100755
--- a/configure
+++ b/configure
@@ -6,8 +6,8 @@
 # 
 ##################################
 
-VERSION=8.1beta
-DATE="Jun 2006"
+VERSION=8.1gamma
+DATE="Nov. 2006"
 
 # a local which command for sh
 which () {
@@ -22,13 +22,75 @@ for i in $PATH; do
 done
 }
 
+usage () {
+    echo -e "Available options for configure are:\n"
+    echo "-help"
+    echo -e "\tDisplays this help page\n"
+    echo "-prefix <dir>"
+    echo -e "\tSet installation directory to <dir>\n"
+    echo "-local"
+    echo -e "\tSet installation directory to the current source tree\n"
+    echo "-src"
+    echo -e "\tSpecifies the source directory\n"
+    echo "-bindir"
+    echo "-libdir"
+    echo "-mandir"
+    echo -e "\tSpecifies where to install bin/lib/man files resp.\n"
+    echo "-emacslib"
+    echo "-emacs"
+    echo -e "\tSpecifies where emacs files are to be installed\n"
+    echo "-coqdocdir"
+    echo -e "\tSpecifies where Coqdoc style files are to be installed\n"
+    echo "-camldir"
+    echo -e "\tTells configure where to look for OCaml files\n"
+    echo "-arch"
+    echo -e "\tSpecifies the architecture\n"
+    echo "-opt"
+    echo -e "\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"
+    echo "-coqide (opt|byte|no)"
+    echo -e "\tSpecifies whether or not to compile Coqide\n"
+    echo "-with-geoproof (yes|no)"
+    echo -e "\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"
+    echo "-byte-only"
+    echo -e "\tCompiles only bytecode version of Coq\n"
+    echo "-debug"
+    echo -e "\tAdd debugging information in the Coq executables\n"
+    echo "-profile"
+    echo -e "\tAdd profiling information in the Coq executables\n"
+    echo "-annotate"
+    echo -e "\tCompiles Coq with -dtypes option"
+}
+
+
+# Default OCaml binaries
 bytecamlc=ocamlc
 nativecamlc=ocamlopt
-camlp4o=camlp4o
+ocamlexec=ocaml
+ocamldepexec=ocamldep
+ocamldocexec=ocamldoc
+ocamllexexec=ocamllex
+ocamlyaccexec=ocamlyacc
+ocamlmktopexec=ocamlmktop
+camlp4oexec=camlp4o
+
+
 coq_debug_flag=
 coq_profile_flag=
+coq_annotate_flag=
+coq_inline_flag=
 best_compiler=opt
 
+gcc_exec=gcc
+ar_exec=ar
+ranlib_exec=ranlib
+
 local=false
 src_spec=no
 prefix_spec=no
@@ -37,6 +99,7 @@ libdir_spec=no
 mandir_spec=no
 emacslib_spec=no
 emacs_spec=no
+camldir_spec=no
 coqdocdir_spec=no
 fsets_opt=no
 fsets=all
@@ -44,16 +107,18 @@ reals_opt=no
 reals=all
 arch_spec=no
 coqide_spec=no
-with_geoproof=true
+with_geoproof=false
 
 # COQTOP=`pwd`
-
+COQSRC=`pwd`
 
 # Parse command-line arguments
 
 while : ; do
   case "$1" in
     "") break;;
+    -help|--help) usage
+	          exit;;
     -prefix|--prefix) prefix_spec=yes
                       prefix="$2"
 		      shift;;
@@ -81,20 +146,32 @@ while : ; do
     -coqdocdir|--coqdocdir) coqdocdir_spec=yes
 	              coqdocdir="$2"
 		      shift;;
+    -camldir|--camldir) camldir_spec=yes
+	                camldir="$2"
+			shift;;
     -arch|--arch) arch_spec=yes
                   arch=$2
 		  shift;;
     -opt|--opt) bytecamlc=ocamlc.opt
-                camlp4o=camlp4o  # can't add .opt since dyn load'll be required
+                camlp4oexec=camlp4o  # can't add .opt since dyn load'll be required
                 nativecamlc=ocamlopt.opt;;
     -fsets|--fsets) fsets_opt=yes
-                    fsets=$2
+                    case "$2" in
+			yes|all) fsets=all;;
+			*) fsets=basic
+		    esac
 		    shift;;
     -reals|--reals) reals_opt=yes
-		    reals=$2
+	            case "$2" in
+			yes|all) reals=all;;
+			*) reals=basic
+		    esac
 		    shift;;
     -coqide|--coqide) coqide_spec=yes
-		      COQIDE=$2
+		      case "$2" in
+			  byte|opt) COQIDE=$2;;
+			  *) COQIDE=no
+		      esac
 		      shift;;
     -with-geoproof|--with-geoproof) 
 	  case $2 in
@@ -102,10 +179,23 @@ while : ; do
 	      no) with_geoproof=false;;
 	  esac
 	  shift;;
+    -with-cc|-with-gcc|--with-cc|--with-gcc) 
+	  gcc_spec=yes
+	  gcc_exec=$2
+	  shift;;
+    -with-ar|--with-ar) 
+	  ar_spec=yes
+	  ar_exec=$2
+	  shift;;
+    -with-ranlib|--with-ranlib) 
+	  ranlib_spec=yes
+	  ranlib_exec=$2
+	  shift;;
     -byte-only|-byteonly|--byteonly|--byte-only) best_compiler=byte;;
     -debug|--debug) coq_debug_flag=-g;;
     -profile|--profile) coq_profile_flag=-p;;
-     *) echo "Unknown option \"$1\"." 1>&2; exit 2;;
+    -annotate|--annotate) coq_annotate_flag=-dtypes;;
+    *) echo "Unknown option \"$1\"." 1>&2; usage; exit 2;;
   esac
   shift
 done
@@ -171,50 +261,71 @@ case $ARCH in
     fi
 esac
 
+# Is the source tree checked out from svn ?
+if test -e .svn/entries ; then 
+    checkedout=1
+else 
+    checkedout=0
+fi
+
 #########################################
 # Objective Caml programs
 
-CAMLC=`which $bytecamlc`
-case "$CAMLC" in
-	"") echo "$bytecamlc is not present in your path !"
-	echo "Give me manually the path to the $bytecamlc executable [/usr/local/bin by default]: "
-	read CAMLC
-	
+case $camldir_spec in
+    no) CAMLC=`which $bytecamlc`
 	case "$CAMLC" in
-		"") CAMLC=/usr/local/bin/$bytecamlc;;
-		*/ocamlc|*/ocamlc.opt) true;;
-		*/) CAMLC="${CAMLC}"$bytecamlc;;
-		*) CAMLC="${CAMLC}"/$bytecamlc;;
+	    "") echo "$bytecamlc is not present in your path !"
+		echo "Give me manually the path to the $bytecamlc executable [/usr/local/bin by default]: "
+		read CAMLC
+		
+		case "$CAMLC" in
+		    "") CAMLC=/usr/local/bin/$bytecamlc;;
+		    */ocamlc|*/ocamlc.opt) true;;
+		    */) CAMLC="${CAMLC}"$bytecamlc;;
+		    *) CAMLC="${CAMLC}"/$bytecamlc;;
+		esac
 	esac
-	bytecamlc="$CAMLC"
-	nativecamlc=`dirname "$CAMLC"`/$nativecamlc;;
+	CAMLBIN=`dirname "$CAMLC"`;;
+    yes) CAMLC=$camldir/$bytecamlc
+        
+         CAMLBIN=`dirname "$CAMLC"`
+	 bytecamlc="$CAMLC"
+	 nativecamlc=$CAMLBIN/$nativecamlc
+	 ocamlexec=$CAMLBIN/ocaml
+	 ocamldepexec=$CAMLBIN/ocamldep
+	 ocamldocexec=$CAMLBIN/ocamldoc
+	 ocamllexexec=$CAMLBIN/ocamllex
+	 ocamlyaccexec=$CAMLBIN/ocamlyacc
+	 camlmktopexec=$CAMLBIN/ocamlmktop
+	 camlp4oexec=$CAMLBIN/camlp4o
 esac
 
 if test ! -f "$CAMLC" ; then
-	echo "I can not find the executable '$CAMLC'! (Have you installed it?)"
-	echo "Configuration script failed!"
-	exit 1
+    echo "I can not find the executable '$CAMLC'! (Have you installed it?)"
+    echo "Configuration script failed!"
+    exit 1
 fi
 
-CAMLBIN=`dirname "$CAMLC"`
-CAMLVERSION=`"$CAMLC" -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `
+
+CAMLVERSION=`"$bytecamlc" -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `
 
 case $CAMLVERSION in
-  1.*|2.*|3.00|3.01|3.02|3.03|3.03alpha|3.04|3.05beta|3.05|3.08.0)
+    1.*|2.*|3.00|3.01|3.02|3.03|3.03alpha|3.04|3.05beta|3.05|3.08.0)
 	echo "Your version of Objective-Caml is $CAMLVERSION."
 	if [ "$CAMLVERSION" = "3.08.0" ] ; then
-	  echo "You need Objective-Caml 3.06 or later (to the exception of 3.08.0)!"
+	    echo "You need Objective-Caml 3.06 or later (to the exception of 3.08.0)!"
 	else
-	  echo "You need Objective-Caml 3.06 or later!";
+	    echo "You need Objective-Caml 3.06 or later!"
 	fi
 	echo "Configuration script failed!"
 	exit 1;;
-  3.06|3.07*|3.08*)
-	echo "You have Objective-Caml $CAMLVERSION. Good!";;
-  ?*)
+    3.06|3.07*|3.08*)
+	echo "You have Objective-Caml $CAMLVERSION. Good!"
+	coq_inline_flag="-inline 0";;
+    ?*)
 	CAMLP4COMPAT="-loc loc" 
 	echo "You have Objective-Caml $CAMLVERSION. Good!";;
-  *)
+    *)
 	echo "I found the Objective-Caml compiler but cannot find its version number!"
 	echo "Is it installed properly ?"
 	echo "Configuration script failed!"
@@ -226,17 +337,18 @@ 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
-  CAMLOPT=`which $nativecamlc`
-  case "$CAMLOPT" in
-    "") best_compiler=byte
-        echo "You have only bytecode compilation.";;
-    *) CAMLOPTVERSION=`"$CAMLOPT" -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `
-       if [ "$CAMLOPTVERSION" != "$CAMLVERSION" ] ; then \
-         echo "native and bytecode compilers do not have the same version!"; fi
-       echo "You have native-code compilation. Good!"
-  esac
+  if test -e `which "$nativecamlc"` ; then
+      CAMLOPTVERSION=`"$nativecamlc" -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `
+      if [ "$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
 
 CAMLLIB=`"$CAMLC" -where`
@@ -485,19 +597,20 @@ echo ""
 
 # An escaped version of a variable
 escape_var () {
-ocaml 2>&1 1>/dev/null <<EOF
+"$ocamlexec" 2>&1 1>/dev/null <<EOF
   prerr_endline(String.escaped(Sys.getenv"$VAR"));;
 EOF
 }
 
-export COQTOP BINDIR LIBDIR CAMLLIB
+export COQTOP BINDIR LIBDIR CAMLBIN CAMLLIB
 ESCCOQTOP="`VAR=COQTOP escape_var`"
 ESCBINDIR="`VAR=BINDIR escape_var`"
 ESCLIBDIR="`VAR=LIBDIR escape_var`"
+ESCCAMLDIR="`VAR=CAMLBIN escape_var`"
 ESCCAMLLIB="`VAR=CAMLLIB escape_var`"
 ESCCAMLP4LIB="$ESCCAMLLIB"/camlp4
 
-mlconfig_file=$COQTOP/config/coq_config.ml
+mlconfig_file="$COQSRC/config/coq_config.ml"
 rm -f $mlconfig_file
 cat << END_OF_COQ_CONFIG > $mlconfig_file
 (* DO NOT EDIT THIS FILE: automatically generated by ../configure *)
@@ -506,6 +619,7 @@ let local = $local
 let bindir = "$ESCBINDIR" 
 let coqlib = "$ESCLIBDIR"
 let coqtop = "$ESCCOQTOP"
+let camldir = "$ESCCAMLDIR"
 let camllib = "$ESCCAMLLIB"
 let camlp4lib = "$ESCCAMLP4LIB"
 let best = "$best_compiler"
@@ -525,25 +639,25 @@ 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 * -type d ! -name .svn -exec $PRINTF "\"%s\";\n" {} \; | grep -v extraction/test | grep -v correctness >> "$mlconfig_file")
 }
 
-echo "let theories_dirs = [" >> $mlconfig_file
+echo "let theories_dirs = [" >> "$mlconfig_file"
 subdirs theories
-echo "]" >> $mlconfig_file
+echo "]" >> "$mlconfig_file"
 
-echo "let contrib_dirs = [" >> $mlconfig_file
+echo "let contrib_dirs = [" >> "$mlconfig_file"
 subdirs contrib
-echo "]" >> $mlconfig_file
+echo "]" >> "$mlconfig_file"
 
-chmod a-w $mlconfig_file
+chmod a-w "$mlconfig_file"
 
 
 ###############################################
 # Building the $COQTOP/config/Makefile file
 ###############################################
 
-rm -f $COQTOP/config/Makefile
+rm -f "$COQSRC/config/Makefile"
 
 # damned backslashes under M$Windows (bis)
 case $ARCH in
@@ -579,25 +693,36 @@ sed -e "s|LOCALINSTALLATION|$local|" \
     -e "s|ARCHITECTURE|$ARCH|" \
     -e "s|OSDEPENDENTLIBS|$OSDEPLIBS|" \
     -e "s|OSDEPENDENTP4OPTFLAGS|$OSDEPP4OPTFLAGS|" \
-    -e "s|CAMLLIBDIRECTORY|$CAMLLIB|" \
+    -e "s|CAMLLIBDIRECTORY|$ESCCAMLLIB|" \
     -e "s|CAMLTAG|$CAMLTAG|" \
     -e "s|CAMLP4BINDIRECTORY|$ESCCAMLP4BIN|" \
     -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIB|" \
-    -e "s|CAMLP4TOOL|$camlp4o|" \
+    -e "s|CAMLP4TOOL|$camlp4oexec|" \
     -e "s|CAMLP4COMPATFLAGS|$CAMLP4COMPAT|" \
     -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|BESTCOMPILER|$best_compiler|" \
     -e "s|EXECUTEEXTENSION|$EXE|" \
     -e "s|BYTECAMLC|$bytecamlc|" \
     -e "s|NATIVECAMLC|$nativecamlc|" \
+    -e "s|OCAMLDEPEXEC|$ocamldepexec|" \
+    -e "s|OCAMLDOCEXEC|$ocamldocexec|" \
+    -e "s|OCAMLLEXEXEC|$ocamllexexec|" \
+    -e "s|OCAMLYACCEXEC|$ocamlyaccexec|" \
+    -e "s|CAMLMKTOPEXEC|$camlmktopexec|" \
+    -e "s|CCEXEC|$gcc_exec|" \
+    -e "s|AREXEC|$ar_exec|" \
+    -e "s|RANLIBEXEC|$ranlib_exec|" \
     -e "s|STRIPCOMMAND|$STRIPCOMMAND|" \
     -e "s|FSETSOPT|$fsets|" \
     -e "s|REALSOPT|$reals|" \
     -e "s|COQIDEOPT|$COQIDE|" \
-      $COQTOP/config/Makefile.template > $COQTOP/config/Makefile
+    -e "s|CHECKEDOUTSOURCETREE|$checkedout|" \
+      "$COQSRC/config/Makefile.template" > "$COQSRC/config/Makefile"
 
-chmod a-w $COQTOP/config/Makefile
+chmod a-w "$COQSRC/config/Makefile"
 
 ##################################################
 # Building the $COQTOP/dev/ocamldebug-coq file
@@ -625,7 +750,7 @@ fi
 ####################################################
 
 if [ "$LABLGTKGE26" = "yes" ] ; then
-  cp -f ide/undo_lablgtk_ge26.mli ide/undo.mli;
+  cp -f ide/undo_lablgtk_ge26.mli ide/undo.mli
 else
   cp -f ide/undo_lablgtk_lt26.mli ide/undo.mli
 fi
@@ -639,4 +764,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 8961 2006-06-15 15:22:05Z notin $
+# $Id: configure 9353 2006-11-07 16:18:57Z notin $