The Coq mailing list

[Judica�l Courant <Judicael.Courant AT lri.fr>]

Dear Ian, 

We apologize for the bad experienced you had trying to install Coq. 
We are still investigating the problem with coq-bugs (it used to work).
As for the configure script, -e is indeed a non-standard feature of echo
in bash. I have just corrected the problem. In order to make your
installation work, you can either run a "bash configure" or apply 
the enclosed configure file (I ran it on my Debian woody with ash and
the build went right). Let us know if you have any other problem. 

Sincerly yours, 

Judicaël Courant. 
-- 
Judicael.Courant AT lri.fr,
 http://www.lri.fr/~jcourant/
(+33) (0)1 69 15 64 85
"Heureux ceux qui savent rire d'eux-mêmes :
 ils n'ont pas fini de s'amuser !"
#!/bin/sh

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

VERSION=7.2
VERSIONSI=1.0
DATE="January 2002"

# 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
bindir_spec=no
libdir_spec=no
mandir_spec=no
emacslib_spec=no
emacs_spec=no
arch_spec=no

COQTOP=`pwd`


# Parse command-line arguments

while : ; do
  case "$1" in
    "") break;;
    -prefix|--prefix) bindir_spec=yes
                      bindir=$2/bin
                      libdir_spec=yes
		      libdir=$2/lib/coq
                      mandir_spec=yes
		      mandir=$2/man
		      shift;;
    -local|--local) local=true
                    bindir_spec=yes
                    bindir=$COQTOP/bin
                    libdir_spec=yes
		    libdir=$COQTOP
                    mandir_spec=yes
		    mandir=$COQTOP/man
                    emacslib_spec=yes
		    emacslib=$COQTOP/tools/emacs;;
    -src|--src) 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;;
    -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;;
    -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


# 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 -f /bin/arch ; then
	    ARCH=`/bin/arch`
	elif test -f /usr/bin/arch ; then
	    ARCH=`/usr/bin/arch`
	elif test -f /usr/ucb/arch ; then
	    ARCH=`/usr/ucb/arch`
	elif /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:#"`
	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

# bindir, libdir, mandir, etc.

case $ARCH in
  win32)
	 bindir_def=\\coq\\bin
	 libdir_def=\\coq\\lib
	 mandir_def=\\coq\\man
	 emacslib_def=\\coq\\emacs;;
  *)
	 bindir_def=/usr/local/bin
	 libdir_def=/usr/local/lib/coq
	 mandir_def=/usr/local/man
	 emacslib_def=/usr/share/emacs/site-lisp;;
esac

emacs_def=emacs

case $bindir_spec in
    no) echo "Where should I install the Coq binaries [$bindir_def] ?"
        read BINDIR
	
	case $BINDIR in
	    "") BINDIR=$bindir_def;;
	    *) true;;
	esac;;
    yes) BINDIR=$bindir;;
esac

case $libdir_spec in
    no) echo "Where should I install the Coq library [$libdir_def] ?"
        read LIBDIR
	
	case $LIBDIR in
	    "") LIBDIR=$libdir_def;;
	    *) true;;
	esac;;
    yes) LIBDIR=$libdir;;
esac

case $mandir_spec in
    no) echo "Where should I install the Coq man pages [$mandir_def] ?"
        read MANDIR
	
	case $MANDIR in
	    "") MANDIR=$mandir_def;;
	    *) true;;
	esac;;
    yes) MANDIR=$mandir;;
esac

case $emacslib_spec in
    no) echo "Where should I install the Coq Emacs mode [$emacslib_def] ?"
        read EMACSLIB
	
	case $EMACSLIB in
	    "") EMACSLIB=$emacslib_def;;
	    *) true;;
	esac;;
    yes) EMACSLIB=$emacslib;;
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

# 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

# OS dependent camlp4 options for native compilation

# executable extension

case $ARCH in
    win32) EXE=".exe";;
    *) EXE=""
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 ocamlc executable [/usr/local/bin by default]: "
	read CAMLC
	
	case "$CAMLC" in
		"") CAMLC=/usr/local/bin/ocamlc;;
		*/ocamlc|*/ocamlc.opt) true;;
		*/) CAMLC="${CAMLC}"ocamlc;;
		*) CAMLC="${CAMLC}"/ocamlc;;
	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)
	echo "Your version of Objective-Caml is $CAMLVERSION."
	echo "You need Objective-Caml 3.01 or later !"
	echo "Configuration script failed!"
	exit 1;;
  ?*)	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

# 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" -v | sed -n -e 's|.*directory:* *\(.*\)$|\1|p' `

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

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

# Camlp4

CAMLP4=`which $camlp4o`
case "$CAMLP4" in
	"") echo "camlp4 is not present in your path!"
	echo "Give me manually the path to the camlp4 executable [/usr/local/bin by default]: "
	read CAMLP4
	
	case "$CAMLP4" in
		"") CAMLP4=/usr/local/bin/camlp4o;;
		*/camlp4) CAMLP4=${CAMLP4}o;;
		*/camlp4o) true;;
		*/) CAMLP4="${CAMLP4}"camlp4o;;
		*) CAMLP4="${CAMLP4}"/camlp4o;;
	esac
	camlp4o="$CAMLP4";;
esac

if test ! -f "$CAMLP4" ; then
	echo "I can not find the executable '$CAMLP4'! (Have you installed it?)"
	echo "Configuration script failed!"
	exit 1
fi

CAMLP4BIN=`dirname "$CAMLP4"`
CAMLP4VERSION=`"$CAMLP4" -v 2>&1 | sed -n -e 's|.*version *\(.*\)$|\1|p'`
case $CAMLP4VERSION in
  0.*|1.*|2.00|3.00*)
        echo "Your version of Camlp4 is $CAMLP4VERSION."
	echo "You need Camlp4 3.01 or later !"
	echo "Configuration script failed!"
	exit 1;;
  ?*)	echo "You have Camlp4 $CAMLP4VERSION. Good!";;
  *) echo "I found Camlp4 but cannot find its version number!"
     echo "Is it installed properly ?"
     echo "Configuration script failed!"
     exit 1;;
esac
case $CAMLP4VERSION,$CAMLOSTYPE in
  3.04,*)
    CAMLP4LIB=+camlp4;;
  *,Win32)
    CAMLP4LIB=`"$CAMLP4" -where |sed -e 's|\\\|/|g'`;;
  *,*)
    CAMLP4LIB=`"$CAMLP4" -where`;;
esac

case $ARCH in
    win32)
	STRIPCOMMAND="true";;
    *)
    if [ "$coq_profile_flag" = "-p" ] ; then
	STRIPCOMMAND="true"
    else
	STRIPCOMMAND="strip"
    fi
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 version         : $CAMLVERSION"
echo "  Objective-Caml binaries in     : $CAMLBIN"
echo "  Objective-Caml library in      : $CAMLLIB"
echo "  Camlp4 version                 : $CAMLP4VERSION"
echo "  Camlp4 binaries in             : $CAMLP4BIN"
echo "  Camlp4 library in              : $CAMLP4LIB"
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/Makefile file

rm -f $COQTOP/config/Makefile

case $ARCH in
    win32)
	BINDIR=`echo $BINDIR |sed -e 's|\\\|/|g'`
	LIBDIR=`echo $LIBDIR |sed -e 's|\\\|/|g'`
	MANDIR=`echo $MANDIR |sed -e 's|\\\|/|g'`;;
esac

#case $CAMLOSTYPE in
#    Win32)
#	CAMLP4BIN=`echo $CAMLP4BIN |sed -e 's|\\\|/|g'`
#	CAMLP4LIB=`echo "$CAMLP4LIB" | sed -e 's|\\\|\\\\\\\\|g'`
#	CAMLP4BIN=`echo $CAMLC |sed -e 's|\\\|/|g'`
#	CAMLP4BIN=`echo $CAMLLIB |sed -e 's|\\\|/|g'`
#        ;;
#esac


sed -e "s|LOCALINSTALLATION|$local|" \
    -e "s|COQTOPDIRECTORY|$COQTOP|" \
    -e "s|COQVERSION|$VERSION|" \
    -e "s|BINDIRDIRECTORY|$BINDIR|" \
    -e "s|COQLIBDIRECTORY|$LIBDIR|" \
    -e "s|MANDIRDIRECTORY|$MANDIR|" \
    -e "s|EMACSLIBDIRECTORY|$EMACSLIB|" \
    -e "s|EMACSCOMMAND|$EMACS|" \
    -e "s|ARCHITECTURE|$ARCH|" \
    -e "s|OSDEPENDENTLIBS|$OSDEPLIBS|" \
    -e "s|OSDEPENDENTP4OPTFLAGS|$OSDEPP4OPTFLAGS|" \
    -e "s|CAMLLIBDIRECTORY|$CAMLLIB|" \
    -e "s|CAMLP4BINDIRECTORY|$CAMLP4BIN|" \
    -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIB|" \
    -e "s|CAMLP4TOOL|$camlp4o|" \
    -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|" \
      $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|$CAMLP4LIB|" \
      $COQTOP/dev/ocamldebug-v7.template > $COQTOP/dev/ocamldebug-v7
  chmod a-w,a+x $COQTOP/dev/ocamldebug-v7
fi

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

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 = "$BINDIR" 
let coqlib = "$LIBDIR"
let coqtop = "$COQTOP"
let camllib = "$CAMLLIB"
let camlp4lib = "$CAMLP4LIB"
let best = "$best_compiler"
let arch = "$ARCH"
let osdeplibs = "$OSDEPLIBS"
let version = "$VERSION"
let versionsi = "$VERSIONSI"
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 ! -name . -exec $PRINTF "\"%s\";\n" {} \; >> $mlconfig_file)
}

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

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

if test "$CAMLOSTYPE" = "Win32" ; then
# We change: / -> \\ and \ -> \\ (dos paths)
# This is a bit tricky
sed -e "s|\\\\\\\\\\\\\\\|\\\|" -e "s|/|\\\|g"  -e "s|\\\|\\\\\\\|g" $mlconfig_file > $mlconfig_file.win
mv $mlconfig_file.win $mlconfig_file
fi
chmod a-w $mlconfig_file

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.40 2002/01/10 18:36:07 herbelin Exp $