configure

#!/bin/sh

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

VERSION=trunk
VOMAGIC=08211
STATEMAGIC=58211
DATE=`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"
    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"
    echo "-emacs"
    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 <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 "-with-cc <file>"
    echo "-with-ar <file>"
    echo "-with-ranlib <file>"
    printf "\tTells configure where to find gcc/ar/ranlib executables\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="-fno-defer-pop -Wall -Wno-unused"
natdynlink=yes

gcc_exec=gcc
ar_exec=ar
ranlib_exec=ranlib

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
                      shift;;
    -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"
		     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;;
    -with-cc|-with-gcc|--with-cc|--with-gcc) 
	  gcc_spec=yes
	  gcc_exec=$2
	  shift;;
    -with-ar|--with-ar) 
	  ar_spec=yes
	  ar_exec=$2
	  shift;;
    -with-ranlib|--with-ranlib) 
	  ranlib_spec=yes
	  ranlib_exec=$2
	  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=`date +"%h %d %Y %H:%M:%S"`;;
esac

# Architecture

case $arch_spec in
    no) 
    # First we test if we are running a Cygwin system
    if [ `uname -s | cut -c -6` = "CYGWIN" ] ; then
	ARCH="win32"
	CYGWIN=yes
    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
  MAKEVERSION=`$MAKE -v | head -1 | 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, OCaml only understands Windows filenames (C:\...)
case $ARCH in
    win32) CAMLBIN=`cygpath -m ${CAMLBIN}`;;
esac

CAMLVERSION=`"$bytecamlc" -version`

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

case $ARCH in
    win32) # Awfull trick to get around a ^M problem at the end of CAMLLIB
      CAMLLIB=`"$CAMLC" -where | sed -e 's/^\(.*\)$/\1/'` ;;
    *)
      CAMLLIB=`"$CAMLC" -where`
esac

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 `"$CAMLC" -where`/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}

if [ "$usecamlp5" = "yes" ]; then
    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 "Objective Caml $CAMLVERSION found but no Camlp5 installed."
	echo "Configuration script failed!"
	exit 1
    fi

    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

else # let's use camlp4
    CAMLP4=camlp4
    CAMLP4MOD=camlp4lib
    CAMLP4LIB=+camlp4
    FULLCAMLP4LIB=${CAMLLIB}/camlp4

    if [ ! -f "${FULLCAMLP4LIB}/${CAMLP4MOD}.cma" ]; then
	echo "Objective Caml $CAMLVERSION found but no Camlp4 installed."
	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
fi

# 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

case $ARCH in
  sun4*) OS=`uname -r`
	case $OS in
	   5*) OS="Sun Solaris $OS"
	       OSDEPLIBS="-cclib -lunix -cclib -lnsl -cclib -lsocket";;
	   *) OS="Sun OS $OS"
	      OSDEPLIBS="-cclib -lunix"
        esac;;
  win32) OS="Win32" 
	 OSDEPLIBS="-cclib -lunix"
	 cflags="-mno-cygwin $cflags";;
  *) OSDEPLIBS="-cclib -lunix"
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 lablgtkdir=$(ocamlfind query lablgtk2.sourceview2 2> /dev/null); then
                lablgtkdir_spec=yes
	    elif [ -f "${CAMLLIB}/lablgtk2/gSourceView2.mli" ]; then
		lablgtkdir=${CAMLLIB}/lablgtk2
	    fi;;
	yes)
	    if [ ! -f "$lablgtkdir/glib.mli" ]; then
		echo "Incorrect LablGtk2 library (glib.mli not found)."
		echo "Configuration script failed!"
		exit 1
	    fi;;
    esac
    if [ "$lablgtkdir" = "" ]; then
	echo "LablGtk2 not found: CoqIde will not be available."
	COQIDE=no
    elif [ -z "`grep -w convert_with_fallback "$lablgtkdir/glib.mli"`" ]; then
	echo "LablGtk2 found but too old: CoqIde will not be available."
	COQIDE=no;
    elif [ "$coqide_spec" = "yes" -a "$COQIDE" = "byte" ]; then 
	echo "LablGtk2 found, bytecode CoqIde will be used as requested."
	COQIDE=byte
    elif [ ! -f "${CAMLLIB}/threads/threads.cmxa" ]; then 
	echo "LablGtk2 found, no native threads: bytecode CoqIde will be available."
	COQIDE=byte
    else
        echo "LablGtk2 found, native threads: native CoqIde will be available."
	COQIDE=opt
        if [ "$nomacintegration_spec" = "no" ] && pkg-config --exists ige-mac-integration;
        then
            cflags=$cflags" `pkg-config --cflags ige-mac-integration`"
	    IDEARCHFLAGS='-ccopt "`pkg-config --libs ige-mac-integration`"'
	    IDEARCHFILE=ide/ide_mac_stubs.o
	    IDEARCHDEF=QUARTZ
	elif [ "$ARCH" = "win32" ];
        then
	    IDEARCHFLAGS=
	    IDEARCHFILE=ide/ide_win32_stubs.o
	    IDEARCHDEF=WIN32
	fi
    fi
fi

case $COQIDE in
    byte|opt)
        case $lablgtkdir_spec in
            no)  LABLGTKLIB=+lablgtk2                   # Pour le message
                 LABLGTKINCLUDES="-I $LABLGTKLIB";;     # Pour le makefile
            yes) LABLGTKLIB=$lablgtkdir               # Pour le message
                 LABLGTKINCLUDES="-I $LABLGTKLIB";; # Pour le makefile
        esac;;
    no) LABLGTKINCLUDES="";;
esac

# strip command

case $ARCH in
    win32)
	# true -> strip : it exists under cygwin !
	STRIPCOMMAND="strip";; 
    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

# mktexlsr
#MKTEXLSR=`which mktexlsr`
#case $MKTEXLSR in
#    "") MKTEXLSR=true;;
#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.

case $src_spec in
  no) COQTOP=${COQSRC}
esac

# OCaml only understand Windows filenames (C:\...)
case $ARCH in
    win32) COQTOP=`cygpath -m ${COQTOP}`
esac

case $ARCH$CYGWIN in
  win32)
	 W32PREF='C:\\coq\\'
	 bindir_def=${W32PREF}bin
	 libdir_def=${W32PREF}lib
	 configdir_def=${W32PREF}config
	 datadir_def=${W32PREF}data
	 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 [$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 [$libdir_def]? "
        read LIBDIR
        libdir_spec=yes
	case $LIBDIR in
	    "") LIBDIR=$libdir_def;;
	    *) true;;
	esac;;
esac

case $libdir_spec in
    yes) LIBDIR_OPTION="Some \"$LIBDIR\"";;
    *) LIBDIR_OPTION="None";;
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 [$configdir_def]? "
        read CONFIGDIR
	case $CONFIGDIR in
	    "") CONFIGDIR=$configdir_def;;
	    *) configdir_spec=yes;;
	esac;;
esac

case $configdir_spec in
    yes) CONFIGDIR_OPTION="Some \"$CONFIGDIR\"";;
    *) CONFIGDIR_OPTION="None";;
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 [$datadir_def]? "
        read DATADIR
	case $DATADIR in
	    "") DATADIR=$datadir_def;;
	    *) datadir_spec=yes;;
	esac;;
esac

case $datadir_spec in
    yes) DATADIR_OPTION="Some \"$DATADIR\"";;
    *) DATADIR_OPTION="None";;
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 [$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 [$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 [$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 [$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";;
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 [$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"
mymlconfig_file="$COQSRC/myocamlbuild_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


# An escaped version of a variable
escape_var () {
"$ocamlexec" 2>&1 1>/dev/null <<EOF
  prerr_endline(String.escaped(Sys.getenv"$VAR"));;
EOF
}

# Escaped version of browser command
export BROWSER
BROWSER=`VAR=BROWSER escape_var`

# damned backslashes under M$Windows
case $ARCH in
    win32)
	COQTOP=`echo $COQTOP |sed -e 's|\\\|\\\\\\\|g'`
	BINDIR=`echo $BINDIR |sed -e 's|\\\|\\\\\\\|g'`
	COQSRC=`cygpath -m $COQSRC |sed -e 's|\\\|\\\\\\\|g'`
	LIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'`
	CONFIGDIR=`echo $CONFIGDIR |sed -e 's|\\\|\\\\\\\|g'`
	DATADIR=`echo $DATADIR |sed -e 's|\\\|\\\\\\\|g'`
	CAMLBIN=`echo $CAMLBIN |sed -e 's|\\\|\\\\\\\|g'`
	CAMLLIB=`echo $CAMLLIB |sed -e 's|\\\|\\\\\\\|g'`
	MANDIR=`echo $MANDIR |sed -e 's|\\\|\\\\\\\|g'`
	DOCDIR=`echo $DOCDIR |sed -e 's|\\\|\\\\\\\|g'`
	EMACSLIB=`echo $EMACSLIB |sed -e 's|\\\|\\\\\\\|g'`
	COQDOCDIR=`echo $COQDOCDIR |sed -e 's|\\\|\\\\\\\|g'`
	CAMLP4BIN=`echo $CAMLP4BIN |sed -e 's|\\\|\\\\\\\|g'`
	CAMLP4LIB=`echo $CAMLP4LIB |sed -e 's|\\\|\\\\\\\|g'`
	LABLGTKINCLUDES=`echo $LABLGTKINCLUDES |sed -e 's|\\\|\\\\\\\|g'`
	COQRUNBYTEFLAGS=`echo $COQRUNBYTEFLAGS |sed -e 's|\\\|\\\\\\\|g'`
	COQTOOLSBYTEFLAGS=`echo $COQTOOLSBYTEFLAGS |sed -e 's|\\\|\\\\\\\|g'`
	BUILDLDPATH=`echo $BUILDLDPATH |sed -e 's|\\\|\\\\\\\|g'`
	ocamlexec=`echo $ocamlexec |sed -e 's|\\\|\\\\\\\|g'`
	bytecamlc=`echo $bytecamlc |sed -e 's|\\\|\\\\\\\|g'`
	nativecamlc=`echo $nativecamlc |sed -e 's|\\\|\\\\\\\|g'`
	ocamlmklibexec=`echo $ocamlmklibexec |sed -e 's|\\\|\\\\\\\|g'`
	ocamldepexec=`echo $ocamldepexec |sed -e 's|\\\|\\\\\\\|g'`
	ocamldocexec=`echo $ocamldocexec |sed -e 's|\\\|\\\\\\\|g'`
	ocamllexexec=`echo $ocamllexexec |sed -e 's|\\\|\\\\\\\|g'`
	ocamlyaccexec=`echo $ocamlyaccexec |sed -e 's|\\\|\\\\\\\|g'`
	camlp4oexec=`echo $camlp4oexec |sed -e 's|\\\|\\\\\\\|g'`
    ;;
esac

#####################################################
# Integer arithmetic matching the architecture      #
#####################################################
if [ `getconf LONG_BIT` = "64" ]; then
  cp $COQSRC/kernel/uint63_amd64.ml $COQSRC/kernel/uint63.ml
else
  cp $COQSRC/kernel/uint63_x86.ml $COQSRC/kernel/uint63.ml
fi


#####################################################
# Building the $COQTOP/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 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"
ln -sf "$mlconfig_file" "$mymlconfig_file"

###############################################
# Building the $COQTOP/config/Makefile file
###############################################

rm -f "$config_file"

sed -e "s|LOCALINSTALLATION|$local|" \
    -e "s|XCOQRUNBYTEFLAGS|$COQRUNBYTEFLAGS|" \
    -e "s|XCOQTOOLSBYTEFLAGS|$COQTOOLSBYTEFLAGS|" \
    -e "s|COQSRCDIRECTORY|$COQSRC|" \
    -e "s|COQVERSION|$VERSION|" \
    -e "s|BINDIRDIRECTORY|$BINDIR|" \
    -e "s|COQLIBDIRECTORY|$LIBDIR|" \
    -e "s|CONFIGDIRDIRECTORY|$CONFIGDIR|" \
    -e "s|DATADIRDIRECTORY|$DATADIR|" \
    -e "s|BUILDLDPATH=|$BUILDLDPATH|" \
    -e "s|MANDIRDIRECTORY|$MANDIR|" \
    -e "s|DOCDIRDIRECTORY|$DOCDIR|" \
    -e "s|EMACSLIBDIRECTORY|$EMACSLIB|" \
    -e "s|EMACSCOMMAND|$EMACS|" \
    -e "s|COQDOCDIRECTORY|$COQDOCDIR|" \
    -e "s|MKTEXLSRCOMMAND|$MKTEXLSR|" \
    -e "s|ARCHITECTURE|$ARCH|" \
    -e "s|OSDEPENDENTLIBS|$OSDEPLIBS|" \
    -e "s|OSDEPENDENTP4OPTFLAGS|$OSDEPP4OPTFLAGS|" \
    -e "s|CAMLLIBDIRECTORY|$CAMLLIB|" \
    -e "s|CAMLTAG|$CAMLTAG|" \
    -e "s|CAMLP4VARIANT|$CAMLP4|" \
    -e "s|CAMLP4BINDIRECTORY|$CAMLP4BIN|" \
    -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIB|" \
    -e "s|CAMLP4TOOL|$camlp4oexec|" \
    -e "s|CAMLP4COMPATFLAGS|$CAMLP4COMPAT|" \
    -e "s|LABLGTKINCLUDES|$LABLGTKINCLUDES|" \
    -e "s|COQDEBUGFLAGOPT|$coq_debug_flag_opt|" \
    -e "s|COQDEBUGFLAG|$coq_debug_flag|" \
    -e "s|COQPROFILEFLAG|$coq_profile_flag|" \
    -e "s|CAMLANNOTATEFLAG|$coq_annotate_flag|" \
    -e "s|CCOMPILEFLAGS|$cflags|" \
    -e "s|BESTCOMPILER|$best_compiler|" \
    -e "s|DLLEXTENSION|$DLLEXT|" \
    -e "s|EXECUTEEXTENSION|$EXE|" \
    -e "s|BYTECAMLC|$bytecamlc|" \
    -e "s|OCAMLMKLIBEXEC|$ocamlmklibexec|" \
    -e "s|NATIVECAMLC|$nativecamlc|" \
    -e "s|OCAMLEXEC|$ocamlexec|" \
    -e "s|OCAMLDEPEXEC|$ocamldepexec|" \
    -e "s|OCAMLDOCEXEC|$ocamldocexec|" \
    -e "s|OCAMLLEXEXEC|$ocamllexexec|" \
    -e "s|OCAMLYACCEXEC|$ocamlyaccexec|" \
    -e "s|CAMLMKTOPEXEC|$ocamlmktopexec|" \
    -e "s|CCEXEC|$gcc_exec|" \
    -e "s|AREXEC|$ar_exec|" \
    -e "s|RANLIBEXEC|$ranlib_exec|" \
    -e "s|STRIPCOMMAND|$STRIPCOMMAND|" \
    -e "s|COQIDEOPT|$COQIDE|" \
    -e "s|IDEARCHFLAGS|$IDEARCHFLAGS|" \
    -e "s|IDEARCHFILE|$IDEARCHFILE|" \
    -e "s|IDEARCHDEF|$IDEARCHDEF|" \
    -e "s|CHECKEDOUTSOURCETREE|$checkedout|" \
    -e "s|WITHDOCOPT|$with_doc|" \
    -e "s|HASNATIVEDYNLINK|$NATDYNLINKFLAG|" \
      "$config_template" > "$config_file"

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'."