blob: 504e96cc249c7325f96fb4fe1ce989bad69c8ea5 (
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
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
|
#!/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
}
# La fonction suivante teste en interactif
# It expects a line "(* Expected time < XXX.YYs *)" in the .v file
# with exactly two digits after the dot
test_complexity() {
if [ -f /proc/cpuinfo ]; then
if grep -q bogomips /proc/cpuinfo; then # i386, ppc
bogomips=`sed -n -e "s/bogomips.*: \([0-9]*\).*/\1/p" /proc/cpuinfo | head -1`
elif grep -q Cpu0Bogo /proc/cpuinfo; then # sparc
bogomips=`sed -n -e "s/Cpu0Bogo.*: \([0-9]*\).*/\1/p" /proc/cpuinfo | head -1`
elif grep -q BogoMIPS /proc/cpuinfo; then # alpha
bogomips=`sed -n -e "s/BogoMIPS.*: \([0-9]*\).*/\1/p" /proc/cpuinfo | head -1`
fi
fi
if [ "$bogomips" = "" ]; then
echo " cannot run complexity tests (no bogomips found)"
else
for f in $1/*.v; do
nbtests=`expr $nbtests + 1`
printf " "$f"..."
# extract effective user time
res=`$command $f 2>&1 | sed -n -e "s/Finished transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1`
if [ $? != 0 ]; then
echo "Error! (should be accepted)"
elif [ "$res" = "" ]; then
echo "Error! (couldn't find a time measure)"
else
# express effective time in centiseconds
res=`echo "$res"00 | sed -n -e "s/\([0-9]*\)\.\([0-9][0-9]\).*/\1\2/p"`
# find expected time * 100
exp=`sed -n -e "s/(\*.*Expected time < \([0-9]\).\([0-9][0-9]\)s.*\*)/\1\2/p" $f`
ok=`expr \( $res \* $bogomips \) "<" \( $exp \* 6120 \)`
if [ "$ok" = 1 ]; then
echo "Ok"
nbtestsok=`expr $nbtestsok + 1`
else
echo "Error! (should run faster)"
fi
fi
done
fi
}
# 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 "Complexity tests"
test_complexity complexity
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
|
