ci-hol4.sh 943 Bytes
Newer Older
Heiko Becker's avatar
Heiko Becker committed
1
#!/bin/bash
Heiko Becker's avatar
Heiko Becker committed
2

Heiko Becker's avatar
Heiko Becker committed
3
if [[ "$HOLDIR" = "" ]]
4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21
then
    #We must be running on ci-server
    echo "HOLDIR not set, starting to install HOL4 into ~/ for current user."
    echo "If this is not intended, please abort with Ctrl-c"
    sleep 5

    #Set HOL4 commit variable
    HOLCOMMIT="$(cat ./.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
    popd
fi

Heiko Becker's avatar
Heiko Becker committed
22
cd ./hol4
Heiko Becker's avatar
Heiko Becker committed
23
#Run configure script to check the versions
24 25
./configure_hol.sh
RET=$?
26

Heiko Becker's avatar
Heiko Becker committed
27
if [ $RET -eq 1 ];
28 29 30 31 32 33
then
   echo "Updating HOL4 to the latest state specified in HOLCOMMIT"
   ./configure_hol.sh --init
else
    echo "Downloading CakeML"
    git submodule init cakeml
Heiko Becker's avatar
Heiko Becker committed
34
    git submodule update -f cakeml
35
fi
Heiko Becker's avatar
Heiko Becker committed
36 37 38

$HOLDIR/bin/Holmake -q

39
cd ./binary
Heiko Becker's avatar
Heiko Becker committed
40 41 42 43

$HOLDIR/bin/Holmake -q checkerBinaryTheory.uo
$HOLDIR/bin/Holmake -q checker.S
$HOLDIR/bin/Holmake -q cake_checker