Imported Upstream version 8.0pl1upstream/8.0pl1

1 files changed, 542 insertions, 0 deletions

diff --git a/configure b/configure
new file mode 100755
index 00000000..923eee76
--- /dev/null
+++ b/configure
@@ -0,0 +1,542 @@
+#!/bin/sh
+
+##################################
+#
+#  Configuration script for Coq
+# 
+##################################
+
+VERSION=8.0pl1
+DATE="Jul 2004"
+
+# a local which command for sh
+which () {
+IFS=":" # set words separator in PATH to be ':' (it allows spaces in dirnames)
+for i in $PATH; do
+  if test -z "$i"; then i=.; fi 
+  if [ -f "$i/$1" ] ; then
+	IFS=" "
+        echo "$i/$1"
+	break
+  fi
+done
+}
+
+bytecamlc=ocamlc
+nativecamlc=ocamlopt
+camlp4o=camlp4o
+coq_debug_flag=
+coq_profile_flag=
+best_compiler=opt
+
+local=false
+bindir_spec=no
+libdir_spec=no
+mandir_spec=no
+emacslib_spec=no
+emacs_spec=no
+coqdocdir_spec=no
+reals_opt=no
+reals=all
+arch_spec=no
+coqide_spec=no
+
+COQTOP=`pwd`
+
+
+# Parse command-line arguments
+
+while : ; do
+  case "$1" in
+    "") break;;
+    -prefix|--prefix) bindir_spec=yes
+                      bindir=$2/bin
+                      libdir_spec=yes
+		      libdir=$2/lib/coq
+                      mandir_spec=yes
+		      mandir=$2/man
+		      coqdocdir_spec=yes
+		      coqdocdir=$2/share/texmf/tex/latex/misc
+		      shift;;
+    -local|--local) local=true
+                    bindir_spec=yes
+                    bindir=$COQTOP/bin
+                    libdir_spec=yes
+		    libdir=$COQTOP
+                    mandir_spec=yes
+		    mandir=$COQTOP/man
+                    emacslib_spec=yes
+		    emacslib=$COQTOP/tools/emacs
+		    coqdocdir_spec=yes
+		    coqdocdir=$COQTOP/tools/coqdoc
+		    reals_opt=yes
+		    reals=all;;
+    -src|--src) COQTOP=$2
+	        shift;;
+    -bindir|--bindir) bindir_spec=yes
+                      bindir=$2
+		      shift;;
+    -libdir|--libdir) libdir_spec=yes
+                      libdir=$2
+		      shift;;
+    -mandir|--mandir) mandir_spec=yes
+                      mandir=$2
+		      shift;;
+    -emacslib|--emacslib) emacslib_spec=yes
+                          emacslib=$2
+			  shift;;
+    -emacs |--emacs) emacs_spec=yes
+		     emacs=$2
+		     shift;;
+    -coqdocdir|--coqdocdir) coqdocdir_spec=yes
+	              coqdocdir=$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
+                nativecamlc=ocamlopt.opt;;
+    -reals|--reals) reals_opt=yes
+		    reals=$2
+		    shift;;
+    -coqide|--coqide) coqide_spec=yes
+		      COQIDE=$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;;
+  esac
+  shift
+done
+
+
+# compile date
+DATEPGM=`which date`
+case $DATEPGM in
+    "") echo "I can't find the program \"date\" in your path."
+        echo "Please give me the current date"
+	read COMPILEDATE;;
+    *)  COMPILEDATE=`date +"%h %d %Y %H:%M:%S"`;;
+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 /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]: "
+	    read ARCH
+	fi;;
+    yes) ARCH=$arch
+esac
+
+# bindir, libdir, mandir, etc.
+
+case $ARCH in
+  win32)
+	 bindir_def=C:\\coq\\bin
+	 libdir_def=C:\\coq\\lib
+	 mandir_def=C:\\coq\\man
+	 emacslib_def=C:\\coq\\emacs;;
+  *)
+	 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;;
+esac
+
+emacs_def=emacs
+
+case $bindir_spec in
+    no) echo "Where should I install the Coq binaries [$bindir_def] ?"
+        read BINDIR
+	
+	case $BINDIR in
+	    "") BINDIR=$bindir_def;;
+	    *) true;;
+	esac;;
+    yes) BINDIR=$bindir;;
+esac
+
+case $libdir_spec in
+    no) echo "Where should I install the Coq library [$libdir_def] ?"
+        read LIBDIR
+	
+	case $LIBDIR in
+	    "") LIBDIR=$libdir_def;;
+	    *) true;;
+	esac;;
+    yes) LIBDIR=$libdir;;
+esac
+
+case $mandir_spec in
+    no) echo "Where should I install the Coq man pages [$mandir_def] ?"
+        read MANDIR
+	
+	case $MANDIR in
+	    "") MANDIR=$mandir_def;;
+	    *) true;;
+	esac;;
+    yes) MANDIR=$mandir;;
+esac
+
+case $emacslib_spec in
+    no) echo "Where should I install the Coq Emacs mode [$emacslib_def] ?"
+        read EMACSLIB
+	
+	case $EMACSLIB in
+	    "") EMACSLIB=$emacslib_def;;
+	    *) true;;
+	esac;;
+    yes) EMACSLIB=$emacslib;;
+esac
+
+case $coqdocdir_spec in
+    no) echo "Where should I install Coqdoc TeX/LaTeX files [$coqdocdir_def] ?"
+        read COQDOCDIR
+	
+	case $COQDOCDIR in
+	    "") COQDOCDIR=$coqdocdir_def;;
+	    *) true;;
+	esac;;
+    yes) COQDOCDIR=$coqdocdir;;
+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
+	
+# 	case $EMACS in
+# 	    "") EMACS=$emacs_def;;
+# 	    *) true;;
+# 	esac;;
+#     yes) EMACS=$emacs;;
+# esac
+
+# OS dependent libraries
+
+case $ARCH in
+  sun4*) OS=`uname -r`
+	case $OS in
+	   5*) OS="Sun Solaris $OS"
+	       OSDEPLIBS="-cclib -lunix -cclib -lnsl -cclib -lsocket";;
+	   *) OS="Sun OS $OS"
+	      OSDEPLIBS="-cclib -lunix"
+        esac;;
+  alpha) OSDEPLIBS="-cclib -lunix";;
+  win32) OS="Win32" 
+	 OSDEPLIBS="-cclib -lunix";;
+  *) OSDEPLIBS="-cclib -lunix"
+esac
+
+# executable extension
+
+case $ARCH in
+    win32) EXE=".exe";;
+    *) EXE=""
+esac
+
+# 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 "$CAMLC" in
+		"") CAMLC=/usr/local/bin/$bytecamlc;;
+		*/ocamlc|*/ocamlc.opt) true;;
+		*/) CAMLC="${CAMLC}"$bytecamlc;;
+		*) CAMLC="${CAMLC}"/$bytecamlc;;
+	esac
+	bytecamlc="$CAMLC"
+	nativecamlc=`dirname "$CAMLC"`/$nativecamlc;;
+esac
+
+if test ! -f "$CAMLC" ; then
+	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' `
+
+case $CAMLVERSION in
+  1.*|2.*|3.00|3.01|3.02|3.03|3.03alpha|3.04|3.05beta|3.05)
+	echo "Your version of Objective-Caml is $CAMLVERSION."
+	echo "You need Objective-Caml 3.06 or later !"
+	echo "Configuration script failed!"
+	exit 1;;
+  ?*)	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!"
+     exit 1;;
+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
+  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
+fi
+
+# For coqmktop
+
+#CAMLLIB=`"$CAMLC" -v | sed -n -e 's|.*directory:* *\(.*\)$|\1|p' `
+CAMLLIB=`"$CAMLC" -where`
+
+# Camlp4 (greatly simplified since merged with ocaml)
+
+CAMLP4BIN=${CAMLBIN}
+
+#case $OS in
+#  Win32)
+    CAMLP4LIB=+camlp4
+# ;;
+#  *)
+#    CAMLP4LIB=${CAMLLIB}/camlp4
+#esac
+
+# lablgtk2 and CoqIDE
+
+if [ "$coqide_spec" = "no" ] ; then
+if test -x "${CAMLLIB}/lablgtk2" ; then
+    if grep -q -w convert_with_fallback "${CAMLLIB}/lablgtk2/glib.mli" ; then
+	if test -f "${CAMLLIB}/threads/threads.cmxa" ; then
+            echo "LablGtk2 found, native threads: native CoqIde will be available"
+	    COQIDE=opt;
+        else
+            echo "LablGtk2 found, no native threads: bytecode CoqIde will be available"
+	    COQIDE=byte
+	fi;
+    else
+        echo "LablGtk2 found but too old: CoqIde will not be available"
+        COQIDE=no;
+    fi
+else
+    echo "LablGtk2 not found: CoqIde will not be available"
+    COQIDE=no
+fi
+fi
+
+# Tell on windows if ocaml understands cygwin or windows path formats
+
+#"$CAMLC" -o config/giveostype config/giveostype.ml
+#CAMLOSTYPE=`config/giveostype`
+#rm config/giveostype
+
+case $ARCH in
+    win32)
+	# true -> strip : it exists under cygwin !
+	STRIPCOMMAND="strip";; 
+    *)
+    if [ "$coq_profile_flag" = "-p" ] ; then
+	STRIPCOMMAND="true"
+    else
+	STRIPCOMMAND="strip"
+    fi
+esac
+
+# mktexlsr
+#MKTEXLSR=`which mktexlsr`
+#case $MKTEXLSR in
+#    "") MKTEXLSR=true;;
+#esac
+
+# Summary of the configuration
+
+echo ""
+echo "  Coq top directory                 : $COQTOP"
+echo "  Architecture                      : $ARCH"
+if test ! -z "$OS" ; then
+  echo "  Operating system                  : $OS"
+fi
+echo "  OS dependent libraries            : $OSDEPLIBS"
+echo "  Objective-Caml/Camlp4 version     : $CAMLVERSION"
+echo "  Objective-Caml/Camlp4 binaries in : $CAMLBIN"
+echo "  Objective-Caml library in         : $CAMLLIB"
+echo "  Camlp4 library in                 : $CAMLP4LIB"
+if test "$reals" = "all"; then
+echo "  Reals theory                      : All"
+else
+echo "  Reals theory                      : Basic"
+fi
+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 ""
+
+#####################################################
+# Building the $COQTOP/config/coq_config.ml file
+#####################################################
+
+# damned backslashes under M$Windows
+case $ARCH in
+    win32)
+	CAMLLIB=`echo $CAMLLIB |sed -e 's|\\\|\\\\\\\|g'`
+	BINDIR=`echo $BINDIR |sed -e 's|\\\|\\\\\\\|g'`
+	LIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'`
+  	MANDIR=`echo $MANDIR |sed -e 's|\\\|\\\\\\\|g'`
+   	EMACSLIB=`echo $EMACSLIB |sed -e 's|\\\|\\\\\\\|g'`
+	;;
+esac
+
+mlconfig_file=$COQTOP/config/coq_config.ml
+rm -f $mlconfig_file
+cat << END_OF_COQ_CONFIG > $mlconfig_file
+(* DO NOT EDIT THIS FILE: automatically generated by ../configure *)
+
+let local = $local
+let bindir = "$BINDIR" 
+let coqlib = "$LIBDIR"
+let coqtop = "$COQTOP"
+let camllib = "$CAMLLIB"
+let camlp4lib = "$CAMLP4LIB"
+let best = "$best_compiler"
+let arch = "$ARCH"
+let osdeplibs = "$OSDEPLIBS"
+let version = "$VERSION"
+let versionsi = "$VERSIONSI"
+let date = "$DATE"
+let compile_date = "$COMPILEDATE"
+let exec_extension = "$EXE"
+
+END_OF_COQ_CONFIG
+
+# to be sure printf is found on windows when spaces occur in PATH variable
+PRINTF=`which printf`
+
+# Subdirectories of theories/ added in coq_config.ml
+subdirs () {
+    (cd $1; find * -type d ! -name CVS -exec $PRINTF "\"%s\";\n" {} \; | grep -v extraction/test | grep -v correctness >> $mlconfig_file)
+}
+
+echo "let theories_dirs = [" >> $mlconfig_file
+subdirs theories
+echo "]" >> $mlconfig_file
+
+echo "let contrib_dirs = [" >> $mlconfig_file
+subdirs contrib
+echo "]" >> $mlconfig_file
+
+chmod a-w $mlconfig_file
+
+
+###############################################
+# Building the $COQTOP/config/Makefile file
+###############################################
+
+rm -f $COQTOP/config/Makefile
+
+# damned backslashes under M$Windows (bis)
+case $ARCH in
+    win32)
+	BINDIR=`echo $BINDIR |sed -e 's|\\\|\\\\\\\|g'`
+	LIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'`
+  	MANDIR=`echo $MANDIR |sed -e 's|\\\|\\\\\\\|g'`
+   	EMACSLIB=`echo $EMACSLIB |sed -e 's|\\\|\\\\\\\|g'`
+	;;
+esac
+
+sed -e "s|LOCALINSTALLATION|$local|" \
+    -e "s|COQTOPDIRECTORY|$COQTOP|" \
+    -e "s|COQVERSION|$VERSION|" \
+    -e "s|BINDIRDIRECTORY|$BINDIR|" \
+    -e "s|COQLIBDIRECTORY|$LIBDIR|" \
+    -e "s|MANDIRDIRECTORY|$MANDIR|" \
+    -e "s|EMACSLIBDIRECTORY|$EMACSLIB|" \
+    -e "s|EMACSCOMMAND|$EMACS|" \
+    -e "s|COQDOCDIRECTORY|$COQDOCDIR|" \
+    -e "s|MKTEXLSRCOMMAND|$MKTEXLSR|" \
+    -e "s|ARCHITECTURE|$ARCH|" \
+    -e "s|OSDEPENDENTLIBS|$OSDEPLIBS|" \
+    -e "s|OSDEPENDENTP4OPTFLAGS|$OSDEPP4OPTFLAGS|" \
+    -e "s|CAMLLIBDIRECTORY|$CAMLLIB|" \
+    -e "s|CAMLTAG|$CAMLTAG|" \
+    -e "s|CAMLP4BINDIRECTORY|$CAMLP4BIN|" \
+    -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIB|" \
+    -e "s|CAMLP4TOOL|$camlp4o|" \
+    -e "s|COQDEBUGFLAG|$coq_debug_flag|" \
+    -e "s|COQPROFILEFLAG|$coq_profile_flag|" \
+    -e "s|BESTCOMPILER|$best_compiler|" \
+    -e "s|EXECUTEEXTENSION|$EXE|" \
+    -e "s|BYTECAMLC|$bytecamlc|" \
+    -e "s|NATIVECAMLC|$nativecamlc|" \
+    -e "s|STRIPCOMMAND|$STRIPCOMMAND|" \
+    -e "s|REALSOPT|$reals|" \
+    -e "s|COQIDEOPT|$COQIDE|" \
+      $COQTOP/config/Makefile.template > $COQTOP/config/Makefile
+
+chmod a-w $COQTOP/config/Makefile
+
+##################################################
+# Building the $COQTOP/dev/ocamldebug-v7 file
+####################################################
+
+if test "$coq_debug_flag" = "-g" ; then
+  rm -f $COQTOP/dev/ocamldebug-v7
+  if [ "$CAMLP4LIB" = "+camlp4" ] ; then
+    CAMLP4LIBFORCAMLDEBUG=$CAMLLIB/camlp4
+  else
+    CAMLP4LIBFORCAMLDEBUG=$CAMLP4LIB
+  fi
+  sed -e "s|COQTOPDIRECTORY|$COQTOP|" \
+      -e "s|COQLIBDIRECTORY|$LIBDIR|" \
+      -e "s|CAMLBINDIRECTORY|$CAMLBIN|" \
+      -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIBFORCAMLDEBUG|" \
+      $COQTOP/dev/ocamldebug-v7.template > $COQTOP/dev/ocamldebug-v7
+  chmod a-w,a+x $COQTOP/dev/ocamldebug-v7
+fi
+
+echo "If anything in the above is wrong, please restart './configure'"
+echo
+echo "*Warning* To compile the system for a new architecture"
+echo "          don't forget to do a 'make archclean' before './configure'."
+
+# $Id: configure,v 1.74.2.5 2004/07/17 17:06:51 herbelin Exp $