From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Tue, 21 Nov 2006 21:38:49 +0000 Subject: Imported Upstream version 8.1~gamma --- configure | 243 +++++++++++++++++++++++++++++++++++++++++++++++--------------- 1 file changed, 184 insertions(+), 59 deletions(-) (limited to 'configure') 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 " + echo -e "\tSet installation directory to \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 " + echo "-with-ar " + echo "-with-ranlib " + 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 <&1 1>/dev/null < $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 $ -- cgit v1.2.3