#!/bin/sh

##################################
#
#  Configuration script for Coq
# 
##################################

VERSION=8.4pl4
VOMAGIC=08400
STATEMAGIC=58400
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 "-src <dir>"
    printf "\tSpecifies the source directory\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 "-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 <command>"
    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?"
    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
#####################################################

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

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 archclean' before './configure'."