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
|
#!/usr/bin/bash
set -ex
export COQBIN=$BIN
export PATH=$COQBIN:$PATH
cd misc/qed-time/
# This test checks that the Qed time includes the time of the replayed command
# The version of this test in output-modulo-time checks that each
# command gets 1 time line, but because output-modulo-time normalizes
# times to 0 it can't check that the replayed command is not ignored
rocq c -time file.v > out
last=$(tail -n 1 out)
last=${last#"Chars 98 - 102 [Qed.] "}
last=${last%" secs"*}
# sanity check: regex produces a float
[[ $last =~ [0-9]+"."[0-9]* ]]
test() {
printf 'if %s <= 0.9:\n\texit (1)\n' "$1" | python3
}
# sanity checks: python works on the code we produce
if test 0.9; then exit 1; fi
test 1.
test 1.1
test "$last"
|
