Commit 9ec7e793 authored by Heiko Becker's avatar Heiko Becker

Fix bugs in scripts preventing proper HOL4 checking

parent c85e922e
......@@ -6,6 +6,17 @@ make
cd ../../
#Setup HOL4, which should be installed by now
if [ ! -d "./HOL4"];
then
echo "HOL4 setup failed, exiting"
exit 1
else
cd ./HOL4
export HOLDIR="$(pwd)"
cd ../
fi
cd ./hol4/binary
$HOLDIR/bin/Holmake -q checkerBinaryTheory.uo
......
......@@ -4,9 +4,10 @@
HOLCOMMIT="$(cat ./hol4/.HOLCOMMIT)"
FLOVERDIR="$(pwd)"
if [[ "$HOLDIR" == "" ]];
#HOL4 always cloned exactly here --> must be in this folder
if [ ! -d "./HOL4" ];
then
echo "HOLDIR not set, starting to install HOL4 into current directory."
echo "HOL4 not installed, starting to install HOL4 into current directory."
echo "If this is not intended, please abort with Ctrl-c"
sleep 5
......@@ -18,6 +19,8 @@ then
export HOLDIR="$(pwd)"
cd ../
else
cd ./HOL4
export HOLDIR="$(pwd)"
cd $HOLDIR
git pull
CURRHOL="$(git rev-parse HEAD)"
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment