configure

#!/bin/sh

if test $# -ne 1
then
  echo "usage: `basename $0` <compcert_dir>"
  exit 1
fi

# create link to compcert directory

if test ! -d $1
then
  echo "warning: $1 does not exist or is not a directory!"
  exit 1
fi

echo create link to $1
echo ln -f -n -s $1 compcert
ln -f -n -s $1 compcert

# create coqrc

echo create coqrc
sed -e "s|/path/to/simsoc-cert|`pwd`|" coqrc.in > coqrc

# check prog

check_prog() {
    echo -n "$prog: "
    which $prog
    if test $? -ne 0
    then
	echo 'cannot find $prog in path!'
	exit 1
    fi
}

# check version

check_version() {
    if test "$ver" != "$ref"
    then
	echo "warning: you use $prog $ver instead of $prog $ref!"
	exit 1
    fi
}

# check coq

prog=coqc
check_prog

ref=8.3pl2
ver=`coqc -v | head -1 | awk '{print$6}'`
check_version

# check ocaml

prog=ocamlopt
check_prog

ref=3.12.1
ver=`ocamlopt -version`
check_version

# check compcert

f=compcert/driver/Configuration.ml
if test ! -f $f
then
    echo "cannot find $f: configure compcert first!"
    exit 1
fi

prog=ccomp
check_prog