1
2
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
|
#!/bin/bash
set -e
function hol_light () {
./ocaml -init hol.ml
}
function holtest() {
echo "######################## HOL Light test $1 ###################"
echo "loadt \"$1\";;" | hol_light 2>&1 | tee /tmp/hol-light-test-log
if egrep -i 'error|not.found' /tmp/hol-light-test-log ; then
echo
echo Error in $1, test failed
false
fi
}
holtest Library/agm.ml
# holtest Library/binary.ml
# holtest Library/binomial.ml
# holtest Library/card.ml
# The prover9 example fails in a clean build environment, because
# prover9 is not installed there. If you want to test whether error
# detection works in this script, uncomment the next holtest line.
#holtest Examples/prover9.ml
|
