Merge branch 'master' of gitlab.mpi-sws.org:AVA/FloVer

scripts/ci-hol4.sh

@@ -40,12 +40,12 @@ cd ./hol4
 
 $HOLDIR/bin/Holmake
 
-cd ./binary
+#cd ./binary
 
-echo "Downloading CakeML"
-git submodule init cakeml
-git submodule update -f cakeml
+#echo "Downloading CakeML"
+#git submodule init cakeml
+#git submodule update -f cakeml
 
-$HOLDIR/bin/Holmake checkerBinaryTheory.uo
-$HOLDIR/bin/Holmake checker.S
-$HOLDIR/bin/Holmake cake_checker
+#$HOLDIR/bin/Holmake checkerBinaryTheory.uo
+#$HOLDIR/bin/Holmake checker.S
+#$HOLDIR/bin/Holmake cake_checker

scripts/regressiontests.sh

@@ -68,15 +68,14 @@ for fname in ./*.sml; do
     fi
 done
 
-#Binary regression tests
-for fname in ./*.txt; do
-    ../../hol4/binary/cake_checker $fname
-    if [ $? -eq 0 ]
-    then
-        echo "Successfully checked $fname";
-    else
-        echo "Checking $fname has failed"
-        exit 1;
-    fi
-
-done
+#Binary regression tests; disabled
+#for fname in ./*.txt; do
+#    ../../hol4/binary/cake_checker $fname
+#    if [ $? -eq 0 ]
+#    then
+#        echo "Successfully checked $fname";
+#    else
+#        echo "Checking $fname has failed"
+#        exit 1;
+#    fi
+#done