#!/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'."