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

3 4
#Set HOL4 commit variable
HOLCOMMIT="$(cat ./hol4/.HOLCOMMIT)"
5 6
FLOVERDIR="$(pwd)"

7 8
#HOL4 always cloned exactly here --> must be in this folder
if [ ! -d "./HOL4" ];
9
then
10
    echo "HOL4 not installed, starting to install HOL4 into current directory."
11 12 13 14 15 16 17 18 19 20 21
    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
22 23
    cd ./HOL4
    export HOLDIR="$(pwd)"
24 25 26 27 28 29 30 31 32 33 34 35 36 37
    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
38

39
cd ./hol4
40

Heiko Becker's avatar
Heiko Becker committed
41 42 43
echo "Downloading CakeML"
git submodule init cakeml
git submodule update -f cakeml
Heiko Becker's avatar
Heiko Becker committed
44

Heiko Becker's avatar
Heiko Becker committed
45
$HOLDIR/bin/Holmake
46 47 48

cd ./binary

49 50 51
$HOLDIR/bin/Holmake checkerBinaryTheory.uo
$HOLDIR/bin/Holmake checker.S
$HOLDIR/bin/Holmake cake_checker