summaryrefslogtreecommitdiff
path: root/configure
diff options
context:
space:
mode:
Diffstat (limited to 'configure')
-rwxr-xr-xconfigure267
1 files changed, 180 insertions, 87 deletions
diff --git a/configure b/configure
index c0cd3775..e964539a 100755
--- a/configure
+++ b/configure
@@ -6,8 +6,8 @@
#
##################################
-VERSION=8.1pl1
-DATE="Jul. 2007"
+VERSION=8.1pl2
+DATE="Oct. 2007"
# a local which command for sh
which () {
@@ -42,7 +42,11 @@ usage () {
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 -e "\tSpecifies the path to the OCaml library\n"
+ echo "-lablgtkdir"
+ echo -e "\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"
echo "-arch"
echo -e "\tSpecifies the architecture\n"
echo "-opt"
@@ -86,6 +90,7 @@ coq_profile_flag=
coq_annotate_flag=
coq_inline_flag=
best_compiler=opt
+cflags="-fno-defer-pop -Wall -Wno-unused"
gcc_exec=gcc
ar_exec=ar
@@ -100,6 +105,7 @@ mandir_spec=no
emacslib_spec=no
emacs_spec=no
camldir_spec=no
+lablgtkdir_spec=no
coqdocdir_spec=no
fsets_opt=no
fsets=all
@@ -109,7 +115,6 @@ arch_spec=no
coqide_spec=no
with_geoproof=false
-# COQTOP=`pwd`
COQSRC=`pwd`
# Parse command-line arguments
@@ -126,7 +131,7 @@ while : ; do
reals_opt=yes
reals=all;;
-src|--src) src_spec=yes
- COQTOP="$2"
+ COQSRC="$2"
shift;;
-bindir|--bindir) bindir_spec=yes
bindir="$2"
@@ -149,6 +154,12 @@ while : ; do
-camldir|--camldir) camldir_spec=yes
camldir="$2"
shift;;
+ -lablgtkdir|--lablgtkdir) lablgtkdir_spec=yes
+ lablgtkdir="$2"
+ shift;;
+ -camlp5dir|--camlp5dir)
+ camlp5dir="$2"
+ shift;;
-arch|--arch) arch_spec=yes
arch=$2
shift;;
@@ -229,6 +240,8 @@ case $arch_spec in
# 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`
else
@@ -274,7 +287,7 @@ fi
case $camldir_spec in
no) CAMLC=`which $bytecamlc`
case "$CAMLC" in
- "") echo "$bytecamlc is not present in your path !"
+ "") 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
@@ -306,6 +319,11 @@ if test ! -f "$CAMLC" ; then
exit 1
fi
+# Under Windows, OCaml only understands Windows filenames (C:\...)
+case $ARCH in
+ win32) CAMLBIN=`cygpath -w ${CAMLBIN}`;;
+esac
+
# this fixes a camlp4 bug under FreeBSD
# ("native-code program cannot do a dynamic load")
if [ `uname -s` = "FreeBSD" ]; then camlp4oexec=$camlp4oexec.byte; fi
@@ -313,24 +331,28 @@ if [ `uname -s` = "FreeBSD" ]; then camlp4oexec=$camlp4oexec.byte; fi
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.06|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.07 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.07 or later!"
fi
echo "Configuration script failed!"
exit 1;;
- 3.06|3.07*|3.08*)
- echo "You have Objective-Caml $CAMLVERSION. Good!"
- coq_inline_flag="-inline 0";;
+ 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"
+ echo "You have Objective-Caml $CAMLVERSION. Good!";;
?*)
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 "Is it installed properly?"
echo "Configuration script failed!"
exit 1;;
esac
@@ -342,11 +364,19 @@ CAMLTAG=OCAML`echo $CAMLVERSION | sed -e "s/\([1-9]\)\.\([0-9]*\).*/\1\2/g"`
if [ "$best_compiler" = "opt" ] ; then
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
+ 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 ;
+ best_compiler=byte
echo "You have only bytecode compilation."
fi
fi
@@ -354,19 +384,54 @@ fi
# For coqmktop & bytecode compiler
-CAMLLIB=`"$CAMLC" -where`
+case $ARCH in
+ win32) # Awfull trick to get around a ^M problem at the end of CAMLLIB
+ CAMLLIB=`"$CAMLC" -where | sed -e 's/^\(.*\)$/\1/'` ;;
+ *)
+ CAMLLIB=`"$CAMLC" -where`
+ esac
+
+
+# Camlp4 / Camlp5 configuration
+# Very basic for the moment: if camlp5 exists, we use it...
+
+if [ "$camlp5dir" != "" ]; then
+ CAMLP4=camlp5
+ CAMLP4LIB=$camlp5dir
+ camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'`
+elif [ "$CAMLTAG" = "OCAML310" ]; then
+ if [ -x "${CAMLLIB}/camlp5" ]; then
+ CAMLP4LIB=+camlp5
+ elif [ -x "${CAMLLIB}/site-lib/camlp5" ]; then
+ CAMLP4LIB=+site-lib/camlp5
+ else
+ echo "Objective Caml 3.10 found but no Camlp5 installed."
+ echo "Configuration script failed!"
+ exit 1
+ fi
+ CAMLP4=camlp5
+ camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'`
+else
+ CAMLP4=camlp4
+ CAMLP4LIB=+camlp4
+fi
+
+if [ "$CAMLP4" = "camlp5" ] && `$camlp4oexec -v 2>&1 | grep -q 5.00`; then
+ echo "Camlp5 version 5.00 not supported: versions 4.0x or >= 5.01 are OK."
+ echo "Configuration script failed!"
+ exit 1
+fi
+
-# Camlp4 (greatly simplified since merged with ocaml)
+case $CAMLP4LIB in
+ +*) FULLCAMLP4LIB=$CAMLLIB/`echo $CAMLP4LIB | cut -b 2-`;;
+ *) FULLCAMLP4LIB=$CAMLP4LIB;;
+esac
+# Assume that camlp(4|5) binaries are at the same place as ocaml ones
+# (this should become configurable some day)
CAMLP4BIN=${CAMLBIN}
-#case $OS in
-# Win32)
- CAMLP4LIB=+camlp4
-# ;;
-# *)
-# CAMLP4LIB=${CAMLLIB}/camlp4
-#esac
# OS dependent libraries
@@ -380,7 +445,8 @@ case $ARCH in
esac;;
alpha) OSDEPLIBS="-cclib -lunix";;
win32) OS="Win32"
- OSDEPLIBS="-cclib -lunix";;
+ OSDEPLIBS="-cclib -lunix"
+ cflags="-mno-cygwin $cflags";;
*) OSDEPLIBS="-cclib -lunix"
esac
@@ -396,24 +462,50 @@ fi
# Which coqide is asked ? which one is possible ?
if [ "$coqide_spec" = "yes" -a "$COQIDE" = "no" ]; then
- echo "CoqIde disabled as requested"
-elif [ ! -x "${CAMLLIB}/lablgtk2" ]; then
- echo "LablGtk2 not found: CoqIde will not be available"
- COQIDE=no
-elif [ -z "`grep -w convert_with_fallback ${CAMLLIB}/lablgtk2/glib.mli`" ]; then
- echo "LablGtk2 found but too old: CoqIde will not be available"
- COQIDE=no;
-elif [ "$coqide_spec" = "yes" -a "$COQIDE" = "byte" ]; then
- echo "LablGtk2 found, bytecode CoqIde will be used as requested"
- COQIDE=byte
-elif [ ! -f "${CAMLLIB}/threads/threads.cmxa" ]; then
- echo "LablGtk2 found, no native threads: bytecode CoqIde will be available"
- COQIDE=byte
-else
- echo "LablGtk2 found, native threads: native CoqIde will be available"
- COQIDE=opt
+ echo "CoqIde disabled as requested."
+else
+ case $lablgtkdir_spec in
+ no)
+ if [ -f "${CAMLLIB}/lablgtk2/glib.mli" ]; then
+ lablgtkdir=${CAMLLIB}/lablgtk2
+ elif [ -f "${CAMLLIB}/site-lib/lablgtk2/glib.mli" ]; then
+ lablgtkdir=${CAMLLIB}/site-lib/lablgtk2
+ fi;;
+ yes)
+ if [ ! -f "$lablgtkdir/glib.mli" ]; then
+ echo "Incorrect LablGtk2 library (glib.mli not found)."
+ echo "Configuration script failed!"
+ exit 1
+ fi;;
+ esac
+ if [ "$lablgtkdir" = "" ]; then
+ echo "LablGtk2 not found: CoqIde will not be available."
+ COQIDE=no
+ elif [ -z "`grep -w convert_with_fallback "$lablgtkdir/glib.mli"`" ]; then
+ echo "LablGtk2 found but too old: CoqIde will not be available."
+ COQIDE=no;
+ elif [ "$coqide_spec" = "yes" -a "$COQIDE" = "byte" ]; then
+ echo "LablGtk2 found, bytecode CoqIde will be used as requested."
+ COQIDE=byte
+ elif [ ! -f "${CAMLLIB}/threads/threads.cmxa" ]; then
+ echo "LablGtk2 found, no native threads: bytecode CoqIde will be available."
+ COQIDE=byte
+ else
+ echo "LablGtk2 found, native threads: native CoqIde will be available."
+ COQIDE=opt
+ fi
fi
+case $COQIDE in
+ byte|opt)
+ case $lablgtkdir_spec in
+ no) LABLGTKLIB=+lablgtk2 # Pour le message
+ LABLGTKINCLUDES="-I $LABLGTKLIB";; # Pour le makefile
+ yes) LABLGTKLIB="$lablgtkdir" # Pour le message
+ LABLGTKINCLUDES="-I \"$LABLGTKLIB\"";; # Pour le makefile
+ esac;;
+ no) LABLGTKINCLUDES="";;
+esac
# Tell on windows if ocaml understands cygwin or windows path formats
@@ -442,14 +534,13 @@ 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`
+ no) COQTOP=${COQSRC}
+esac
+
+# OCaml only understand Windows filenames (C:\...)
+case $ARCH in
+ win32) COQTOP=`cygpath -w ${COQTOP}`
esac
case $ARCH in
@@ -578,6 +669,9 @@ 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 "$COQIDE" != "no"; then
+echo " Lablgtk2 library in : $LABLGTKLIB"
+fi
if test "$fsets" = "all"; then
echo " FSets theory : All"
else
@@ -609,13 +703,35 @@ escape_var () {
EOF
}
-export COQTOP BINDIR LIBDIR CAMLBIN CAMLLIB
-ESCCOQTOP="`VAR=COQTOP escape_var`"
-ESCBINDIR="`VAR=BINDIR escape_var`"
-ESCLIBDIR="`VAR=LIBDIR escape_var`"
-ESCCAMLDIR="`VAR=CAMLBIN escape_var`"
-ESCCAMLLIB="`VAR=CAMLLIB escape_var`"
-ESCCAMLP4LIB="$ESCCAMLLIB"/camlp4
+# damned backslashes under M$Windows
+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'`
+ ESCCAMLDIR=`echo $CAMLBIN |sed -e 's|\\\|\\\\\\\|g'`
+ ESCCAMLLIB=`echo $CAMLLIB |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'`
+ ESCCAMLP4LIB=`echo $CAMLP4LIB |sed -e 's|\\\|\\\\\\\|g'`
+ ESCLABLGTKINCLUDES=`echo $LABLGTKINCLUDES |sed -e 's|\\\|\\\\\\\|g'`
+ ;;
+ *)
+ ESCCOQTOP="$COQTOP"
+ ESCBINDIR="$BINDIR"
+ ESCLIBDIR="$LIBDIR"
+ ESCCAMLDIR="$CAMLBIN"
+ ESCCAMLLIB="$CAMLLIB"
+ ESCMANDIR="$MANDIR"
+ ESCEMACSLIB="$EMACSLIB"
+ ESCCOQDOCDIR="$COQDOCDIR"
+ ESCCAMLP4BIN="$CAMLP4BIN"
+ ESCCAMLP4LIB="$CAMLP4LIB"
+ ESCLABLGTKINCLUDES="$LABLGTKINCLUDES"
+ ;;
+esac
mlconfig_file="$COQSRC/config/coq_config.ml"
rm -f $mlconfig_file
@@ -628,6 +744,7 @@ let coqlib = "$ESCLIBDIR"
let coqtop = "$ESCCOQTOP"
let camldir = "$ESCCAMLDIR"
let camllib = "$ESCCAMLLIB"
+let camlp4 = "$CAMLP4"
let camlp4lib = "$ESCCAMLP4LIB"
let best = "$best_compiler"
let arch = "$ARCH"
@@ -666,29 +783,8 @@ chmod a-w "$mlconfig_file"
rm -f "$COQSRC/config/Makefile"
-# 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'`
- ;;
- *)
- 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|COQSRCDIRECTORY|$COQSRC|" \
-e "s|COQVERSION|$VERSION|" \
-e "s|BINDIRDIRECTORY|$ESCBINDIR|" \
-e "s|COQLIBDIRECTORY|$ESCLIBDIR|" \
@@ -706,10 +802,12 @@ sed -e "s|LOCALINSTALLATION|$local|" \
-e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIB|" \
-e "s|CAMLP4TOOL|$camlp4oexec|" \
-e "s|CAMLP4COMPATFLAGS|$CAMLP4COMPAT|" \
+ -e "s|LABLGTKINCLUDES|$ESCLABLGTKINCLUDES|" \
-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|" \
@@ -735,19 +833,14 @@ chmod a-w "$COQSRC/config/Makefile"
# Building the $COQTOP/dev/ocamldebug-coq file
##################################################
-OCAMLDEBUGCOQ=$COQTOP/dev/ocamldebug-coq
+OCAMLDEBUGCOQ=$COQSRC/dev/ocamldebug-coq
if test "$coq_debug_flag" = "-g" ; then
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|$CAMLP4LIBFORCAMLDEBUG|" \
+ -e "s|CAMLP4LIBDIRECTORY|$FULLCAMLP4LIB|"\
$OCAMLDEBUGCOQ.template > $OCAMLDEBUGCOQ
chmod a-w,a+x $OCAMLDEBUGCOQ
fi
@@ -757,7 +850,7 @@ fi
####################################################
if [ ! "$COQIDE" = "no" ]; then
- if grep "class view " "$CAMLLIB/lablgtk2/gText.mli" | grep -q "\[>" ; then
+ if grep "class view " "$lablgtkdir/gText.mli" | grep -q "\[>" ; then
cp -f ide/undo_lablgtk_ge26.mli ide/undo.mli
else
cp -f ide/undo_lablgtk_lt26.mli ide/undo.mli
@@ -773,4 +866,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 10039 2007-07-20 22:04:33Z notin $
+# $Id: configure 10215 2007-10-11 13:13:51Z herbelin $