blob: 99893f882602df100dc091d69c2b4219f2233656 (
plain)
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
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
|
#!/bin/sh
# Automatic test of Coq
if [ "$1" = -byte ]; then
coqtop="../bin/coqtop.byte -q -batch"
else
coqtop="../bin/coqtop -q -batch"
fi
command="$coqtop -top Top -load-vernac-source"
# on compte le nombre de tests et de succès
nbtests=0
nbtestsok=0
# La fonction suivante teste le compilateur sur des fichiers qu'il doit
# accepter
test_success() {
for f in $1/*.v; do
nbtests=`expr $nbtests + 1`
printf " "$f"..."
$command $f $2 > /dev/null 2>&1
if [ $? = 0 ]; then
echo "Ok"
nbtestsok=`expr $nbtestsok + 1`
else
echo "Error! (should be accepted)"
fi
done
}
# La fonction suivante teste le compilateur sur des fichiers qu'il doit
# refuser
test_failure() {
for f in $1/*.v; do
nbtests=`expr $nbtests + 1`
printf " "$f"..."
$command $f > /dev/null 2>&1
if [ $? != 0 ]; then
echo "Ok"
nbtestsok=`expr $nbtestsok + 1`
else
echo "Error! (should be rejected)"
fi
done
}
# La fonction suivante teste la sortie des fichiers qu'elle exécute
test_output() {
for f in $1/*.v; do
nbtests=`expr $nbtests + 1`
printf " "$f"..."
tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`
$command $f 2>&1 | grep -v "Welcome to Coq" | grep -v "Skipping rcfile loading" > $tmpoutput
foutput=`dirname $f`/`basename $f .v`.out
diff $tmpoutput $foutput >& /dev/null
if [ $? = 0 ]; then
echo "Ok"
nbtestsok=`expr $nbtestsok + 1`
else
echo "Error! (unexpected output)"
fi
rm $tmpoutput
done
}
# La fonction suivante teste l'analyseur syntaxique fournit par "parser"
# Elle fonctionne comme test_output
test_parser() {
if [ -d $1 ]; then
for f in $1/*.v; do
nbtests=`expr $nbtests + 1`
printf " "$f"..."
tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`
foutput=`dirname $f`/`basename $f .v`.out
echo "parse_file 1 \"$f\"" | ../bin/parser > $tmpoutput 2>&1
perl -ne 'if(/Starting.*Parser Loop/){$printit = 1};print if $printit' \
$tmpoutput 2>&1 | grep -i error > /dev/null
if [ $? = 0 ] ; then
echo "Error! (unexpected output)"
else
echo "Ok"
nbtestsok=`expr $nbtestsok + 1`
fi
rm $tmpoutput
done
fi
}
# La fonction suivante teste en interactif
test_interactive() {
for f in $1/*.v; do
nbtests=`expr $nbtests + 1`
printf " "$f"..."
$coqtop < $f > /dev/null 2>&1
if [ $? = 0 ]; then
echo "Ok"
nbtestsok=`expr $nbtestsok + 1`
else
echo "Error! (should be accepted)"
fi
done
}
# Programme principal
echo "Success tests"
test_success success
echo "Failure tests"
test_failure failure
echo "Output tests"
test_output output
echo "Parser tests"
test_parser parser
echo "Interactive tests"
test_interactive interactive
echo "Module tests"
$coqtop -compile modules/Nat
$coqtop -compile modules/plik
test_success modules "-I modules -impredicative-set"
pourcentage=`expr 100 \* $nbtestsok / $nbtests`
echo
echo "$nbtestsok tests passed over $nbtests, i.e. $pourcentage %"
#echo "Ideal-features tests"
#test_success ideal-features
|
