aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/check
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 %"