configure

#!/usr/bin/env bash

CALLNAME="$0"
OPTFILE="_CoqProject"

function usage {
    >&2 echo "usage: $CALLNAME [options]"
    >&2 echo
    >&2 echo "options are:"

    >&2 printf '\t--hoqdir <dir>\tdirectory containing hoqc, hoqtop and hoqdep'
    >&2 printf '\t\t\t(can be passed through environment variable HOQDIR)'

    >&2 printf '\t--coqbin <dir>\tdirectory containing coq_makefile'
    >&2 printf '\t\t\t(can be passed through environment variable COQBIN)'

    >&2 printf '\t--no-emacs\tdo not generate .dir-locals.el'

    >&2 printf '\t-h\t\tdisplay this list of options and quit'
    >&2 printf '\t-help\t\tdisplay this list of options and quit'
    >&2 printf '\t--help\t\tdisplay this list of options and quit'
}

DO_EMACS=true

while [[ "$#" -gt 0 ]]
do
    case "$1" in
        "--hoqdir")
            if [[ "$#" = 1 ]]
            then
                >&2 echo "$CALLNAME: option '--hoqdir' needs one argument"
                usage
                exit 1
            fi
            HOQDIR="$2"
            shift;;
        "--coqbin")
            if [[ "$#" = 1 ]]
            then
                >&2 echo "$CALLNAME: option '--coqbin' needs one argument"
                usage
                exit 1
            fi
            COQBIN="$2"
            shift;;
        "--no-emacs")
            DO_EMACS=false;;
        "-h"|"-help"|"--help")
            usage
            exit 0;;
        *)
            >&2 echo "$CALLNAME: unknown argument $1"
            usage
            exit 1;;
    esac
    shift
done

if [ -z "${HOQDIR}" ]
then
    OK=true
    HOQC=$(command -v hoqc) || OK=false
    HOQTOP=$(command -v hoqtop) || OK=false
    HOQDEP=$(command -v hoqdep) || OK=false
    if $OK
    then
        :
    else
        >&2 echo "$CALLNAME: hoqc, hoqtop or hoqdep not in PATH, use option --hoqdir"
        usage
        exit 1
    fi
else
    #readlink -nm: canonicalize (strip double slash and . .. and
    #symlinks) without checking existence
    HOQC=$(readlink -nm "$HOQDIR/hoqc")
    HOQTOP=$(readlink -nm "$HOQDIR/hoqtop")
    HOQDEP=$(readlink -nm "$HOQDIR/hoqdep")

fi

if [ -z "${COQBIN}" ]
then
    OK=true
    COQMAKEFILE=$(command -v coq_makefile) || OK=false
    if $OK
     then
         :
     else
         >&2 echo "$CALLNAME: coq_makefile not in PATH, use option --coqbin"
         usage
         exit 1
     fi
else
    COQMAKEFILE=$(readlink -nm "$COQBIN/coq_makefile")
    if [ -x "$COQMAKEFILE" ] && [ -f "$COQMAKEFILE" ]
    then
        :
    else
        >&2 echo "$CALLNAME: $COQMAKEFILE is not executable"
        usage
        exit 1
    fi
fi

echo "Summary:"
echo "Generate .dir-locals.el: $DO_EMACS"
echo "HOQC=$HOQC"
echo "HOQTOP=$HOQTOP"
echo "HOQDEP=$HOQDEP"
echo "COQMAKEFILE=$COQMAKEFILE"

########### Work

cp "$OPTFILE.in" "$OPTFILE"

echo "COQC = $HOQC" >> "$OPTFILE"
echo "COQDEP = $HOQDEP" >> "$OPTFILE"

#non IR find
#HoTTBook and CPP depend on IR
find ./theories -name '*.v' -print >> "$OPTFILE"

"$COQMAKEFILE" -f "$OPTFILE" -o Makefile || exit 1

if $DO_EMACS
then echo "((coq-mode . ((coq-prog-name . \"$HOQTOP\"))))" > .dir-locals.el
fi

echo "$0 success!"