Commit 215ffe0f authored by Heiko Becker's avatar Heiko Becker

Merge branch 'master' into fixed_point_hol4

parents 3637e1bb 9c1261ae
image: localhost:5000/flover
variables:
GIT_SUBMODULE_STRATEGY: normal
GIT_SUBMODULE_STRATEGY: none
stages:
- compile
......@@ -9,8 +9,6 @@ stages:
compile-coq:
stage: compile
except:
- /^WIP:.*$/
script: ./scripts/ci-coq.sh
artifacts:
expire_in: 24h
......@@ -19,8 +17,6 @@ compile-coq:
compile-hol:
stage: compile
except:
- /^WIP:.*$/
script: ./scripts/ci-hol4.sh
artifacts:
expire_in: 24h
......@@ -29,6 +25,4 @@ compile-hol:
regression-tests:
stage: regression
except:
- /^WIP:.*$/
script: ./scripts/regressiontests.sh
\ No newline at end of file
......@@ -30,10 +30,11 @@ if [[ "$INIT" = "yes" ]];
then
echo "Checking out CakeML submodule to correct state"
git submodule init
git submodule --update cakeml
git submodule update -f cakeml
echo "Checking out correct HOL4 version"
cd $HOLDIR
git pull
git checkout $HOLCOMMIT
$HOLDIR/bin/build cleanAll
poly < $HOLDIR/tools/smart-configure.sml
......@@ -46,9 +47,9 @@ else
if [[ "$CURR_HOL" = "$HOLCOMMIT" ]]
then
echo "All set. HOL4 is on the correct commit."
exit 0
else
echo "Please make sure HOL4 uses the commit $HOLCOMMIT"
echo "or consider running the script with the --init parameter."
exit 1
fi
fi
#!/bin/sh
cd ./hol4/binary
$HOLDIR/bin/Holmake checkerBinaryTheory.uo
$HOLDIR/bin/Holmake checker.S
$HOLDIR/bin/Holmake cake_checker
#!/bin/sh
cd ./hol4
$HOLDIR/bin/Holmake
#Run configure script to check the versions
./configure_hol.sh
RET=$?
if [ $RET -eq 1 ];
then
echo "Updating HOL4 to the latest state specified in HOLCOMMIT"
./configure_hol.sh --init
else
echo "Downloading CakeML"
git submodule init cakeml
git submodule update -f cakeml
fi
$HOLDIR/bin/Holmake -q
cd ./binary
$HOLDIR/bin/Holmake checkerBinaryTheory.uo
$HOLDIR/bin/Holmake checker.S
$HOLDIR/bin/Holmake cake_checker
$HOLDIR/bin/Holmake -q checkerBinaryTheory.uo
$HOLDIR/bin/Holmake -q checker.S
$HOLDIR/bin/Holmake -q cake_checker
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