From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 25 Jul 2008 15:12:53 +0200 Subject: Imported Upstream version 8.2~beta3+dfsg --- configure | 288 ++++++++++++++++++++++++++++++++++++++------------------------ 1 file changed, 179 insertions(+), 109 deletions(-) (limited to 'configure') 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 " - echo -e "\tSet installation directory to \n" + printf "\tSet installation directory to \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 " echo "-with-ar " echo "-with-ranlib " - 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 $ -- cgit v1.2.3