Commit 7e05f873 authored by Heiko Becker's avatar Heiko Becker

Rework CI infrastructure a bit to make the scripts account for caching

Coq CI script fails early when 8.7.2  compilation breaks
HOL4 CI script does not build binaries anymore, this is done by ci-binary.sh
ci-binary.sh can be used to build both Coq and HOl4 binaries in a separate pipeline
parent 9ac65923
#!/bin/bash
cd ./coq/binary
make
cd ../../
cd ./hol4/binary
$HOLDIR/bin/Holmake -q checkerBinaryTheory.uo
$HOLDIR/bin/Holmake -q checker.S
$HOLDIR/bin/Holmake -q cake_checker
......@@ -8,6 +8,12 @@ eval `opam config env`
./configure_coq.sh
make -j
if [[ "$?" != "0"]]
then
echo "Compilation with Coq 8.7.2 failed"
exit 1
fi
make clean
opam switch coq8.8
......
#!/bin/bash
#We must be running on ci-server
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)"
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="$(pwd)"
cd ../
FLOVERDIR="$(pwd)"
if [[ "$HOLDIR" == "" ]];
then
echo "HOLDIR not set, starting to install HOL4 into current directory."
echo "If this is not intended, please abort with Ctrl-c"
sleep 5
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="$(pwd)"
cd ../
else
cd $HOLDIR
git pull
CURRHOL="$(git rev-parse HEAD)"
if [[ "$CURRHOL" != "$HOLCOMMIT" ]];
then
echo "Updating HOL4 to latest version specified in .HOLCOMMIT"
git checkout $HOLCOMMIT
bin/build cleanAll
poly < tools/smart-configure.sml
bin/build
else
echo "HOL4 up-to-date"
fi
cd $FLOVERDIR
fi
cd ./hol4
#Do a clean build -> remove all temp files
$HOLDIR/bin/Holmake cleanAll -r
echo "Downloading CakeML"
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