hoq-config.in

#!/bin/bash
# This is the configuration for wrapers around coq which tricks Coq
# into using the HoTT standard library and enables the HoTT-specific
# options.  One day we might figure out how to create an honest Coq
# toplevel instead.
prefix="@prefix@"
export COQC="@COQC@"
export COQDEP="@COQDEP@"
export COQDOC="@COQDOC@"
export COQIDE="@COQIDE@"
export COQTOP="@COQTOP@"

function readlink_f() {
    # readlink -f doesn't work on Mac OS.  So we roll our own readlink
    # -f, from
    # http://stackoverflow.com/questions/1055671/how-can-i-get-the-behavior-of-gnus-readlink-f-on-a-mac
    TARGET_FILE="$1"

    cd "$(dirname "$TARGET_FILE")"
    TARGET_FILE=`basename "$TARGET_FILE"`

    # Iterate down a (possible) chain of symlinks
    while [ -L "$TARGET_FILE" ]
    do
	TARGET_FILE=`readlink "$TARGET_FILE"`
	cd "$(dirname "$TARGET_FILE")"
	TARGET_FILE=`basename "$TARGET_FILE"`
    done

    # Compute the canonicalized name by finding the physical path
    # for the directory we're in and appending the target file.
    PHYS_DIR=`pwd -P`
    RESULT="$PHYS_DIR/$TARGET_FILE"
    echo "$RESULT"
}

# If there is a coq/theories directory in the parent directory of this
# script, then use that one, otherwise use the global one. This trick
# allows hoqc to work "in place" on the source files.
mydir="$(dirname "$(readlink_f "${BASH_SOURCE[0]}")")"
which cygpath 2>/dev/null >/dev/null && mydir="$(cygpath -m "$mydir")"
if test -d "$mydir/coq/theories"
then
  export COQLIB="$mydir/coq"
  export HOTTLIB="$mydir/theories"
else
  export COQLIB="@hottdir@/coq"
  export HOTTLIB="@hottdir@/theories"
fi
#export COQ_ARGS=(-no-native-compiler -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -indices-matter)