#!/bin/sh

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

VERSION=8.2rc2
VOMAGIC=08193 
STATEMAGIC=19764
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\n"
    echo "-src"
    printf "\tSpecifies the source directory\n"
    echo "-bindir"
    echo "-libdir"
    echo "-mandir"
    echo "-docdir"
    printf "\tSpecifies where to install bin/lib/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 "-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 "-fsets (all|basic)"
    echo "-reals (all|basic)"
    printf "\tSpecifies whether or not to compile full FSets/Reals library\n"
    echo "-coqide (opt|byte|no)"
    printf "\tSpecifies whether or not to compile Coqide\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"
}


# 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"

gcc_exec=gcc
ar_exec=ar
ranlib_exec=ranlib

local=false
coqrunbyteflags_spec=no
src_spec=no
prefix_spec=no
bindir_spec=no
libdir_spec=no
mandir_spec=no
docdir_spec=no
emacslib_spec=no
emacs_spec=no
camldir_spec=no
lablgtkdir_spec=no
coqdocdir_spec=no
fsets=all
reals=all
arch_spec=no
coqide_spec=no
browser_spec=no
with_geoproof=false
with_doc=all
with_doc_spec=no

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;;
    -src|--src) src_spec=yes
                COQSRC="$2"
	        shift;;
    -bindir|--bindir) bindir_spec=yes
                      bindir="$2"
		      shift;;
    -libdir|--libdir) libdir_spec=yes
                      libdir="$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;;
    -camlp5dir|--camlp5dir)
	                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;;
    -fsets|--fsets) case "$2" in
			yes|all) fsets=all;;
			*) fsets=basic
		    esac
		    shift;;
    -reals|--reals) case "$2" in
			yes|all) reals=all;;
			*) reals=basic
		    esac
		    shift;;
    -coqide|--coqide) coqide_spec=yes
		      case "$2" in
			  byte|opt) COQIDE=$2;;
			  *) COQIDE=no
		      esac
		      shift;;
    -browser|--browser) browser_spec=yes
		      BROWSER=$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;;
    -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;;
    *) 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"
    else
	# If not, we determine the architecture
	if 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`
 	elif test -x /bin/uname ; then
 	    ARCH=`/bin/uname -s`
 	elif test -x /usr/bin/uname ; then
 	    ARCH=`/usr/bin/uname -s`
	else
	    echo "I can not automatically find the name of your architecture"
	    echo -n\
		"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 make`
if [ "$MAKE" != "" ]; then
  MAKEVERSION=`$MAKE -v | head -1`
  case $MAKEVERSION in
    "GNU Make 3.81") 
      echo "You have GNU Make 3.81. Good!";;
    *)
      OK="no"
      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
  esac
else
  echo "Cannot find GNU Make 3.81"
fi

# Browser command

if [ "$browser_spec" = "no" ]; then
    case $ARCH in
        win32) BROWSER='C:\PROGRA~1\INTERN~1\IEXPLORE %s' ;;
        *) BROWSER='firefox -remote "OpenURL(%s,new-tab)" || firefox %s &' ;;
    esac
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 -w ${CAMLBIN}`;;
esac

# this fixes a camlp4 bug under FreeBSD
# ("native-code program cannot do a dynamic load")
if [ `uname -s` = "FreeBSD" ]; then camlp4oexec=$camlp4oexec.byte; fi

CAMLVERSION=`"$bytecamlc" -version`

case $CAMLVERSION in
    1.*|2.*|3.00|3.01|3.02|3.03|3.03alpha|3.04|3.05beta|3.05|3.06|3.08.0)
	echo "Your version of Objective-Caml is $CAMLVERSION."
	if [ "$CAMLVERSION" = "3.08.0" ] ; then
	    echo "You need Objective-Caml 3.07 or later (to the exception of 3.08.0)!"
	else
	    echo "You need Objective-Caml 3.07 or later!"
	fi
	echo "Configuration script failed!"
	exit 1;;
    3.07*|3.08*)
	echo "You have Objective-Caml $CAMLVERSION. Good!";;
    ?*)
	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

# We need to set va special flag for OCaml 3.07
case  $CAMLVERSION in 
	3.07*)
	  cflags="$cflags -DOCAML_307";;
esac

if [ "$coq_debug_flag" = "-g" ]; then
    case $CAMLTAG in
        OCAML31*)
            # Compilation debug flag
            coq_debug_flag_opt="-g"
            ;;
    esac
fi

# Native dynlink
if test -f `"$CAMLC" -where`/dynlink.cmxa; then
    HASNATDYNLINK=true
else
    HASNATDYNLINK=false
fi

# Camlp4 / Camlp5 configuration

if [ "$camlp5dir" != "" ]; then
    CAMLP4=camlp5
    CAMLP4LIB=$camlp5dir
    if [ ! -f $camlp5dir/camlp5.cma ]; then
	echo "Cannot find camlp5 libraries in $camlp5dir (camlp5.cma not found)"
	echo "Configuration script failed!"
	exit 1
    fi
    camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'`
    if [ `$camlp4oexec -pmode 2>&1` = "strict" ]; then 
	echo "Error: Camlp5 found, but in strict mode!"
	echo "Please compile Camlp5 in transitional mode."
	exit 1
    fi
else
    case $CAMLTAG in
        OCAML31*)
            if [ -x "${CAMLLIB}/camlp5" ]; then
                CAMLP4LIB=+camlp5
            elif [ -x "${CAMLLIB}/site-lib/camlp5" ]; then
                CAMLP4LIB=+site-lib/camlp5
            else
	        echo "Objective Caml $CAMLVERSION found but no Camlp5 installed."
	        echo "Configuration script failed!"
	        exit 1
            fi
            CAMLP4=camlp5
            camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'`
            if [ `$camlp4oexec -pmode 2>&1` = "strict" ]; then
	        echo "Error: Camlp5 found, but in strict mode!"
	        echo "Please compile Camlp5 in transitional mode."
	        exit 1
            fi
            ;;
        *)
            CAMLP4=camlp4
            CAMLP4LIB=+camlp4
            ;;
    esac
fi

if [ "$CAMLP4" = "camlp5" ] && `$camlp4oexec -v 2>&1 | grep -q 5.00`; then
    echo "Camlp5 version 5.00 not supported: versions 4.0x or >= 5.01 are OK."
    echo "Configuration script failed!"
    exit 1
fi


case $CAMLP4LIB in
    +*) FULLCAMLP4LIB=$CAMLLIB/`echo $CAMLP4LIB | cut -b 2-`;;
    *)  FULLCAMLP4LIB=$CAMLP4LIB;;
esac

# Assume that camlp(4|5) binaries are at the same place as ocaml ones
# (this should become configurable some day) 
CAMLP4BIN=${CAMLBIN}

# 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 [ "`uname -s`" = "Darwin" -a "$ARCH" = "i386" ]; then
	  case $CAMLOPTVERSION in
	      3.09.3|3.1?*) ;;
	      *) echo "Native compilation on MacOS X Pentium requires Objective-Caml >= 3.09.3,"
		 best_compiler=byte
		 echo "only the bytecode version of Coq will be available."
	  esac
      elif [ ! -f $FULLCAMLP4LIB/gramlib.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;;
  alpha) OSDEPLIBS="-cclib -lunix";;
  win32) OS="Win32" 
	 OSDEPLIBS="-cclib -lunix"
	 cflags="-mno-cygwin $cflags";;
  *) OSDEPLIBS="-cclib -lunix"
esac

# lablgtk2 and CoqIDE

# -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 [ -f "${CAMLLIB}/lablgtk2/glib.mli" ]; then
		lablgtkdir=${CAMLLIB}/lablgtk2
	    elif [ -f "${CAMLLIB}/site-lib/lablgtk2/glib.mli" ]; then
		lablgtkdir=${CAMLLIB}/site-lib/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
    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

# Tell on windows if ocaml understands cygwin or windows path formats

#"$CAMLC" -o config/giveostype config/giveostype.ml
#CAMLOSTYPE=`config/giveostype`
#rm config/giveostype

# strip command

case $ARCH in
    win32)
	# true -> strip : it exists under cygwin !
	STRIPCOMMAND="strip";; 
    *)
    if [ "$coq_profile_flag" = "-p" ] || [ "$coq_debug_flag" = "-g" ] ||
       [ "`uname -s`" = "Darwin" -a "$HASNATDYNLINK" = "true" ]
    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
    if test "`which latex`" = ""
    then 
	echo "latex was not found; documentation will not be available"
	with_doc=no
    else
	if test "`which hevea`" = ""
	then
	    with_doc=no
	    echo "hevea was not found: documentation will not be available"
	fi
    fi
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 -w ${COQTOP}`
esac

case $ARCH in
  win32)
	 bindir_def='C:\coq\bin'
	 libdir_def='C:\coq\lib'
	 mandir_def='C:\coq\man'
	 docdir_def='C:\coq\doc'
	 emacslib_def='C:\coq\emacs'
         coqdocdir_def='C:\coq\latex';;
  *)
	 bindir_def=/usr/local/bin
	 libdir_def=/usr/local/lib/coq
	 mandir_def=/usr/local/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/*)
        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
	case $LIBDIR in
	    "") LIBDIR=$libdir_def;;
	    *) true;;
	esac;;
esac

case $mandir_spec/$prefix_spec/$local in
    yes/*/*) MANDIR=$mandir;;
    */yes/*) MANDIR=$prefix/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/man ;;
    *)  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

BUILDLDPATH="# you might want to set CAML_LD_LIBRARY_PATH by hand!"
case $coqrunbyteflags_spec/$local in
    yes/*) COQRUNBYTEFLAGS="$coqrunbyteflags";;
    */true) COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath $COQTOP/kernel/byterun";;
    *) COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath $LIBDIR"
       BUILDLDPATH="export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun";;
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 "  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 "$COQIDE" != "no"; then
echo "  Lablgtk2 library in               : $LABLGTKLIB"
fi
if test "$fsets" = "all"; then
echo "  FSets theory                      : All"
else
echo "  FSets theory                      : Basic"
fi
if test "$reals" = "all"; then
echo "  Reals theory                      : All"
else
echo "  Reals theory                      : Basic"
fi
if test "$with_doc" = "all"; then
echo "  Documentation                     : All"
else
echo "  Documentation                     : None"
fi
echo "  CoqIde                            : $COQIDE"
echo "  Web browser                       : $BROWSER"
echo ""

echo "  Paths for true installation:"
echo "    binaries      will be copied in $BINDIR"
echo "    library       will be copied in $LIBDIR"
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/config/coq_config.ml file
#####################################################

# 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
ESCBROWSER=`VAR=BROWSER escape_var`

# damned backslashes under M$Windows
case $ARCH in
    win32)
	ESCCOQTOP=`echo $COQTOP |sed -e 's|\\\|\\\\\\\|g'`
	ESCBINDIR=`echo $BINDIR |sed -e 's|\\\|\\\\\\\|g'`
	ESCSRCDIR=`cygpath -d $COQSRC |sed -e 's|\\\|\\\\\\\|g'`
	ESCLIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'`
	ESCCAMLDIR=`echo $CAMLBIN |sed -e 's|\\\|\\\\\\\|g'`
	ESCCAMLLIB=`echo $CAMLLIB |sed -e 's|\\\|\\\\\\\|g'`
  	ESCMANDIR=`echo $MANDIR |sed -e 's|\\\|\\\\\\\|g'`
  	ESCDOCDIR=`echo $DOCDIR |sed -e 's|\\\|\\\\\\\|g'`
   	ESCEMACSLIB=`echo $EMACSLIB |sed -e 's|\\\|\\\\\\\|g'`
   	ESCCOQDOCDIR=`echo $COQDOCDIR |sed -e 's|\\\|\\\\\\\|g'`
   	ESCCAMLP4BIN=`echo $CAMLP4BIN |sed -e 's|\\\|\\\\\\\|g'`
	ESCCAMLP4LIB=`echo $CAMLP4LIB |sed -e 's|\\\|\\\\\\\|g'`
	ESCLABLGTKINCLUDES=`echo $LABLGTKINCLUDES |sed -e 's|\\\|\\\\\\\|g'`
	ESCCOQRUNBYTEFLAGS=`echo $COQRUNBYTEFLAGS |sed -e 's|\\\|\\\\\\\|g'`
	ESCBUILDLDPATH=`echo $BUILDLDPATH |sed -e 's|\\\|\\\\\\\|g'`
;;
    *)
        ESCCOQTOP="$COQTOP"
	ESCBINDIR="$BINDIR"
	ESCSRCDIR="$COQSRC"
	ESCLIBDIR="$LIBDIR"
	ESCCAMLDIR="$CAMLBIN"
	ESCCAMLLIB="$CAMLLIB"
  	ESCMANDIR="$MANDIR"
  	ESCDOCDIR="$DOCDIR"
   	ESCEMACSLIB="$EMACSLIB"
   	ESCCOQDOCDIR="$COQDOCDIR"
   	ESCCAMLP4BIN="$CAMLP4BIN"
   	ESCCAMLP4LIB="$CAMLP4LIB"
	ESCLABLGTKINCLUDES="$LABLGTKINCLUDES"
	ESCCOQRUNBYTEFLAGS="$COQRUNBYTEFLAGS"
	;;
esac

mlconfig_file="$COQSRC/config/coq_config.ml"
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 = "$ESCCOQRUNBYTEFLAGS"
let coqlib = "$ESCLIBDIR"
let coqsrc = "$ESCSRCDIR"
let camlbin = "$ESCCAMLDIR"
let camllib = "$ESCCAMLLIB"
let camlp4 = "$CAMLP4"
let camlp4bin = "$ESCCAMLP4BIN"
let camlp4lib = "$ESCCAMLP4LIB"
let best = "$best_compiler"
let arch = "$ARCH"
let has_natdynlink = $HASNATDYNLINK
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 = "$ESCBROWSER"

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" {} \; \) | grep -v correctness >> "$mlconfig_file")
}

echo "let theories_dirs = [" >> "$mlconfig_file"
subdirs theories
echo "]" >> "$mlconfig_file"

echo "let contrib_dirs = [" >> "$mlconfig_file"
subdirs contrib
echo "]" >> "$mlconfig_file"

chmod a-w "$mlconfig_file"


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

rm -f "$COQSRC/config/Makefile"

sed -e "s|LOCALINSTALLATION|$local|" \
    -e "s|XCOQRUNBYTEFLAGS|$ESCCOQRUNBYTEFLAGS|" \
    -e "s|COQSRCDIRECTORY|$COQSRC|" \
    -e "s|COQVERSION|$VERSION|" \
    -e "s|BINDIRDIRECTORY|$ESCBINDIR|" \
    -e "s|COQLIBDIRECTORY|$ESCLIBDIR|" \
    -e "s|BUILDLDPATH=|$ESCBUILDLDPATH|" \
    -e "s|MANDIRDIRECTORY|$ESCMANDIR|" \
    -e "s|DOCDIRDIRECTORY|$ESCDOCDIR|" \
    -e "s|EMACSLIBDIRECTORY|$ESCEMACSLIB|" \
    -e "s|EMACSCOMMAND|$EMACS|" \
    -e "s|COQDOCDIRECTORY|$ESCCOQDOCDIR|" \
    -e "s|MKTEXLSRCOMMAND|$MKTEXLSR|" \
    -e "s|ARCHITECTURE|$ARCH|" \
    -e "s|OSDEPENDENTLIBS|$OSDEPLIBS|" \
    -e "s|OSDEPENDENTP4OPTFLAGS|$OSDEPP4OPTFLAGS|" \
    -e "s|CAMLLIBDIRECTORY|$ESCCAMLLIB|" \
    -e "s|CAMLTAG|$CAMLTAG|" \
    -e "s|CAMLP4BINDIRECTORY|$ESCCAMLP4BIN|" \
    -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIB|" \
    -e "s|CAMLP4TOOL|$camlp4oexec|" \
    -e "s|CAMLP4COMPATFLAGS|$CAMLP4COMPAT|" \
    -e "s|LABLGTKINCLUDES|$ESCLABLGTKINCLUDES|" \
    -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|FSETSOPT|$fsets|" \
    -e "s|REALSOPT|$reals|" \
    -e "s|COQIDEOPT|$COQIDE|" \
    -e "s|CHECKEDOUTSOURCETREE|$checkedout|" \
    -e "s|WITHDOCOPT|$with_doc|" \
    -e "s|HASNATIVEDYNLINK|$HASNATDYNLINK|" \
      "$COQSRC/config/Makefile.template" > "$COQSRC/config/Makefile"

chmod a-w "$COQSRC/config/Makefile"

##################################################
# 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  

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

# $Id: configure 11858 2009-01-26 13:27:23Z notin $