regressiontests.sh 1.69 KB
Newer Older
1 2
#!/bin/bash

3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37
HOLCOMMIT="$(cat ./hol4/.HOLCOMMIT)"
FLOVERDIR="$(pwd)"

#HOL4 regression tests
if [ ! -d "./HOL4" ];
then
    echo "HOL4 not installed, 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 ./HOL4
    export HOLDIR="$(pwd)"
    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
eval `opam config env`

40 41 42 43 44
cd ./testcases/regression

#Coq regression tests
for fname in ./*.v; do
    coqc -R ../../coq Flover $fname
45
    if [ $? -eq 0 ]
46
    then
47 48
       echo "Successfully checked $fname"
    else
49 50 51
       echo "Checking $fname failed"
       exit 1;
    fi
52

53 54 55
done

#HOL4 regression tests
56
$HOLDIR/bin/Holmake heap
57

58 59 60
for fname in ./*.sml; do
    FILEPRE=${fname/Script.sml/}
    FILENAME=$FILEPRE
61 62
    $HOLDIR/bin/Holmake ${fname/Script.sml/Theory.sig}
    if [ $? -eq 0 ]
63
    then
64 65
       echo "Successfully checked $FILENAME"
    else
66 67 68 69 70 71 72 73
       echo "Checking $FILENAME has failed"
       exit 1;
    fi
done

#Binary regression tests
for fname in ./*.txt; do
    ../../hol4/binary/cake_checker $fname
74
    if [ $? -eq 0 ]
75
    then
76 77
        echo "Successfully checked $fname";
    else
78 79 80
        echo "Checking $fname has failed"
        exit 1;
    fi
81

82
done