Commit 56f287cf authored by Heiko Becker's avatar Heiko Becker

Next iteration on HOL4 ci, log some paths to debug

parent 6fcc5341
......@@ -15,13 +15,15 @@ compile-coq:
stage: compile
script: ./scripts/ci-coq.sh
artifacts:
expire_in: 24h
paths:
- coq/
compile-hol:
stage: compile
script: ./scripts/ci-hol4.sh
artifacts:
paths:
- hol4/
# regression-tests:
# stage: regression
......
......@@ -4,6 +4,9 @@
HOLCOMMIT="$(cat ./hol4/.HOLCOMMIT)"
FLOVERDIR="$(pwd)"
#Debugging only:
echo "Set FloverDir to $FLOVERDIR"
#HOL4 always cloned exactly here --> must be in this folder
if [ ! -d "./HOL4" ];
then
......@@ -37,11 +40,17 @@ else
cd $FLOVERDIR
fi
cd ./hol4
#Debugging only:
echo "I am in $(pwd)"
cd ./hol4/binary
#Do a clean build -> remove all temp files
$HOLDIR/bin/Holmake cleanAll -r
cd ..
echo "Downloading CakeML"
git submodule init cakeml
git submodule update -f cakeml
......@@ -50,9 +59,6 @@ $HOLDIR/bin/Holmake
cd ./binary
#TODO Remove me when CI is stable again?
$HOLDIR/bin/Holmake cleanAll -r
$HOLDIR/bin/Holmake checkerBinaryTheory.uo
$HOLDIR/bin/Holmake checker.S
$HOLDIR/bin/Holmake 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