Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Fetching contributors…

Cannot retrieve contributors at this time

executable file 1232 lines (1087 sloc) 38.116 kb
#!/bin/sh
##################################
#
# Configuration script for Coq
#
##################################
VERSION=trunk
VOMAGIC=08511
STATEMAGIC=58511
DATE=`LC_ALL=C LANG=C date +"%B %Y"`
# Create the bin/ directory if non-existent
test -d bin || mkdir bin
# a local which command for sh
which () {
IFS=":" # set words separator in PATH to be ':' (it allows spaces in dirnames)
for i in $PATH; do
if test -z "$i"; then i=.; fi
if [ -f "$i/$1" ] ; then
IFS=" "
echo "$i/$1"
break
fi
done
}
usage () {
printf "Available options for configure are:\n"
echo "-help"
printf "\tDisplays this help page\n"
echo "-prefix <dir>"
printf "\tSet installation directory to <dir>\n"
echo "-local"
printf "\tSet installation directory to the current source tree\n"
echo "-coqrunbyteflags <flags>"
printf "\tSet link flags for VM-dependent bytecode (coqtop)\n"
echo "-coqtoolsbyteflags <flags>"
printf "\tSet link flags for VM-independant bytecode (coqdep, coqdoc, ...)\n"
echo "-custom"
printf "\tGenerate all bytecode executables with -custom (not recommended)\n"
echo "-bindir <dir>"
echo "-libdir <dir>"
echo "-configdir <dir>"
echo "-datadir <dir>"
echo "-mandir <dir>"
echo "-docdir <dir>"
printf "\tSpecifies where to install bin/lib/config/data/man/doc files resp.\n"
echo "-emacslib <dir>"
printf "\tSpecifies where emacs files are to be installed\n"
echo "-coqdocdir <dir>"
printf "\tSpecifies where Coqdoc style files are to be installed\n"
echo "-camldir <dir>"
printf "\tSpecifies the path to the OCaml library\n"
echo "-lablgtkdir <dir>"
printf "\tSpecifies the path to the Lablgtk library\n"
echo "-usecamlp5"
printf "\tSpecifies to use camlp5 instead of camlp4\n"
echo "-usecamlp4"
printf "\tSpecifies to use camlp4 instead of camlp5\n"
echo "-camlp5dir <dir>"
printf "\tSpecifies where to look for the Camlp5 library and tells to use it\n"
echo "-arch <arch>"
printf "\tSpecifies the architecture\n"
echo "-opt"
printf "\tSpecifies whether or not to use OCaml *.opt optimized compilers\n"
echo "-natdynlink (yes|no)"
printf "\tSpecifies whether or not to use dynamic loading of native code\n"
echo "-coqide (opt|byte|no)"
printf "\tSpecifies whether or not to compile Coqide\n"
echo "-nomacintegration"
printf "\tSpecifies to not try to build coqide mac integration\n"
echo "-browser <command>"
printf "\tUse <command> to open URL %%s\n"
echo "-nodoc"
printf "\tSpecifies to not compile the documentation\n"
echo "-with-geoproof (yes|no)"
printf "\tSpecifies whether or not to use Geoproof binding\n"
echo "-byte-only"
printf "\tCompiles only bytecode version of Coq\n"
echo "-debug"
printf "\tAdd debugging information in the Coq executables\n"
echo "-profile"
printf "\tAdd profiling information in the Coq executables\n"
echo "-annotate"
printf "\tCompiles Coq with -dtypes option\n"
echo "-typerex"
printf "\tCompiles Coq using typerex wrapper\n"
echo "-makecmd <command>"
printf "\tName of GNU Make command\n"
echo "-no-native-compiler"
printf "\tDisables compilation to native code for conversion and normalization\n"
}
# Default OCaml binaries
bytecamlc=ocamlc
nativecamlc=ocamlopt
ocamlmklibexec=ocamlmklib
ocamlexec=ocaml
ocamldepexec=ocamldep
ocamldocexec=ocamldoc
ocamllexexec=ocamllex
ocamlyaccexec=ocamlyacc
camlp4oexec=camlp4o
default_typerex_wrapper="ocp-wrapper -save-types"
coq_debug_flag=
coq_debug_flag_opt=
coq_profile_flag=
coq_annotate_flag=
coq_typerex_wrapper=
best_compiler=opt
cflags="-fno-defer-pop -Wall -Wno-unused"
natdynlink=yes
local=false
coqrunbyteflags_spec=no
coqtoolsbyteflags_spec=no
custom_spec=no
prefix_spec=no
bindir_spec=no
libdir_spec=no
configdir_spec=no
datadir_spec=no
mandir_spec=no
docdir_spec=no
emacslib_spec=no
emacs_spec=no
camldir_spec=no
lablgtkdir_spec=no
coqdocdir_spec=no
arch_spec=no
coqide_spec=no
nomacintegration_spec=no
browser_spec=no
wwwcoq_spec=no
with_geoproof=false
with_doc=all
with_doc_spec=no
force_caml_version=no
force_caml_version_spec=no
usecamlp5=yes
no_native_compiler=false
# Parse command-line arguments
while : ; do
case "$1" in
"") break;;
-help|--help) usage
exit;;
-prefix|--prefix) prefix_spec=yes
prefix="$2"
shift;;
-local|--local) local=true;;
-coqrunbyteflags|--coqrunbyteflags) coqrunbyteflags_spec=yes
coqrunbyteflags="$2"
shift;;
-coqtoolsbyteflags|--coqtoolsbyteflags) coqtoolsbyteflags_spec=yes
coqtoolsbyteflags="$2"
shift;;
-custom|--custom) custom_spec=yes;;
-bindir|--bindir) bindir_spec=yes
bindir="$2"
shift;;
-libdir|--libdir) libdir_spec=yes
libdir="$2"
shift;;
-configdir|--configdir) configdir_spec=yes
configdir="$2"
shift;;
-datadir|--datadir) datadir_spec=yes
datadir="$2"
shift;;
-mandir|--mandir) mandir_spec=yes
mandir="$2"
shift;;
-docdir|--docdir) docdir_spec=yes
docdir="$2"
shift;;
-emacslib|--emacslib) emacslib_spec=yes
emacslib="$2"
shift;;
-emacs |--emacs) emacs_spec=yes
emacs="$2"
printf "Warning: obsolete -emacs option\n"
shift;;
-coqdocdir|--coqdocdir) coqdocdir_spec=yes
coqdocdir="$2"
shift;;
-camldir|--camldir) camldir_spec=yes
camldir="$2"
shift;;
-lablgtkdir|--lablgtkdir) lablgtkdir_spec=yes
lablgtkdir="$2"
shift;;
-usecamlp5|--usecamlp5)
usecamlp5=yes;;
-usecamlp4|--usecamlp4)
usecamlp5=no;;
-camlp5dir|--camlp5dir)
usecamlp5=yes
camlp5dir="$2"
shift;;
-arch|--arch) arch_spec=yes
arch=$2
shift;;
-opt|--opt) bytecamlc=ocamlc.opt
camlp4oexec=camlp4o # can't add .opt since dyn load'll be required
nativecamlc=ocamlopt.opt;;
-natdynlink|--natdynlink) case "$2" in
yes) natdynlink=yes;;
*) natdynlink=no
esac
shift;;
-coqide|--coqide) coqide_spec=yes
case "$2" in
byte|opt) COQIDE=$2;;
*) COQIDE=no
esac
shift;;
-nomacintegration) nomacintegration_spec=yes
shift;;
-browser|--browser) browser_spec=yes
BROWSER=$2
shift;;
-coqwebsite|--coqwebsite) wwwcoq_spec=yes
WWWCOQ=$2
shift;;
-nodoc|--nodoc) with_doc_spec=yes
with_doc=no;;
-with-doc|--with-doc) with_doc_spec=yes
case "$2" in
yes|all) with_doc=all;;
*) with_doc=no
esac
shift;;
-with-geoproof|--with-geoproof)
case "$2" in
yes) with_geoproof=true;;
no) with_geoproof=false;;
esac
shift;;
-makecmd|--makecmd) makecmd="$2"
shift;;
-byte-only|-byteonly|--byteonly|--byte-only) best_compiler=byte;;
-debug|--debug) coq_debug_flag=-g;;
-profile|--profile) coq_profile_flag=-p;;
-annotate|--annotate) coq_annotate_flag=-dtypes;;
-typerex|--typerex) coq_typerex_wrapper=$default_typerex_wrapper;;
-no-native-compiler|--no-native-compiler) no_native_compiler=true;;
-force-caml-version|--force-caml-version|-force-ocaml-version|--force-ocaml-version)
force_caml_version_spec=yes
force_caml_version=yes;;
*) echo "Unknown option \"$1\"." 1>&2; usage; exit 2;;
esac
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`
case $DATEPGM in
"") echo "I can't find the program \"date\" in your path."
echo "Please give me the current date"
read COMPILEDATE;;
*) COMPILEDATE=`LC_ALL=C LANG=C date +"%b %d %Y %H:%M:%S"`;;
esac
# Architecture
case $arch_spec in
no)
# First we test if we are running a Cygwin or Mingw/Msys system
if [ `uname -s | cut -c -6` = "CYGWIN" ] ; then
ARCH="win32"
CYGWIN=yes
elif [ `uname -s | cut -c -7` = "MINGW32" ]; then
ARCH="win32"
else
# If not, we determine the architecture
if test -x /bin/uname ; then
ARCH=`/bin/uname -s`
elif test -x /usr/bin/uname ; then
ARCH=`/usr/bin/uname -s`
elif 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`
else
echo "I can not automatically find the name of your architecture."
printf "%s"\
"Give me a name, please [win32 for Win95, Win98 or WinNT]: "
read ARCH
fi
fi;;
yes) ARCH=$arch
esac
# executable extension
case $ARCH in
win32)
ARCH_WIN32=true
EXE=".exe"
DLLEXT=".dll";;
*) ARCH_WIN32=false
EXE=""
DLLEXT=".so"
esac
# Is the source tree checked out from a recognised
# version control system ?
if test -e .svn/entries ; then
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 ${makecmd:-make}`
if [ "$MAKE" != "" ]; then
MAKEVERSION=`$MAKE -v | head -1 | cut -d" " -f3`
MAKEVERSIONMAJOR=`echo $MAKEVERSION | cut -d. -f1`
MAKEVERSIONMINOR=`echo $MAKEVERSION | cut -d. -f2`
if [ "$MAKEVERSIONMAJOR" -eq 3 -a "$MAKEVERSIONMINOR" -ge 81 ]; then
echo "You have GNU Make $MAKEVERSION. Good!"
else
OK="no"
#Extra support for local installation of make 3.81
#will be useless when make >= 3.81 will be standard
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
fi
else
echo "Cannot find GNU Make >= 3.81."
fi
# Browser command
if [ "$browser_spec" = "no" ]; then
case $ARCH in
win32) BROWSER='start %s' ;;
Darwin) BROWSER='open %s' ;;
*) BROWSER='firefox -remote "OpenURL(%s,new-tab)" || firefox %s &' ;;
esac
fi
if [ "$wwwcoq_spec" = "no" ]; then
WWWCOQ="http://coq.inria.fr/"
fi
#########################################
# Objective Caml programs
case $camldir_spec in
no) 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 "$CAMLC" in
"") CAMLC=/usr/local/bin/$bytecamlc;;
*/ocamlc|*/ocamlc.opt) true;;
*/) CAMLC="${CAMLC}"$bytecamlc;;
*) CAMLC="${CAMLC}"/$bytecamlc;;
esac
esac
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
ocamlmklibexec=$CAMLBIN/ocamlmklib
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
fi
# Under Windows, we need to convert from cygwin/mingw paths (/c/Program Files/Ocaml)
# to more windows-looking paths (c:/Program Files/Ocaml). Note that / are kept
mk_win_path () {
case $ARCH,$CYGWIN in
win32,yes) cygpath -m "$1" ;;
win32*) "$ocamlexec" "tools/mingwpath.ml" "$1" ;;
*) echo "$1" ;;
esac
}
case $ARCH in
win32) CAMLBIN=`mk_win_path "$CAMLBIN"`;;
esac
# Beware of the final \r in Win32
CAMLVERSION=`"$CAMLC" -version | tr -d "\r"`
CAMLLIB=`"$CAMLC" -where | tr -d "\r"`
case $CAMLVERSION in
1.*|2.*|3.0*|3.10*|3.11.[01])
echo "Your version of Objective-Caml is $CAMLVERSION."
if [ "$force_caml_version" = "yes" ]; then
echo "*Warning* You are compiling Coq with an outdated version of Objective-Caml."
else
echo " You need Objective-Caml 3.11.2 or later."
echo " Configuration script failed!"
exit 1
fi;;
3.11.2|3.12*|4.*)
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!"
exit 1;;
esac
CAMLTAG=OCAML`echo $CAMLVERSION | sed -e "s/\([1-9]\)\.\([0-9]*\).*/\1\2/g"`
# For coqmktop & bytecode compiler
if [ "$coq_debug_flag" = "-g" ]; then
case $CAMLTAG in
OCAML31*|OCAML4*)
# Compilation debug flag
coq_debug_flag_opt="-g"
;;
esac
fi
# Camlp4 / Camlp5 configuration
# Assume that camlp(4|5) binaries are at the same place as ocaml ones
# (this should become configurable some day)
CAMLP4BIN=${CAMLBIN}
case $usecamlp5 in
yes)
CAMLP4=camlp5
CAMLP4MOD=gramlib
if [ "$camlp5dir" != "" ]; then
if [ -f "$camlp5dir/${CAMLP4MOD}.cma" ]; then
CAMLP4LIB=$camlp5dir
FULLCAMLP4LIB=$camlp5dir
else
echo "Cannot find camlp5 libraries in $camlp5dir (camlp5.cma not found)."
echo "Configuration script failed!"
exit 1
fi
elif [ -f "${CAMLLIB}/camlp5/${CAMLP4MOD}.cma" ]; then
CAMLP4LIB=+camlp5
FULLCAMLP4LIB=${CAMLLIB}/camlp5
elif [ -f "${CAMLLIB}/site-lib/${CAMLP4MOD}.cma" ]; then
CAMLP4LIB=+site-lib/camlp5
FULLCAMLP4LIB=${CAMLLIB}/site-lib/camlp5
else
echo "No Camlp5 installation found. Looking for Camlp4 instead..."
usecamlp5=no
fi
esac
# If we're (still...) going to use Camlp5, let's check its version
case $usecamlp5 in
yes)
camlp4oexec=`echo "$camlp4oexec" | tr 4 5`
case `"$camlp4oexec" -v 2>&1` in
*"version 4.0"*|*5.00*)
echo "Camlp5 version < 5.01 not supported."
echo "Configuration script failed!"
exit 1;;
esac
esac
# We might now try to use Camlp4, either by explicit choice or
# by lack of proper Camlp5 installation
case $usecamlp5 in
no)
CAMLP4=camlp4
CAMLP4MOD=camlp4lib
CAMLP4LIB=+camlp4
FULLCAMLP4LIB=${CAMLLIB}/camlp4
if [ ! -f "${FULLCAMLP4LIB}/${CAMLP4MOD}.cma" ]; then
echo "No Camlp4 installation found."
echo "Configuration script failed!"
exit 1
fi
camlp4oexec=${camlp4oexec}rf
if [ "`"$camlp4oexec" 2>&1`" != "" ]; then
echo "Error: $camlp4oexec not found or not executable."
echo "Configuration script failed!"
exit 1
fi
esac
# 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 [ ! -f "${FULLCAMLP4LIB}/${CAMLP4MOD}.cmxa" ]; then
best_compiler=byte
echo "Cannot find native-code $CAMLP4,"
echo "only the bytecode version of Coq will be available."
elif [ ! -f "$CAMLLIB"/dynlink.cmxa ]; then
best_compiler=byte
echo "Cannot find native-code dynlink library,"
echo "only the bytecode version of Coq will be available."
echo "For building a native-code Coq, you may try to first"
echo "compile and install a dummy dynlink.cmxa (see dev/dynlink.ml)"
echo "and then run ./configure -natdynlink no"
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
# Native dynlink
if [ "$natdynlink" = "yes" -a -f "$CAMLLIB"/dynlink.cmxa ]; then
HASNATDYNLINK=true
else
HASNATDYNLINK=false
fi
case $HASNATDYNLINK,$ARCH,`uname -r`,$CAMLVERSION in
true,Darwin,9.*,3.11.*) # ocaml 3.11.0 dynlink on MacOS 10.5 is buggy
NATDYNLINKFLAG=os5fixme;;
#Possibly a problem on 10.6.0/10.6.1/10.6.2
#May just be a 32 vs 64 problem for all 10.6.*
true,Darwin,10.0.*,3.11.*) # Possibly a problem on 10.6.0
NATDYNLINKFLAG=os5fixme;;
true,Darwin,10.1.*,3.11.*) # Possibly a problem on 10.6.1
NATDYNLINKFLAG=os5fixme;;
true,Darwin,10.2.*,3.11.*) # Possibly a problem on 10.6.2
NATDYNLINKFLAG=os5fixme;;
true,Darwin,10.*,3.11.*)
if [ `getconf LONG_BIT` = "32" ]; then
# Still a problem for x86_32
NATDYNLINKFLAG=os5fixme
else
# Not a problem for x86_64
NATDYNLINKFLAG=$HASNATDYNLINK
fi;;
*)
NATDYNLINKFLAG=$HASNATDYNLINK;;
esac
# OS dependent libraries
OSDEPLIBS="-cclib -lunix"
case $ARCH in
sun4*) OS=`uname -r`
case $OS in
5*) OS="Sun Solaris $OS"
OSDEPLIBS="$OSDEPLIBS -cclib -lnsl -cclib -lsocket";;
*) OS="Sun OS $OS"
esac;;
esac
# lablgtk2 and CoqIDE
IDEARCHFLAGS=
IDEARCHFILE=
IDEARCHDEF=X11
# -byte-only should imply -coqide byte, unless the user decides otherwise
if [ "$best_compiler" = "byte" -a "$coqide_spec" = "no" ]; then
coqide_spec=yes
COQIDE=byte
fi
# Which coqide is asked ? which one is possible ?
if [ "$coqide_spec" = "yes" -a "$COQIDE" = "no" ]; then
echo "CoqIde disabled as requested."
else
case $lablgtkdir_spec in
no)
if lablgtkdirtmp=$(ocamlfind query lablgtk2.sourceview2 2> /dev/null); then
if [ ! -f "$lablgtkdirtmp/gSourceView2.cmi" ]; then
echo "Incomplete Lablgtk2 found by ocamlfind (gSourceView.cmi not found)."
elif [ ! -f "$lablgtkdirtmp/glib.mli" ]; then
echo "Incomplete Lablgtk2 found by ocamlfind (glib.mli not found)."
else
lablgtkdirfoundmsg="LabelGtk2 found by ocamlfind"
lablgtkdir=$lablgtkdirtmp
LABLGTKLIB=$lablgtkdir # Pour le message utilisateur
fi
fi
if [ "$lablgtkdir" = "" -a -f "${CAMLLIB}/lablgtk2/gSourceView2.cmi" -a -f "${CAMLLIB}/lablgtk2/glib.mli" ]; then
lablgtkdirfoundmsg="LablGtk2 found in ocaml lib directory"
lablgtkdir=${CAMLLIB}/lablgtk2
LABLGTKLIB=+lablgtk2 # Pour le message utilisateur
fi;;
yes)
if [ ! -d "$lablgtkdir" ]; then
echo "$lablgtkdir is not a valid directory."
echo "Configuration script failed!"
exit 1
elif [ ! -f "$lablgtkdir/gSourceView2.cmi" ]; then
echo "Incomplete LablGtk2 library (gSourceView2.cmi not found)."
echo "Make sure that the GtkSourceView bindings are available."
echo "Configuration script failed!"
exit 1
elif [ ! -f "$lablgtkdir/glib.mli" ]; then
echo "Incomplete LablGtk2 library (glib.mli not found)."
echo "Configuration script failed!"
exit 1
else
lablgtkdirfoundmsg="LablGtk2 directory found"
LABLGTKLIB=$lablgtkdir # Pour le message utilisateur
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 "$lablgtkdirfoundmsg but too old: CoqIde will not be available."
COQIDE=no;
elif [ "$coqide_spec" = "yes" -a "$COQIDE" = "byte" ]; then
echo "$lablgtkdirfoundmsg, bytecode CoqIde will be used as requested."
COQIDE=byte
elif [ ! -f "${CAMLLIB}/threads/threads.cmxa" -a -f "${lablgtkdir}/gtkThread.cmx" ]; then
echo "$lablgtkdirfoundmsg, not native (or no native threads): bytecode CoqIde will be available."
COQIDE=byte
else
echo "$lablgtkdirfoundmsg, native threads: native CoqIde will be available."
COQIDE=opt
if [ "$nomacintegration_spec" = "no" ] && lablgtkosxdir=$(ocamlfind query lablgtkosx 2> /dev/null);
then
IDEARCHFLAGS=lablgtkosx.cmxa
IDEARCHDEF=QUARTZ
elif [ "$ARCH" = "win32" ];
then
IDEARCHFLAGS=
IDEARCHFILE=ide/ide_win32_stubs.o
IDEARCHDEF=WIN32
fi
fi
fi
case $COQIDE in
byte|opt)
LABLGTKINCLUDES="-I $LABLGTKLIB";;
no)
LABLGTKINCLUDES="";;
esac
[ x$lablgtkosxdir = x ] || LABLGTKINCLUDES="$LABLGTKINCLUDES -I $lablgtkosxdir"
# strip command
case $ARCH in
Darwin) if [ "$HASNATDYNLINK" = "true" ]
then
STRIPCOMMAND="true"
else
STRIPCOMMAND="strip"
fi;;
*)
if [ "$coq_profile_flag" = "-p" ] || [ "$coq_debug_flag" = "-g" ]
then
STRIPCOMMAND="true"
else
STRIPCOMMAND="strip"
fi
esac
### Test if documentation can be compiled (latex, hevea)
if test "$with_doc" = "all"
then
for cmd in "latex" "hevea" ; do
if test ! -x "`which $cmd`"
then
echo "$cmd was not found; documentation will not be available"
with_doc=no
break
fi
done
fi
###########################################
# bindir, libdir, mandir, docdir, etc.
COQTOP=$PWD
# OCaml only understand Windows filenames (C:\...)
case $ARCH in
win32) COQTOP=`mk_win_path "$COQTOP"`
CAMLBIN=`mk_win_path "$CAMLBIN"`
CAMLP4BIN=`mk_win_path "$CAMLP4BIN"`
esac
# Default installation directories
case $ARCH$CYGWIN in
win32)
W32PREF='C:/coq/'
bindir_def="${W32PREF}bin"
libdir_def="${W32PREF}lib"
configdir_def="${W32PREF}config"
datadir_def="${W32PREF}share"
mandir_def="${W32PREF}man"
docdir_def="${W32PREF}doc"
emacslib_def="${W32PREF}emacs"
coqdocdir_def="${W32PREF}latex";;
*)
bindir_def=/usr/local/bin
libdir_def=/usr/local/lib/coq
configdir_def=/etc/xdg/coq
datadir_def=/usr/local/share/coq
mandir_def=/usr/local/share/man
docdir_def=/usr/local/share/doc/coq
emacslib_def=/usr/local/share/emacs/site-lisp
coqdocdir_def=/usr/local/share/texmf/tex/latex/misc;;
esac
askdir () {
printf "Where should I install $1 [%s]? " $2
read answer
if [ "$answer" = "" ]; then answer="$2"; fi
}
if [ $local = false ]; then
# Installation directories for a non-local build
case $bindir_spec/$prefix_spec in
yes/*) BINDIR=$bindir ;;
no/yes) BINDIR=$prefix/bin ;;
*) askdir "the Coq binaries" $bindir_def
BINDIR="$answer";;
esac
case $libdir_spec/$prefix_spec/$ARCH in
yes/*) LIBDIR=$libdir;;
no/yes/win32) LIBDIR=$prefix;;
no/yes/*) LIBDIR=$prefix/lib/coq ;;
*) askdir "the Coq library" $libdir_def
LIBDIR="$answer";;
esac
libdir_spec=yes
case $configdir_spec/$prefix_spec/$ARCH in
yes/*) CONFIGDIR=$configdir;;
no/yes/win32) CONFIGDIR=$prefix/config;;
no/yes/*) CONFIGDIR=$prefix/etc/xdg/coq;;
*) askdir "the Coqide configuration files" $configdir_def
CONFIGDIR="$answer";;
esac
if [ "$CONFIGDIR" != "$configdir_def" ]; then configdir_spec=yes; fi
case $datadir_spec/$prefix_spec in
yes/*) DATADIR=$datadir;;
no/yes) DATADIR=$prefix/share/coq;;
*) askdir "the Coqide data files" $datadir_def
DATADIR="$answer";;
esac
if [ "$DATADIR" != "datadir_def" ]; then datadir_spec=yes; fi
case $mandir_spec/$prefix_spec in
yes/*) MANDIR=$mandir;;
no/yes) MANDIR=$prefix/share/man ;;
*) askdir "the Coq man pages" $mandir_def
MANDIR="$answer";;
esac
case $docdir_spec/$prefix_spec in
yes/*) DOCDIR=$docdir;;
no/yes) DOCDIR=$prefix/share/doc/coq;;
*) askdir "the Coq documentation [%s]? " $docdir_def
DOCDIR="$answer";;
esac
case $emacslib_spec/$prefix_spec/$ARCH in
yes/*) EMACSLIB=$emacslib;;
no/yes/win32) EMACSLIB=$prefix/emacs ;;
no/yes/*) EMACSLIB=$prefix/share/emacs/site-lisp ;;
*) askdir "the Coq Emacs mode" $emacslib_def
EMACSLIB="$answer";;
esac
case $coqdocdir_spec/$prefix_spec/$ARCH in
yes/*) COQDOCDIR=$coqdocdir;;
no/yes/win32) COQDOCDIR=$prefix/latex ;;
no/yes/*) COQDOCDIR=$prefix/share/emacs/site-lisp ;;
*) askdir "Coqdoc TeX/LaTeX files" $coqdocdir_def
COQDOCDIR="$answer";;
esac
else # local build
CONFIGDIR=$COQTOP/ide
DATADIR=$COQTOP/ide
configdir_spec=yes
datadir_spec=yes
fi
# Determine if we enable -custom by default (Windows and MacOS)
CUSTOM_OS=no
if [ "$ARCH" = "win32" ] || [ "$ARCH" = "Darwin" ]; then
CUSTOM_OS=yes
fi
BUILDLDPATH="# you might want to set CAML_LD_LIBRARY_PATH by hand!"
case $coqrunbyteflags_spec/$local/$custom_spec/$CUSTOM_OS in
yes/*/*/*) COQRUNBYTEFLAGS="$coqrunbyteflags";;
*/*/yes/*|*/*/*/yes) COQRUNBYTEFLAGS="-custom";;
*/true/*/*) COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath '$COQTOP'/kernel/byterun";;
*)
COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath '$LIBDIR'"
BUILDLDPATH="export CAML_LD_LIBRARY_PATH='$COQTOP'/kernel/byterun";;
esac
case $coqtoolsbyteflags_spec/$custom_spec/$CUSTOM_OS in
yes/*/*) COQTOOLSBYTEFLAGS="$coqtoolsbyteflags";;
*/yes/*|*/*/yes) COQTOOLSBYTEFLAGS="-custom";;
*) COQTOOLSBYTEFLAGS="";;
esac
###########################################
# Summary of the configuration
echo ""
echo " Architecture : $ARCH"
if test ! -z "$OS" ; then
echo " Operating system : $OS"
fi
echo " Coq VM bytecode link flags : $COQRUNBYTEFLAGS"
echo " Coq tools bytecode link flags : $COQTOOLSBYTEFLAGS"
echo " OS dependent libraries : $OSDEPLIBS"
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 "$best_compiler" = opt ; then
echo " Native dynamic link support : $HASNATDYNLINK"
fi
if test "$COQIDE" != "no"; then
echo " Lablgtk2 library in : $LABLGTKLIB"
fi
if test "$IDEARCHDEF" = "QUARTZ"; then
echo " Mac OS integration is on"
fi
if test "$with_doc" = "all"; then
echo " Documentation : All"
else
echo " Documentation : None"
fi
echo " CoqIde : $COQIDE"
echo " Web browser : $BROWSER"
echo " Coq web site : $WWWCOQ"
echo ""
if test "$no_native_compiler" = "true"; then
echo " Native compiler for conversion and normalization disabled"
echo ""
fi
if test "$local" = "true"; then
echo " Local build, no installation..."
echo ""
else
echo " Paths for true installation:"
echo " binaries will be copied in $BINDIR"
echo " library will be copied in $LIBDIR"
echo " config files will be copied in $CONFIGDIR"
echo " data files will be copied in $DATADIR"
echo " man pages will be copied in $MANDIR"
echo " documentation will be copied in $DOCDIR"
echo " emacs mode will be copied in $EMACSLIB"
echo ""
fi
##################################################
# Building the dev/ocamldebug-coq file
##################################################
OCAMLDEBUGCOQ=dev/ocamldebug-coq
if test "$coq_debug_flag" = "-g" ; then
rm -f $OCAMLDEBUGCOQ
sed -e "s|COQTOPDIRECTORY|$COQTOP|" \
-e "s|CAMLBINDIRECTORY|$CAMLBIN|" \
-e "s|CAMLP4LIBDIRECTORY|$FULLCAMLP4LIB|"\
$OCAMLDEBUGCOQ.template > $OCAMLDEBUGCOQ
chmod a-w,a+x $OCAMLDEBUGCOQ
fi
##############################################
# Creation of configuration files
##############################################
mlconfig_file=config/coq_config.ml
mymlconfig_file=myocamlbuild_config.ml
config_file=config/Makefile
config_template=config/Makefile.template
### Warning !!
### After this line, be careful when using variables,
### since some of them will be escaped
escape_string () {
"$ocamlexec" "tools/escape_string.ml" "$1"
}
# Escaped version of browser command
BROWSER=`escape_string "$BROWSER"`
# Under Windows, we now escape the backslashes that will ends in
# ocaml strings (coq_config.ml) or in Makefile variables.
case $ARCH in
win32)
BINDIR=`escape_string "$BINDIR"`
LIBDIR=`escape_string "$LIBDIR"`
CONFIGDIR=`escape_string "$CONFIGDIR"`
DATADIR=`escape_string "$DATADIR"`
CAMLBIN=`escape_string "$CAMLBIN"`
CAMLLIB=`escape_string "$CAMLLIB"`
MANDIR=`escape_string "$MANDIR"`
DOCDIR=`escape_string "$DOCDIR"`
EMACSLIB=`escape_string "$EMACSLIB"`
COQDOCDIR=`escape_string "$COQDOCDIR"`
CAMLP4BIN=`escape_string "$CAMLP4BIN"`
CAMLP4LIB=`escape_string "$CAMLP4LIB"`
LABLGTKINCLUDES=`escape_string "$LABLGTKINCLUDES"`
COQRUNBYTEFLAGS=`escape_string "$COQRUNBYTEFLAGS"`
COQTOOLSBYTEFLAGS=`escape_string "$COQTOOLSBYTEFLAGS"`
BUILDLDPATH=`escape_string "$BUILDLDPATH"`
ocamlexec=`escape_string "$ocamlexec"`
bytecamlc=`escape_string "$bytecamlc"`
nativecamlc=`escape_string "$nativecamlc"`
ocamlmklibexec=`escape_string "$ocamlmklibexec"`
ocamldepexec=`escape_string "$ocamldepexec"`
ocamldocexec=`escape_string "$ocamldocexec"`
ocamllexexec=`escape_string "$ocamllexexec"`
ocamlyaccexec=`escape_string "$ocamlyaccexec"`
camlp4oexec=`escape_string "$camlp4oexec"`
;;
esac
case $libdir_spec in
yes) LIBDIR_OPTION="Some \"$LIBDIR\"";;
*) LIBDIR_OPTION="None";;
esac
case $configdir_spec in
yes) CONFIGDIR_OPTION="Some \"$CONFIGDIR\"";;
*) CONFIGDIR_OPTION="None";;
esac
case $datadir_spec in
yes) DATADIR_OPTION="Some \"$DATADIR\"";;
*) DATADIR_OPTION="None";;
esac
#####################################################
# Building the config/coq_config.ml file
#####################################################
rm -f "$mlconfig_file" "$mymlconfig_file"
cat << END_OF_COQ_CONFIG > $mlconfig_file
(* DO NOT EDIT THIS FILE: automatically generated by ../configure *)
let local = $local
let coqrunbyteflags = "$COQRUNBYTEFLAGS"
let coqlib = $LIBDIR_OPTION
let configdir = $CONFIGDIR_OPTION
let datadir = $DATADIR_OPTION
let docdir = "$DOCDIR"
let ocaml = "$ocamlexec"
let ocamlc = "$bytecamlc"
let ocamlopt = "$nativecamlc"
let ocamlmklib = "$ocamlmklibexec"
let ocamldep = "$ocamldepexec"
let ocamldoc = "$ocamldocexec"
let ocamlyacc = "$ocamlyaccexec"
let ocamllex = "$ocamllexexec"
let camlbin = "$CAMLBIN"
let camllib = "$CAMLLIB"
let camlp4 = "$CAMLP4"
let camlp4o = "$camlp4oexec"
let camlp4bin = "$CAMLP4BIN"
let camlp4lib = "$CAMLP4LIB"
let camlp4compat = "$CAMLP4COMPAT"
let coqideincl = "$LABLGTKINCLUDES"
let cflags = "$cflags"
let best = "$best_compiler"
let arch = "$ARCH"
let arch_is_win32 = $ARCH_WIN32
let has_coqide = "$COQIDE"
let gtk_platform = \`$IDEARCHDEF
let has_natdynlink = $HASNATDYNLINK
let natdynlinkflag = "$NATDYNLINKFLAG"
let osdeplibs = "$OSDEPLIBS"
let version = "$VERSION"
let caml_version = "$CAMLVERSION"
let date = "$DATE"
let compile_date = "$COMPILEDATE"
let vo_magic_number = $VOMAGIC
let state_magic_number = $STATEMAGIC
let exec_extension = "$EXE"
let with_geoproof = ref $with_geoproof
let browser = "$BROWSER"
let wwwcoq = "$WWWCOQ"
let wwwrefman = wwwcoq ^ "distrib/" ^ version ^ "/refman/"
let wwwstdlib = wwwcoq ^ "distrib/" ^ version ^ "/stdlib/"
let localwwwrefman = "file:/" ^ docdir ^ "html/refman"
let no_native_compiler = $no_native_compiler
END_OF_COQ_CONFIG
echo "let plugins_dirs = [" >> "$mlconfig_file"
find plugins/* \( -name .svn -prune \) -o \( -type d -exec printf "\"%s\";\n" {} \; \) >> "$mlconfig_file"
echo "]" >> "$mlconfig_file"
chmod a-w "$mlconfig_file"
ln -sf "$mlconfig_file" "$mymlconfig_file"
###############################################
# Building the config/Makefile file
###############################################
rm -f "$config_file"
cat << END_OF_MAKEFILE > $config_file
###### config/Makefile : Configuration file for Coq ##############
# #
# This file is generated by the script "configure" #
# DO NOT EDIT IT !! DO NOT EDIT IT !! DO NOT EDIT IT !! #
# If something is wrong below, then rerun the script "configure" #
# with the good options (see the file INSTALL). #
# #
##################################################################
#Variable used to detect whether ./configure has run successfully.
COQ_CONFIGURED=yes
# Local use (no installation)
LOCAL=$local
# Bytecode link flags for VM ("-custom" or "-dllib -lcoqrun")
COQRUNBYTEFLAGS=$COQRUNBYTEFLAGS
COQTOOLSBYTEFLAGS=$COQTOOLSBYTEFLAGS
$BUILDLDPATH
# Paths for true installation
# BINDIR=path where coqtop, coqc, coqmktop, coq-tex, coqdep, gallina and
# do_Makefile will reside
# LIBDIR=path where the Coq library will reside
# MANDIR=path where to install manual pages
# EMACSDIR=path where to put Coq's Emacs mode (coq.el)
BINDIR="$BINDIR"
COQLIBINSTALL="$LIBDIR"
CONFIGDIR="$CONFIGDIR"
DATADIR="$DATADIR"
MANDIR="$MANDIR"
DOCDIR="$DOCDIR"
EMACSLIB="$EMACSLIB"
EMACS=$EMACS
# Path to Coq distribution
VERSION=$VERSION
# Ocaml version number
CAMLVERSION=$CAMLTAG
# Ocaml libraries
CAMLLIB="$CAMLLIB"
# Ocaml .h directory
CAMLHLIB="$CAMLLIB"
# Camlp4 : flavor, binaries, libraries ...
# NB : CAMLP4BIN can be empty if camlp4 is in the PATH
# NB : avoid using CAMLP4LIB (conflict under Windows)
CAMLP4BIN="$CAMLP4BIN"
CAMLP4=$CAMLP4
CAMLP4O=$camlp4oexec
CAMLP4COMPAT=$CAMLP4COMPAT
MYCAMLP4LIB="$CAMLP4LIB"
# LablGTK
COQIDEINCLUDES=$LABLGTKINCLUDES
# Objective-Caml compile command
OCAML="$ocamlexec"
OCAMLC="$bytecamlc"
OCAMLMKLIB="$ocamlmklibexec"
OCAMLOPT="$nativecamlc"
OCAMLDEP="$ocamldepexec"
OCAMLDOC="$ocamldocexec"
OCAMLLEX="$ocamllexexec"
OCAMLYACC="$ocamlyaccexec"
# Caml link command and Caml make top command
CAMLLINK="$bytecamlc"
CAMLOPTLINK="$nativecamlc"
# Caml flags
CAMLFLAGS=-rectypes $coq_annotate_flag
TYPEREX=$coq_typerex_wrapper
# Compilation debug flags
CAMLDEBUG=$coq_debug_flag
CAMLDEBUGOPT=$coq_debug_flag_opt
# User compilation flag
USERFLAGS=
# Flags for GCC
CFLAGS=$cflags
# Compilation profile flag
CAMLTIMEPROF=$coq_profile_flag
# The best compiler: native (=opt) or bytecode (=byte) if no native compiler
BEST=$best_compiler
# Your architecture
# Can be obtain by UNIX command arch
ARCH=$ARCH
HASNATDYNLINK=$NATDYNLINKFLAG
# Supplementary libs for some systems, currently:
# . Sun Solaris: -cclib -lunix -cclib -lnsl -cclib -lsocket
# . others : -cclib -lunix
OSDEPLIBS=$OSDEPLIBS
# executable files extension, currently:
# Unix systems:
# Win32 systems : .exe
EXE=$EXE
DLLEXT=$DLLEXT
# the command MKDIR (try to replace it with mkdirhier if you have problems)
MKDIR=mkdir -p
# where to put the coqdoc.sty style file
COQDOCDIR="$COQDOCDIR"
#the command STRIP
# Unix systems and profiling: true
# Unix systems and no profiling: strip
STRIP=$STRIPCOMMAND
# CoqIde (no/byte/opt)
HASCOQIDE=$COQIDE
IDEOPTFLAGS=$IDEARCHFLAGS
IDEOPTDEPS=$IDEARCHFILE
IDEOPTINT=$IDEARCHDEF
# Defining REVISION
CHECKEDOUT=$checkedout
# Option to control compilation and installation of the documentation
WITHDOC=$with_doc
# make or sed are bogus and believe lines not terminating by a return
# are inexistent
END_OF_MAKEFILE
chmod a-w "$config_file"
##################################################
# The end
####################################################
echo "If anything in the above is wrong, please restart './configure'."
echo
echo "*Warning* To compile the system for a new architecture"
echo " don't forget to do a 'make clean' before './configure'."
Jump to Line
Something went wrong with that request. Please try again.