path: root/configure

#!/bin/sh

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

VERSION=8.0pl3
DATE="Jan 2006"

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

bytecamlc=ocamlc
nativecamlc=ocamlopt
camlp4o=camlp4o
coq_debug_flag=
coq_profile_flag=
best_compiler=opt

local=false
src_spec=no
prefix_spec=no
bindir_spec=no
libdir_spec=no
mandir_spec=no
emacslib_spec=no
#emacs_spec=no
coqdocdir_spec=no
reals_opt=no
reals=all
arch_spec=no
coqide_spec=no

# Parse command-line arguments

while : ; do
  case "$1" in
    "") break;;
    -prefix|--prefix) prefix_spec=yes
                      prefix="$2"
		      shift;;
    -local|--local) local=true
		    reals_opt=yes
		    reals=all;;
    -src|--src) src_spec=yes
                COQTOP="$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;;
    -emacslib|--emacslib) emacslib_spec=yes
                          emacslib="$2"
			  shift;;
#    -emacs |--emacs) emacs_spec=yes
#		     emacs="$2"
#		     shift;;
    -coqdocdir|--coqdocdir) coqdocdir_spec=yes
	              coqdocdir="$2"
		      shift;;
    -arch|--arch) arch_spec=yes
                  arch=$2
		  shift;;
    -opt|--opt) bytecamlc=ocamlc.opt
                camlp4o=camlp4o  # can't add .opt since dyn load'll be required
                nativecamlc=ocamlopt.opt;;
    -reals|--reals) reals_opt=yes
		    reals=$2
		    shift;;
    -coqide|--coqide) coqide_spec=yes
		      COQIDE=$2
		      shift;;
    -byte-only|-byteonly|--byteonly|--byte-only) best_compiler=byte;;
    -debug|--debug) coq_debug_flag=-g;;
    -profile|--profile) coq_profile_flag=-p;;
     *) echo "Unknown option \"$1\"." 1>&2; 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) 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 && (/bin/uname -s | grep -q -i CYGWIN) ; then
	    ARCH=win32
	    # cygwin returns a name of the form /cygdrive/c/... 
	    # that coqc does not understand; need to transform it
	    COQTOP=`echo $COQTOP | sed -e "s#.*cygdrive.\(.\)#\1:#"`
	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;;
    yes) ARCH=$arch
esac

# executable extension

case $ARCH in
    win32) EXE=".exe";;
    *) EXE=""
esac

# strip command

case $ARCH in
    win32)
	# true -> strip : it exists under cygwin !
	STRIPCOMMAND="strip";; 
    *)
    if [ "$coq_profile_flag" = "-p" ] ; then
	STRIPCOMMAND="true"
    else
	STRIPCOMMAND="strip"
    fi
esac

#########################################
# Objective Caml programs

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
	bytecamlc="$CAMLC"
	nativecamlc=`dirname "$CAMLC"`/$nativecamlc;;
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

CAMLBIN=`dirname "$CAMLC"`
CAMLVERSION=`"$CAMLC" -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `

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

# do we have a native compiler: test of ocamlopt and its version

if [ "$best_compiler" = "opt" ] ; then
  CAMLOPT=`which $nativecamlc`
  case "$CAMLOPT" in
    "") best_compiler=byte
        echo "You have only bytecode compilation.";;
    *) CAMLOPTVERSION=`"$CAMLOPT" -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `
       if [ "$CAMLOPTVERSION" != "$CAMLVERSION" ] ; then \
         echo "native and bytecode compilers do not have the same version!"; fi
       echo "You have native-code compilation. Good!"
  esac
fi

# For coqmktop

CAMLLIB=`"$CAMLC" -where`

# Camlp4 (greatly simplified since merged with ocaml)

CAMLP4BIN=${CAMLBIN}
CAMLP4LIB=+camlp4

# 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";;
  *) OSDEPLIBS="-cclib -lunix"
esac

# lablgtk2 and CoqIDE

if [ "$coqide_spec" = "no" ] ; then
if test -x "${CAMLLIB}/lablgtk2" ; then
    if grep -q -w convert_with_fallback "${CAMLLIB}/lablgtk2/glib.mli" ; then
	if test -f "${CAMLLIB}/threads/threads.cmxa" ; then
            echo "LablGtk2 found, native threads: native CoqIde will be available"
	    COQIDE=opt;
        else
            echo "LablGtk2 found, no native threads: bytecode CoqIde will be available"
	    COQIDE=byte
	fi
    else
        echo "LablGtk2 found but too old: CoqIde will not be available"
        COQIDE=no;
    fi
else
    echo "LablGtk2 not found: CoqIde will not be available"
    COQIDE=no
fi
fi

if [ $COQIDE != no ] ; then
  if grep "class view " "${CAMLLIB}/lablgtk2/gText.mli" | grep -q "\[>" ; then
    LABLGTKGE26=yes;
  else
    LABLGTKGE26=no
  fi
fi

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

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

######################################
# mktexlsr

#MKTEXLSR=`which mktexlsr`
#case $MKTEXLSR in
#    "") MKTEXLSR=true;;
#esac

###########################################
# bindir, libdir, mandir, etc.

canonical_pwd () {
ocaml 2>&1 1>/dev/null <<EOF
  prerr_endline(Sys.getcwd());;
EOF
}

case $src_spec in
  no) COQTOP=`canonical_pwd`
esac

case $ARCH in
  win32)
	 bindir_def='C:\coq\bin'
	 libdir_def='C:\coq\lib'
	 mandir_def='C:\coq\man'
	 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
	 emacslib_def=/usr/share/emacs/site-lisp
         coqdocdir_def=/usr/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 ;;
    *) echo "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 ;;
    *)  echo "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 ;;
    *)  echo "Where should I install the Coq man pages [$mandir_def] ?"
        read MANDIR
	case $MANDIR in
	    "") MANDIR=$mandir_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 ;;
    *) echo "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 ;;
    *) echo "Where should I install Coqdoc TeX/LaTeX files [$coqdocdir_def] ?"
        read COQDOCDIR
	case $COQDOCDIR in
	    "") COQDOCDIR=$coqdocdir_def;;
	    *) true;;
	esac;;
esac

case $reals_opt in
    no) echo "Should I compile the complete theory of real analysis [Y/N, default is Y] ?"
	read reals_ans

	case $reals_ans in
	    "N"|"n"|"No"|"NO"|"no")
		    reals=basic;;
		*) reals=all;;
	esac;;
    yes) true;;
esac

# case $emacs_spec in
#     no) echo "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 "  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 "$reals" = "all"; then
echo "  Reals theory                      : All"
else
echo "  Reals theory                      : Basic"
fi
echo "  CoqIde                            : $COQIDE"
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 "    emacs mode will be copied in $EMACSLIB"
echo ""

#####################################################
# Building the $COQTOP/config/coq_config.ml file
#####################################################

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

export COQTOP BINDIR LIBDIR CAMLLIB
ESCCOQTOP="`VAR=COQTOP escape_var`"
ESCBINDIR="`VAR=BINDIR escape_var`"
ESCLIBDIR="`VAR=LIBDIR escape_var`"
ESCCAMLLIB="`VAR=CAMLLIB escape_var`"
ESCCAMLP4LIB="$ESCCAMLLIB"/camlp4

mlconfig_file=$COQTOP/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 bindir = "$ESCBINDIR" 
let coqlib = "$ESCLIBDIR"
let coqtop = "$ESCCOQTOP"
let camllib = "$ESCCAMLLIB"
let camlp4lib = "$ESCCAMLP4LIB"
let best = "$best_compiler"
let arch = "$ARCH"
let osdeplibs = "$OSDEPLIBS"
let version = "$VERSION"
let date = "$DATE"
let compile_date = "$COMPILEDATE"
let exec_extension = "$EXE"

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 * -type d ! -name CVS -exec $PRINTF "\"%s\";\n" {} \; | grep -v extraction/test | 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 $COQTOP/config/Makefile

# damned backslashes under M$Windows
case $ARCH in
    win32)
	ESCCOQTOP=`echo $COQTOP |sed -e 's|\\\|\\\\\\\|g'`
	ESCBINDIR=`echo $BINDIR |sed -e 's|\\\|\\\\\\\|g'`
	ESCLIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'`
  	ESCMANDIR=`echo $MANDIR |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'`
	;;
    *)
        ESCCOQTOP="$COQTOP"
	ESCBINDIR="$BINDIR"
	ESCLIBDIR="$LIBDIR"
  	ESCMANDIR="$MANDIR"
   	ESCEMACSLIB="$EMACSLIB"
   	ESCCOQDOCDIR="$COQDOCDIR"
   	ESCCAMLP4BIN="$CAMLP4BIN" ;;
esac

sed -e "s|LOCALINSTALLATION|$local|" \
    -e "s|COQTOPDIRECTORY|$ESCCOQTOP|" \
    -e "s|COQVERSION|$VERSION|" \
    -e "s|BINDIRDIRECTORY|$ESCBINDIR|" \
    -e "s|COQLIBDIRECTORY|$ESCLIBDIR|" \
    -e "s|MANDIRDIRECTORY|$ESCMANDIR|" \
    -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|CAMLTAG|$CAMLTAG|" \
    -e "s|CAMLP4BINDIRECTORY|$ESCCAMLP4BIN|" \
    -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIB|" \
    -e "s|CAMLP4TOOL|$camlp4o|" \
    -e "s|CAMLP4COMPATFLAGS|$CAMLP4COMPAT|" \
    -e "s|COQDEBUGFLAG|$coq_debug_flag|" \
    -e "s|COQPROFILEFLAG|$coq_profile_flag|" \
    -e "s|BESTCOMPILER|$best_compiler|" \
    -e "s|EXECUTEEXTENSION|$EXE|" \
    -e "s|BYTECAMLC|$bytecamlc|" \
    -e "s|NATIVECAMLC|$nativecamlc|" \
    -e "s|STRIPCOMMAND|$STRIPCOMMAND|" \
    -e "s|REALSOPT|$reals|" \
    -e "s|COQIDEOPT|$COQIDE|" \
      $COQTOP/config/Makefile.template > $COQTOP/config/Makefile

chmod a-w $COQTOP/config/Makefile

##################################################
# Building the $COQTOP/dev/ocamldebug-v7 file
####################################################

if test "$coq_debug_flag" = "-g" ; then
  rm -f $COQTOP/dev/ocamldebug-v7
  sed -e "s|COQTOPDIRECTORY|$COQTOP|" \
      -e "s|COQLIBDIRECTORY|$LIBDIR|" \
      -e "s|CAMLBINDIRECTORY|$CAMLBIN|" \
      -e "s|CAMLP4LIBDIRECTORY|$CAMLLIB/camlp4|" \
      $COQTOP/dev/ocamldebug-v7.template > $COQTOP/dev/ocamldebug-v7
  chmod a-w,a+x $COQTOP/dev/ocamldebug-v7
fi

##################################################
# Fixing lablgtk types
####################################################

if [ "$LABLGTKGE26" = "yes" ] ; then
  cp -f ide/undo_lablgtk_ge26.mli ide/undo.mli;
else
  cp -f ide/undo_lablgtk_lt26.mli ide/undo.mli
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,v 1.74.2.19 2006/01/13 11:50:07 barras Exp $