From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- configure | 1305 ++----------------------------------------------------------- 1 file changed, 24 insertions(+), 1281 deletions(-) (limited to 'configure') diff --git a/configure b/configure index cb43a73d..09585e59 100755 --- a/configure +++ b/configure @@ -1,1294 +1,37 @@ #!/bin/sh -################################## -# -# Configuration script for Coq -# -################################## +## This micro-configure shell script is here only to +## launch the real configuration via ocaml -VERSION=8.4pl4 -VOMAGIC=08400 -STATEMAGIC=58400 -DATE=`LC_ALL=C LANG=C date +"%B %Y"` +cmd=ocaml +script=./configure.ml -# 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 " - printf "\tSet installation directory to \n" - echo "-local" - printf "\tSet installation directory to the current source tree\n" - echo "-coqrunbyteflags " - printf "\tSet link flags for VM-dependent bytecode (coqtop)\n" - echo "-coqtoolsbyteflags " - printf "\tSet link flags for VM-independant bytecode (coqdep, coqdoc, ...)\n" - echo "-custom" - printf "\tGenerate all bytecode executables with -custom (not recommended)\n" - echo "-src " - printf "\tSpecifies the source directory\n" - echo "-bindir " - echo "-libdir " - echo "-configdir " - echo "-datadir " - echo "-mandir " - echo "-docdir " - printf "\tSpecifies where to install bin/lib/config/data/man/doc files resp.\n" - echo "-emacslib " - printf "\tSpecifies where emacs files are to be installed\n" - echo "-coqdocdir " - printf "\tSpecifies where Coqdoc style files are to be installed\n" - echo "-camldir " - printf "\tSpecifies the path to the OCaml library\n" - echo "-lablgtkdir " - 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 " - printf "\tSpecifies where to look for the Camlp5 library and tells to use it\n" - echo "-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 " - printf "\tUse to open URL %%s\n" - echo "-with-doc (yes|no)" - printf "\tSpecifies whether or not to 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 "-makecmd " - printf "\tName of GNU Make command.\n" -} - - -# Default OCaml binaries -bytecamlc=ocamlc -nativecamlc=ocamlopt -ocamlmklibexec=ocamlmklib -ocamlexec=ocaml -ocamldepexec=ocamldep -ocamldocexec=ocamldoc -ocamllexexec=ocamllex -ocamlyaccexec=ocamlyacc -ocamlmktopexec=ocamlmktop -camlp4oexec=camlp4o - - -coq_debug_flag= -coq_debug_flag_opt= -coq_profile_flag= -coq_annotate_flag= -best_compiler=opt -cflags="-Wall -Wno-unused" -natdynlink=yes - -local=false -coqrunbyteflags_spec=no -coqtoolsbyteflags_spec=no -custom_spec=no -src_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 - -COQSRC=`pwd` - -# 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;; - -src|--src) src_spec=yes - COQSRC="$2" - shift;; - -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;; - -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;; - -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) - EXE=".exe" - DLLEXT=".dll";; - *) 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 - # Beware of the final \r in Win32 - MAKEVERSION=`"$MAKE" -v | head -1 | tr -d "\r" | cut -d" " -f3` - MAKEVERSIONMAJOR=`echo $MAKEVERSION | cut -d. -f1` - MAKEVERSIONMINOR=`echo $MAKEVERSION | cut -d. -f2` - if [ "$MAKEVERSIONMAJOR" -gt 3 -o "$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 - ocamlmktopexec=$CAMLBIN/ocamlmktop - ocamlmklibexec=$CAMLBIN/ocamlmklib - camlp4oexec=$CAMLBIN/camlp4o -esac - -if test ! -f "$CAMLC" ; then - echo "I can not find the executable '$CAMLC'. Have you installed it?" +if [ ! -f $script ]; then + echo "Error: file $script not found in the current directory." + echo "Please run the configure script from the root of the coq sources." 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,$src_spec in - win32,yes) echo "Error: the -src option is currently not supported on Windows" - exit 1;; - 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 - -# 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 - -# 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 - else - # Beware of the final \r in Win32 - camlp5dir="$(camlp5 -where | tr -d '\r')" - if [ "$camlp5dir" != "" ]; then - CAMLP4LIB=$camlp5dir - FULLCAMLP4LIB=$camlp5dir - 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 - 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." - 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 - -# 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) - # Beware of the final \r in Win32 - lablgtkdirtmp="$(ocamlfind query lablgtk2 2> /dev/null | tr -d '\r')" - if [ "$lablgtkdirtmp" != "" ]; then - if [ -f "$lablgtkdirtmp/glib.cmi" -a -f "$lablgtkdirtmp/glib.mli" ]; then - lablgtkdirfoundmsg="LabelGtk2 found by ocamlfind" - lablgtkdir=$lablgtkdirtmp - LABLGTKLIB=$lablgtkdir # Pour le message utilisateur - else - echo "Headers missings in Lablgtk2 found by ocamlfind (glib.cmi/glib.mli not found)." - fi - fi - if [ "$lablgtkdir" = "" -a -f "${CAMLLIB}/lablgtk2/glib.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/glib.cmi" -a -f "$lablgtkdir/glib.mli" ]; then - lablgtkdirfoundmsg="LablGtk2 directory found" - LABLGTKLIB=$lablgtkdir # Pour le message utilisateur - else - echo "Headers missing in LablGtk2 library (glib.cmi/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 "$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" ]; then - echo "$lablgtkdirfoundmsg, 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. - -# OCaml only understand Windows filenames (C:\...) -case $ARCH in - win32) COQSRC=`mk_win_path "$COQSRC"` - CAMLBIN=`mk_win_path "$CAMLBIN"` - CAMLP4BIN=`mk_win_path "$CAMLP4BIN"` -esac - -case $src_spec in - no) COQTOP=${COQSRC} -esac - -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 - -emacs_def=emacs - -case $bindir_spec/$prefix_spec/$local in - yes/*/*) BINDIR=$bindir ;; - */yes/*) BINDIR=$prefix/bin ;; - */*/true) BINDIR=$COQTOP/bin ;; - *) printf "Where should I install the Coq binaries [%s]? " "$bindir_def" - read BINDIR - case $BINDIR in - "") BINDIR=$bindir_def;; - *) true;; - esac;; -esac - -case $libdir_spec/$prefix_spec/$local in - yes/*/*) LIBDIR=$libdir;; - */yes/*) - libdir_spec=yes - case $ARCH in - win32) LIBDIR=$prefix ;; - *) LIBDIR=$prefix/lib/coq ;; - esac ;; - */*/true) LIBDIR=$COQTOP ;; - *) printf "Where should I install the Coq library [%s]? " "$libdir_def" - read LIBDIR - libdir_spec=yes - case $LIBDIR in - "") LIBDIR=$libdir_def;; - *) true;; - esac;; -esac - -case $configdir_spec/$prefix_spec/$local in - yes/*/*) CONFIGDIR=$configdir;; - */yes/*) configdir_spec=yes - case $ARCH in - win32) CONFIGDIR=$prefix/config;; - *) CONFIGDIR=$prefix/etc/xdg/coq;; - esac;; - */*/true) CONFIGDIR=$COQTOP/ide - configdir_spec=yes;; - *) printf "Where should I install the Coqide configuration files [%s]? " "$configdir_def" - read CONFIGDIR - case $CONFIGDIR in - "") CONFIGDIR=$configdir_def;; - *) configdir_spec=yes;; - esac;; -esac - -case $datadir_spec/$prefix_spec/$local in - yes/*/*) DATADIR=$datadir;; - */yes/*) DATADIR=$prefix/share/coq;; - */*/true) DATADIR=$COQTOP/ide - datadir_spec=yes;; - *) printf "Where should I install the Coqide data files [%s]? " "$datadir_def" - read DATADIR - case $DATADIR in - "") DATADIR=$datadir_def;; - *) datadir_spec=yes;; - esac;; -esac - -case $mandir_spec/$prefix_spec/$local in - yes/*/*) MANDIR=$mandir;; - */yes/*) MANDIR=$prefix/share/man ;; - */*/true) MANDIR=$COQTOP/man ;; - *) printf "Where should I install the Coq man pages [%s]? " "$mandir_def" - read MANDIR - case $MANDIR in - "") MANDIR=$mandir_def;; - *) true;; - esac;; -esac - -case $docdir_spec/$prefix_spec/$local in - yes/*/*) DOCDIR=$docdir;; - */yes/*) DOCDIR=$prefix/share/doc/coq;; - */*/true) DOCDIR=$COQTOP/doc;; - *) printf "Where should I install the Coq documentation [%s]? " "$docdir_def" - read DOCDIR - case $DOCDIR in - "") DOCDIR=$docdir_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 ;; - *) printf "Where should I install the Coq Emacs mode [%s]? " "$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 ;; - *) printf "Where should I install Coqdoc TeX/LaTeX files [%s]? " "$coqdocdir_def" - read COQDOCDIR - case $COQDOCDIR in - "") COQDOCDIR=$coqdocdir_def;; - *) true;; - esac;; -esac - -# 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:$CAML_LD_LIBRARY_PATH";; -esac -case $coqtoolsbyteflags_spec/$custom_spec/$CUSTOM_OS in - yes/*/*) COQTOOLSBYTEFLAGS="$coqtoolsbyteflags";; - */yes/*|*/*/yes) COQTOOLSBYTEFLAGS="-custom";; - *) COQTOOLSBYTEFLAGS="";; -esac - -# case $emacs_spec in -# no) printf "Which Emacs command should I use to compile coq.el [%s]? " "$emacs_def" -# read EMACS - -# case $EMACS in -# "") EMACS="$emacs_def";; -# *) true;; -# esac;; -# yes) EMACS="$emacs";; -# esac - - - -########################################### -# Summary of the configuration - -echo "" -echo " Coq top directory : $COQTOP" -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 "" - -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 "" - -################################################## -# Building the $COQTOP/dev/ocamldebug-coq file -################################################## - -OCAMLDEBUGCOQ=$COQSRC/dev/ocamldebug-coq - -if test "$coq_debug_flag" = "-g" ; then - rm -f $OCAMLDEBUGCOQ - sed -e "s|COQTOPDIRECTORY|$COQTOP|" \ - -e "s|COQLIBDIRECTORY|$LIBDIR|" \ - -e "s|CAMLBINDIRECTORY|$CAMLBIN|" \ - -e "s|CAMLP4LIBDIRECTORY|$FULLCAMLP4LIB|"\ - $OCAMLDEBUGCOQ.template > $OCAMLDEBUGCOQ - chmod a-w,a+x $OCAMLDEBUGCOQ -fi - -#################################################### -# Fixing lablgtk types (before/after 2.6.0) -#################################################### - -if [ ! "$COQIDE" = "no" ]; then - if grep "class view " "$lablgtkdir/gText.mli" | grep -q "\[>" ; then - if grep -q "?accepts_tab:bool" "$lablgtkdir/gText.mli" ; then - cp -f ide/undo_lablgtk_ge212.mli ide/undo.mli - else - cp -f ide/undo_lablgtk_ge26.mli ide/undo.mli - fi - else - cp -f ide/undo_lablgtk_lt26.mli ide/undo.mli - fi -fi - -############################################## -# Creation of configuration files -############################################## - -mlconfig_file="$COQSRC/config/coq_config.ml" -config_file="$COQSRC/config/Makefile" -config_template="$COQSRC/config/Makefile.template" - - -### Warning !! -### After this line, be careful when using variables, -### since some of them (e.g. $COQSRC) 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) - COQTOP=`escape_string "$COQTOP"` - BINDIR=`escape_string "$BINDIR"` - COQSRC=`escape_string "$COQSRC"` - 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 $COQTOP/config/coq_config.ml file -##################################################### +## Parse the args, only looking for -camldir +## We avoid using shift to keep "$@" intact -rm -f "$mlconfig_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 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" - -END_OF_COQ_CONFIG - -# to be sure printf is found on windows when spaces occur in PATH variable -PRINTF=`which printf` - -# Subdirectories of theories/ added in coq_config.ml -subdirs () { - (cd $1; find * \( -name .svn -prune \) -o \( -type d -exec $PRINTF "\"%s\";\n" {} \; \) >> "$mlconfig_file") -} - -echo "let theories_dirs = [" >> "$mlconfig_file" -subdirs theories -echo "]" >> "$mlconfig_file" - -echo "let plugins_dirs = [" >> "$mlconfig_file" -subdirs plugins -echo "]" >> "$mlconfig_file" - -chmod a-w "$mlconfig_file" - - -############################################### -# Building the $COQTOP/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 -COQSRC="$COQSRC" -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" -CAMLMKTOP="$ocamlmktopexec" - -# Caml flags -CAMLFLAGS=-rectypes $coq_annotate_flag - -# 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 +last= +for i; do + case $last in + -camldir|--camldir) cmd="$i/ocaml"; break;; + esac + last=$i +done -chmod a-w "$config_file" +## We check that $cmd is ok before the real exec $cmd -################################################## -# The end -#################################################### +`$cmd -version > /dev/null 2>&1` && exec $cmd $script "$@" -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 archclean' before './configure'." +## If we're still here, something is wrong with $cmd +echo "Error: failed to run $cmd" +echo "Please use the option -camldir if 'ocaml' is installed" +echo "in directory , or add to your path." +echo "Configuration script failed!" +exit 1 -- cgit v1.2.3