configure_hol.sh 1.23 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25
#!/bin/bash
function display_help {
    echo "configure_hol.sh - Check for environment variables and HOL4"
    echo "                   commit hash to be correct"
    echo ""
    echo -e "--help\t Show this text"
    echo -e " --init\t Initialize CakeML submodule to latest state"
}

INIT=no
while [ $# != 0 ]; do
   case "$1" in
   --help)  display_help;;
   --init) INIT=yes;;
   *)
   esac
   shift
 done

if [[ "$HOLDIR" = "" ]];
then
    echo "ERROR: HOLDIR variable not set. Please configure the HOLDIR variable first"
    exit 1
fi

26
DIR="$(pwd)"
27 28 29 30 31 32
HOLCOMMIT="$(cat ./.HOLCOMMIT)"

if [[ "$INIT" = "yes" ]];
then
    echo "Checking out CakeML submodule to correct state"
    git submodule init
Heiko Becker's avatar
Heiko Becker committed
33
    git submodule update -f cakeml
34 35 36

    echo "Checking out correct HOL4 version"
    cd $HOLDIR
Heiko Becker's avatar
Heiko Becker committed
37
    git pull
38
    git checkout $HOLCOMMIT
39
    bin/build cleanAll
40
    poly < $HOLDIR/tools/smart-configure.sml
41
    bin/build 
42 43 44 45 46 47 48 49 50 51 52
    cd $DIR
else
    cd $HOLDIR
    CURR_HOL="$(git rev-parse HEAD)"

    if [[ "$CURR_HOL" = "$HOLCOMMIT" ]]
    then
        echo "All set. HOL4 is on the correct commit."
    else
        echo "Please make sure HOL4 uses the commit $HOLCOMMIT"
        echo "or consider running the script with the --init parameter."
53
        exit 1
54 55
    fi
fi