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

3 4 5 6 7 8 9 10 11 12 13 14 15 16 17
#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 ../

18

Heiko Becker's avatar
Heiko Becker committed
19
cd ./hol4
20

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

$HOLDIR/bin/Holmake -q

27
cd ./binary
Heiko Becker's avatar
Heiko Becker committed
28 29 30 31

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