diff options
Diffstat (limited to 'configure')
| -rwxr-xr-x | configure | 454 |
1 files changed, 217 insertions, 237 deletions
@@ -6,8 +6,8 @@ # ################################## -VERSION=8.0pl3 -DATE="Jan 2006" +VERSION=8.1-alpha +DATE="Mar 2006" # a local which command for sh which () { @@ -30,50 +30,66 @@ coq_profile_flag= best_compiler=opt local=false -src_spec=no -prefix_spec=no bindir_spec=no libdir_spec=no mandir_spec=no emacslib_spec=no -#emacs_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) prefix_spec=yes - prefix="$2" + -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) src_spec=yes - COQTOP="$2" + -src|--src) COQTOP=$2 shift;; -bindir|--bindir) bindir_spec=yes - bindir="$2" + bindir=$2 shift;; -libdir|--libdir) libdir_spec=yes - libdir="$2" + libdir=$2 shift;; -mandir|--mandir) mandir_spec=yes mandir=$2 shift;; -emacslib|--emacslib) emacslib_spec=yes - emacslib="$2" + emacslib=$2 shift;; -# -emacs |--emacs) emacs_spec=yes -# emacs="$2" -# shift;; + -emacs |--emacs) emacs_spec=yes + emacs=$2 + shift;; -coqdocdir|--coqdocdir) coqdocdir_spec=yes - coqdocdir="$2" + coqdocdir=$2 shift;; -arch|--arch) arch_spec=yes arch=$2 @@ -95,11 +111,6 @@ while : ; do shift done -if [ $prefix_spec = yes -a $local = true ] ; then - echo "Options -prefix and -local are incompatible" - echo "Configure script failed!" - exit 1 -fi # compile date DATEPGM=`which date` @@ -135,28 +146,125 @@ case $arch_spec in yes) ARCH=$arch esac -# executable extension +# bindir, libdir, mandir, etc. case $ARCH in - win32) EXE=".exe";; - *) EXE="" + 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 -# strip command +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 - win32) - # true -> strip : it exists under cygwin ! - STRIPCOMMAND="strip";; - *) - if [ "$coq_profile_flag" = "-p" ] ; then - STRIPCOMMAND="true" - else - STRIPCOMMAND="strip" - fi + 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` @@ -222,30 +330,21 @@ if [ "$best_compiler" = "opt" ] ; then esac fi -# For coqmktop +# For coqmktop & bytecode compiler CAMLLIB=`"$CAMLC" -where` # Camlp4 (greatly simplified since merged with ocaml) CAMLP4BIN=${CAMLBIN} -CAMLP4LIB=+camlp4 -# 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 +#case $OS in +# Win32) + CAMLP4LIB=+camlp4 +# ;; +# *) +# CAMLP4LIB=${CAMLLIB}/camlp4 +#esac # lablgtk2 and CoqIDE @@ -259,6 +358,11 @@ if test -x "${CAMLLIB}/lablgtk2" ; then echo "LablGtk2 found, no native threads: bytecode CoqIde will be available" COQIDE=byte fi + if grep "class view " "${CAMLLIB}/lablgtk2/gText.mli" | grep -q "\[>" ; then + LABLGTKGE26=yes; + else + LABLGTKGE26=no + fi; else echo "LablGtk2 found but too old: CoqIde will not be available" COQIDE=no; @@ -269,154 +373,30 @@ else fi fi -if [ $COQIDE != no ] ; then - if grep "class view " "${CAMLLIB}/lablgtk2/gText.mli" | grep -q "\[>" ; then - LABLGTKGE26=yes; - else - LABLGTKGE26=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 -###################################### -# mktexlsr +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 -########################################### -# bindir, libdir, mandir, etc. - -canonical_pwd () { -ocaml 2>&1 1>/dev/null <<EOF - prerr_endline(Sys.getcwd());; -EOF -} - -case $src_spec in - no) COQTOP=`canonical_pwd` -esac - -case $ARCH in - win32) - bindir_def='C:\coq\bin' - libdir_def='C:\coq\lib' - mandir_def='C:\coq\man' - 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;; -esac - -emacs_def=emacs - -case $bindir_spec/$prefix_spec/$local in - yes/*/*) BINDIR=$bindir ;; - */yes/*) BINDIR=$prefix/bin ;; - */*/true) BINDIR=$COQTOP/bin ;; - *) echo "Where should I install the Coq binaries [$bindir_def] ?" - read BINDIR - case $BINDIR in - "") BINDIR=$bindir_def;; - *) true;; - esac;; -esac - -case $libdir_spec/$prefix_spec/$local in - yes/*/*) LIBDIR=$libdir;; - */yes/*) - case $ARCH in - win32) LIBDIR=$prefix ;; - *) LIBDIR=$prefix/lib/coq ;; - esac ;; - */*/true) LIBDIR=$COQTOP ;; - *) echo "Where should I install the Coq library [$libdir_def] ?" - read LIBDIR - case $LIBDIR in - "") LIBDIR=$libdir_def;; - *) true;; - esac;; -esac - -case $mandir_spec/$prefix_spec/$local in - yes/*/*) MANDIR=$mandir;; - */yes/*) MANDIR=$prefix/man ;; - */*/true) MANDIR=$COQTOP/man ;; - *) echo "Where should I install the Coq man pages [$mandir_def] ?" - read MANDIR - case $MANDIR in - "") MANDIR=$mandir_def;; - *) true;; - esac;; -esac - -case $emacslib_spec/$prefix_spec/$local in - yes/*/*) EMACSLIB=$emacslib;; - */yes/*) - case $ARCH in - win32) EMACSLIB=$prefix/emacs ;; - *) EMACSLIB=$prefix/share/emacs/site-lisp ;; - esac ;; - */*/true) EMACSLIB=$COQTOP/tools/emacs ;; - *) echo "Where should I install the Coq Emacs mode [$emacslib_def] ?" - read EMACSLIB - case $EMACSLIB in - "") EMACSLIB=$emacslib_def;; - *) true;; - esac;; -esac - -case $coqdocdir_spec/$prefix_spec/$local in - yes/*/*) COQDOCDIR=$coqdocdir;; - */yes/*) - case $ARCH in - win32) COQDOCDIR=$prefix/latex ;; - *) COQDOCDIR=$prefix/share/emacs/site-lisp ;; - esac ;; - */*/true) COQDOCDIR=$COQTOP/tools/coqdoc ;; - *) echo "Where should I install Coqdoc TeX/LaTeX files [$coqdocdir_def] ?" - read COQDOCDIR - case $COQDOCDIR in - "") COQDOCDIR=$coqdocdir_def;; - *) true;; - 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 - -# case $EMACS in -# "") EMACS=$emacs_def;; -# *) true;; -# esac;; -# yes) EMACS=$emacs;; -# esac - -########################################### # Summary of the configuration echo "" @@ -449,19 +429,16 @@ echo "" # Building the $COQTOP/config/coq_config.ml file ##################################################### -# An escaped version of a variable -escape_var () { -ocaml 2>&1 1>/dev/null <<EOF - prerr_endline(String.escaped(Sys.getenv"$VAR"));; -EOF -} - -export COQTOP BINDIR LIBDIR CAMLLIB -ESCCOQTOP="`VAR=COQTOP escape_var`" -ESCBINDIR="`VAR=BINDIR escape_var`" -ESCLIBDIR="`VAR=LIBDIR escape_var`" -ESCCAMLLIB="`VAR=CAMLLIB escape_var`" -ESCCAMLP4LIB="$ESCCAMLLIB"/camlp4 +# 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 @@ -469,15 +446,16 @@ cat << END_OF_COQ_CONFIG > $mlconfig_file (* DO NOT EDIT THIS FILE: automatically generated by ../configure *) let local = $local -let bindir = "$ESCBINDIR" -let coqlib = "$ESCLIBDIR" -let coqtop = "$ESCCOQTOP" -let camllib = "$ESCCAMLLIB" -let camlp4lib = "$ESCCAMLP4LIB" +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" @@ -489,7 +467,7 @@ 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) + (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 @@ -509,42 +487,32 @@ chmod a-w $mlconfig_file rm -f $COQTOP/config/Makefile -# damned backslashes under M$Windows +# damned backslashes under M$Windows (bis) case $ARCH in win32) - ESCCOQTOP=`echo $COQTOP |sed -e 's|\\\|\\\\\\\|g'` - ESCBINDIR=`echo $BINDIR |sed -e 's|\\\|\\\\\\\|g'` - ESCLIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'` - ESCMANDIR=`echo $MANDIR |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'` + 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'` ;; - *) - ESCCOQTOP="$COQTOP" - ESCBINDIR="$BINDIR" - ESCLIBDIR="$LIBDIR" - ESCMANDIR="$MANDIR" - ESCEMACSLIB="$EMACSLIB" - ESCCOQDOCDIR="$COQDOCDIR" - ESCCAMLP4BIN="$CAMLP4BIN" ;; esac sed -e "s|LOCALINSTALLATION|$local|" \ - -e "s|COQTOPDIRECTORY|$ESCCOQTOP|" \ + -e "s|COQTOPDIRECTORY|$COQTOP|" \ -e "s|COQVERSION|$VERSION|" \ - -e "s|BINDIRDIRECTORY|$ESCBINDIR|" \ - -e "s|COQLIBDIRECTORY|$ESCLIBDIR|" \ - -e "s|MANDIRDIRECTORY|$ESCMANDIR|" \ - -e "s|EMACSLIBDIRECTORY|$ESCEMACSLIB|" \ + -e "s|BINDIRDIRECTORY|$BINDIR|" \ + -e "s|COQLIBDIRECTORY|$LIBDIR|" \ + -e "s|MANDIRDIRECTORY|$MANDIR|" \ + -e "s|EMACSLIBDIRECTORY|$EMACSLIB|" \ -e "s|EMACSCOMMAND|$EMACS|" \ - -e "s|COQDOCDIRECTORY|$ESCCOQDOCDIR|" \ + -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|$ESCCAMLP4BIN|" \ + -e "s|CAMLP4BINDIRECTORY|$CAMLP4BIN|" \ -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIB|" \ -e "s|CAMLP4TOOL|$camlp4o|" \ -e "s|CAMLP4COMPATFLAGS|$CAMLP4COMPAT|" \ @@ -562,17 +530,29 @@ sed -e "s|LOCALINSTALLATION|$local|" \ chmod a-w $COQTOP/config/Makefile ################################################## -# Building the $COQTOP/dev/ocamldebug-v7 file -#################################################### +# Building the $COQTOP/dev/ocamldebug-coq file +################################################## + +OCAMLDEBUGCOQ=$COQTOP/dev/ocamldebug-coq if test "$coq_debug_flag" = "-g" ; then - rm -f $COQTOP/dev/ocamldebug-v7 + rm -f $OCAMLDEBUGCOQ + 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|$CAMLLIB/camlp4|" \ - $COQTOP/dev/ocamldebug-v7.template > $COQTOP/dev/ocamldebug-v7 - chmod a-w,a+x $COQTOP/dev/ocamldebug-v7 + -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIBFORCAMLDEBUG|" \ + $OCAMLDEBUGCOQ.template > $OCAMLDEBUGCOQ + chmod a-w,a+x $OCAMLDEBUGCOQ +fi + +# Compatibility with previous name +if [ ! -f $COQTOP/dev/ocamldebug-v7 ] ; then + ln -s `basename $OCAMLDEBUGCOQ` $COQTOP/dev/ocamldebug-v7 fi ################################################## @@ -594,4 +574,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,v 1.74.2.19 2006/01/13 11:50:07 barras Exp $ +# $Id: configure 8712 2006-04-14 10:34:47Z notin $ |