blob: 47960e98d50ba4999889be0dda972ccbecf8af1e (
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
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
|
#!/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 2>&1
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 "coq-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/coq-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
# The reference for time is a 6120 bogomips cpu
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
}
test_bugs () {
# Process verifications concerning submitted bugs. A message is
# printed for all opened bugs (still active or seems to be closed).
# For closed bugs that behave as expected, no message is printed
# All files are assumed to have <# of the bug>.v as a name
echo "Testing opened bugs..."
# We first test opened bugs that should not succeed
files=`/bin/ls -1 $1/opened/shoulnotsucceed/*.v 2> /dev/null`
for f in $files; do
nbtests=`expr $nbtests + 1`
printf " "$f"..."
$command $f $2 > /dev/null 2>&1
if [ $? = 0 ]; then
echo "still active"
nbtestsok=`expr $nbtestsok + 1`
else
echo "Error! (bug seems to be closed, please check)"
fi
done
# And opened bugs that should not fail
files=`/bin/ls -1 $1/opened/shouldnotfail/*.v 2> /dev/null`
for f in $files; do
nbtests=`expr $nbtests + 1`
printf " "$f"..."
$command $f > /dev/null 2>&1
if [ $? != 0 ]; then
echo "still active"
nbtestsok=`expr $nbtestsok + 1`
else
echo "Error! (bug seems to be closed, please check)"
fi
done
echo "Testing closed bugs..."
# Then closed bugs that should succeed
files=`/bin/ls -1 $1/closed/shouldsucceed/*.v 2> /dev/null`
for f in $files; 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! (bug seems to be opened, please check)"
fi
done
# At last, we test closed bugs that should fail
files=`/bin/ls -1 $1/closed/shouldfail/*.v 2> /dev/null`
for f in $files; 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! (bug seems to be opened, please check)"
fi
done
}
test_features () {
# Process verifications concerning submitted bugs. A message is
# printed for all opened bugs (still active or seem to be closed.
# For closed bugs that behave as expected, no message is printed
echo "Testing wishes..."
files=`/bin/ls -1 $1/*.v 2> /dev/null`
for f in $files; do
nbtests=`expr $nbtests + 1`
printf " "$f"..."
$command $f $2 > /dev/null 2>&1
if [ $? != 0 ]; then
echo "still wished"
nbtestsok=`expr $nbtestsok + 1`
else
echo "Good news! (wish seems to be granted, please check)"
fi
done
}
# Programme principal
echo "Success tests"
test_success success
echo "Failure tests"
test_failure failure
echo "Bugs tests"
test_bugs bugs
echo "Output tests"
test_output output
echo "Parser tests"
test_parser parser
echo "Interactive tests"
test_interactive interactive
echo "Micromega tests"
test_success micromega
# We give a chance to disable the complexity tests which may cause
# random build failures on build farms
if [ -z "$COQTEST_SKIPCOMPLEXITY" ]; then
echo "Complexity tests"
test_complexity complexity
else
echo "Skipping complexity tests"
fi
echo "Module tests"
$coqtop -compile modules/Nat
$coqtop -compile modules/plik
test_success modules "-I modules -impredicative-set"
#echo "Ideal-features tests"
#test_features ideal-features
pourcentage=`expr 100 \* $nbtestsok / $nbtests`
echo
echo "$nbtestsok tests passed over $nbtests, i.e. $pourcentage %"
|