Commit 8cf59d34 authored by Heiko Becker's avatar Heiko Becker

Next step for reworked ci, now the Dockerimage must be rebuild

parent ddafa605
......@@ -5,7 +5,7 @@ variables:
stages:
- compile
- regression
! - regression
compile-coq:
stage: compile
......@@ -23,6 +23,6 @@ compile-hol:
paths:
- hol4/binary/
regression-tests:
stage: regression
script: ./scripts/regressiontests.sh
\ No newline at end of file
! regression-tests:
! stage: regression
! script: ./scripts/regressiontests.sh
\ No newline at end of file
......@@ -3,21 +3,19 @@
if [[ "$HOLDIR" = "" ]]
then
#We must be running on ci-server
echo "HOLDIR not set, starting to install HOL4 into ~/ for current user."
echo "HOLDIR not set, starting to install HOL4 into current directory."
echo "If this is not intended, please abort with Ctrl-c"
sleep 5
#Set HOL4 commit variable
HOLCOMMIT="$(cat ./hol4/.HOLCOMMIT)"
pushd ./
cd ~/
git clone https://github.com/HOL-Theorem-Prover/HOL.git HOL4
cd HOL4
git checkout $HOLCOMMIT
poly < tools/smart-configure.sml
bin/build
export HOLDIR=~/HOL4/
popd
export HOLDIR="$(pwd)"
cd ../
fi
cd ./hol4
......
......@@ -18,6 +18,8 @@ for fname in ./*.v; do
done
#HOL4 regression tests
HOLDIR=../../HOL4
for fname in ./*.sml; do
FILEPRE=${fname/Script.sml/}
FILENAME=$FILEPRE
......
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