summaryrefslogtreecommitdiff
path: root/configure
diff options
context:
space:
mode:
Diffstat (limited to 'configure')
-rwxr-xr-xconfigure454
1 files changed, 217 insertions, 237 deletions
diff --git a/configure b/configure
index 193ebff4..a380cf86 100755
--- a/configure
+++ b/configure
@@ -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 $