Disable coq regression tests

scripts/regressiontests.sh

 #!/bin/bash
 
-HOLCOMMIT="$(cat ./hol4/.HOLCOMMIT)"
+#HOLCOMMIT="$(cat ./hol4/.HOLCOMMIT)"
 FLOVERDIR="$(pwd)"
 
 #HOL4 regression tests
-if [ ! -d "./HOL4" ];
-then
-    echo "HOL4 not installed, starting to install HOL4 into current directory."
-    echo "If this is not intended, please abort with Ctrl-c"
-    sleep 5
-
-    git clone https://github.com/HOL-Theorem-Prover/HOL.git HOL4
-    cd HOL4
-    git checkout $HOLCOMMIT
-    poly < tools/smart-configure.sml
-    bin/build
-    export HOLDIR="$(pwd)"
-    cd ../
-else
-    cd ./HOL4
-    export HOLDIR="$(pwd)"
-    git pull
-    CURRHOL="$(git rev-parse HEAD)"
-    if [[ "$CURRHOL" != "$HOLCOMMIT" ]];
-    then
-        echo "Updating HOL4 to latest version specified in .HOLCOMMIT"
-        git checkout $HOLCOMMIT
-        bin/build cleanAll
-        poly < tools/smart-configure.sml
-        bin/build
-    else
-        echo "HOL4 up-to-date"
-    fi
-    cd $FLOVERDIR
-fi
-
-eval `opam config env`
+#if [ ! -d "./HOL4" ];
+#then
+#    echo "HOL4 not installed, starting to install HOL4 into current directory."
+#    echo "If this is not intended, please abort with Ctrl-c"
+#    sleep 5
+#
+#    git clone https://github.com/HOL-Theorem-Prover/HOL.git HOL4
+#    cd HOL4
+#    git checkout $HOLCOMMIT
+#    poly < tools/smart-configure.sml
+#    bin/build
+#    export HOLDIR="$(pwd)"
+#    cd ../
+#else
+#    cd ./HOL4
+#    export HOLDIR="$(pwd)"
+#    git pull
+#    CURRHOL="$(git rev-parse HEAD)"
+#    if [[ "$CURRHOL" != "$HOLCOMMIT" ]];
+#    then
+#        echo "Updating HOL4 to latest version specified in .HOLCOMMIT"
+#        git checkout $HOLCOMMIT
+#        bin/build cleanAll
+#        poly < tools/smart-configure.sml
+#        bin/build
+#    else
+#        echo "HOL4 up-to-date"
+#    fi
+#    cd $FLOVERDIR
+#fi
+#
+#eval `opam config env`
 
 cd ./testcases/regression
 
-#Coq regression tests
-for fname in ./*.v; do
-    coqc -R ../../coq Flover $fname
-    if [ $? -eq 0 ]
-    then
-       echo "Successfully checked $fname"
-    else
-       echo "Checking $fname failed"
-       exit 1;
-    fi
-
-done
+#Coq regression tests - disabled
+#for fname in ./*.v; do
+#    coqc -R ../../coq Flover $fname
+#    if [ $? -eq 0 ]
+#    then
+#       echo "Successfully checked $fname"
+#    else
+#       echo "Checking $fname failed"
+#       exit 1;
+#    fi
+#
+#done
 
 #HOL4 regression tests
 $HOLDIR/bin/Holmake heap