ci-hol4.sh 745 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
then
    #We must be running on ci-server
6
    echo "HOLDIR not set, starting to install HOL4 into current directory."
7 8 9 10
    echo "If this is not intended, please abort with Ctrl-c"
    sleep 5

    #Set HOL4 commit variable
Heiko Becker's avatar
Heiko Becker committed
11
    HOLCOMMIT="$(cat ./hol4/.HOLCOMMIT)"
12 13 14 15 16
    git clone https://github.com/HOL-Theorem-Prover/HOL.git HOL4
    cd HOL4
    git checkout $HOLCOMMIT
    poly < tools/smart-configure.sml
    bin/build
17 18
    export HOLDIR="$(pwd)"
    cd ../
19 20
fi

Heiko Becker's avatar
Heiko Becker committed
21
cd ./hol4
22

Heiko Becker's avatar
Heiko Becker committed
23 24 25
echo "Downloading CakeML"
git submodule init cakeml
git submodule update -f cakeml
Heiko Becker's avatar
Heiko Becker committed
26 27 28

$HOLDIR/bin/Holmake -q

29
cd ./binary
Heiko Becker's avatar
Heiko Becker committed
30 31 32 33

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