Commit 2c96eaf4 authored by Heiko Becker's avatar Heiko Becker

Try to fix some CI issues introduced by splitting

parent 135918f1
......@@ -5,13 +5,11 @@ variables:
stages:
- compile
- binary
# - regression
cache:
paths:
- "HOL4/"
- "hol4/cakeml"
compile-coq:
stage: compile
......@@ -25,14 +23,6 @@ compile-hol:
stage: compile
script: ./scripts/ci-hol4.sh
binaries:
stage: binary
script: ./scripts/ci-binary.sh
artifacts:
paths:
- hol4/binary
- coq/binary
# regression-tests:
# stage: regression
# script: ./scripts/regressiontests.sh
\ No newline at end of file
#!/bin/bash
cd ./coq/binary
eval `opam config env`
make
cd ../../
pwd
#Setup HOL4, which should be installed by now
if [ ! -d "./HOL4" ];
then
echo "HOL4 setup failed, exiting"
exit 1
else
cd ./HOL4
export HOLDIR="$(pwd)"
cd ../
fi
cd ./hol4/binary
$HOLDIR/bin/Holmake -q checkerBinaryTheory.uo
$HOLDIR/bin/Holmake -q checker.S
$HOLDIR/bin/Holmake -q cake_checker
......@@ -8,7 +8,7 @@ eval `opam config env`
./configure_coq.sh
make -j
if [[ "$?" != "0"]]
if [[ "$?" != "0" ]];
then
echo "Compilation with Coq 8.7.2 failed"
exit 1
......
......@@ -36,6 +36,7 @@ else
fi
cd $FLOVERDIR
fi
scripts/ci-hol4-setup.sh
cd ./hol4
......@@ -47,3 +48,9 @@ git submodule init cakeml
git submodule update -f cakeml
$HOLDIR/bin/Holmake
cd ./binary
$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