regressiontests.sh 868 Bytes
Newer Older
1 2
#!/bin/bash

3 4
eval `opam config env`

5 6 7 8 9
cd ./testcases/regression

#Coq regression tests
for fname in ./*.v; do
    coqc -R ../../coq Flover $fname
10
    if [ $? -eq 0 ]
11
    then
12 13
       echo "Successfully checked $fname"
    else
14 15 16
       echo "Checking $fname failed"
       exit 1;
    fi
17

18 19 20
done

#HOL4 regression tests
21 22
HOLDIR=../../HOL4

23 24 25
for fname in ./*.sml; do
    FILEPRE=${fname/Script.sml/}
    FILENAME=$FILEPRE
26 27
    $HOLDIR/bin/Holmake ${fname/Script.sml/Theory.sig}
    if [ $? -eq 0 ]
28
    then
29 30
       echo "Successfully checked $FILENAME"
    else
31 32 33 34 35 36 37 38
       echo "Checking $FILENAME has failed"
       exit 1;
    fi
done

#Binary regression tests
for fname in ./*.txt; do
    ../../hol4/binary/cake_checker $fname
39
    if [ $? -eq 0 ]
40
    then
41 42
        echo "Successfully checked $fname";
    else
43 44 45
        echo "Checking $fname has failed"
        exit 1;
    fi
46

47
done