diff --git a/scripts/ci-hol4.sh b/scripts/ci-hol4.sh index b67af1995baa9f37afe4400a5b2fcb39a1f03432..384aadf96637e050e8d2ba4733e37194b19f8023 100755 --- a/scripts/ci-hol4.sh +++ b/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