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
|
#!/usr/bin/env bash
#set -x
set -e
# tools
TTOOLSDIR="$COQPREFIX/lib/coq-core/tools"
export make_both_time_files="$TTOOLSDIR"/make-both-time-files.py
export make_one_time_file="$TTOOLSDIR"/make-one-time-file.py
export make_both_single_timing_files="$TTOOLSDIR"/make-both-single-timing-files.py
#
NONATIVECOMP=$(grep "let native_compiler = NativeOff" ../../../config/coq_config.ml)||true
if [[ ! $NONATIVECOMP ]]; then exit 0 ; fi
. ../template/path-init.sh
# reset MAKEFLAGS so that, e.g., `make -C test-suite -B coq-makefile` doesn't give us issues
MAKEFLAGS=
cd precomputed-time-tests
./run.sh || exit $?
cd ../error
coq_makefile -f _CoqProject -o Makefile
make cleanall
if make pretty-timed TGTS="all" -j1; then
echo "Error: make pretty-timed should have failed"
exit 1
fi
cd ../aggregate
coq_makefile -f _CoqProject -o Makefile
make cleanall
make pretty-timed TGTS="all" -j1 || exit $?
cd ../before
coq_makefile -f _CoqProject -o Makefile
make cleanall
make make-pretty-timed-before TGTS="all" -j1 || exit $?
cd ../after
coq_makefile -f _CoqProject -o Makefile
make cleanall
make make-pretty-timed-after TGTS="all" -j1 || exit $?
rm -f time-of-build-before.log
make print-pretty-timed-diff TIMING_SORT_BY=diff TIME_OF_BUILD_BEFORE_FILE=../before/time-of-build-before.log
cp ../before/time-of-build-before.log ./
make print-pretty-timed-diff TIMING_SORT_BY=diff || exit $?
INFINITY="∞"
INFINITY_REPLACEMENT="+.%" # assume that if the before time is zero, we expected the time to increase
TO_SED_IN_BOTH=(
-e s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" # Whether or not something shows up as ∞ depends on whether a time registers as 0.s or as 0.001s, so we can't rely on this being consistent
-e s':|\s*N/A\s*$:| '"${INFINITY_REPLACEMENT}"':g' # Whether or not something shows up as N/A depends on whether a time registers as 0.s or as 0.001s, so we can't rely on this being consistent
-e s'/ *$//g' # the number of trailing spaces depends on how many digits percentages end up being; since this varies across runs, we remove trailing spaces
-e s'/[0-9]*\.[0-9]*//g' # the precise timing numbers vary, so we strip them out
-e s'/^-*$/------/g' # When none of the numbers get over 100 (or 1000, in per-file), the width of the table is different, so we normalize the number of dashes for table separators
-e s'/+/-/g' # some code lines don't really change, but this can show up as either -0m00.01s or +0m00.01s, so we need to normalize the signs; additionally, some N/A's show up where we expect to get -∞ on the per-line file, and so the ∞-replacement gets the sign wrong, so we must correct it
-e s'/[0-9]//g' # sometimes the time is under 1 minute, sometimes it's over 1 minute, so we want to remove/normalize both instances; see https://github.com/coq/coq/issues/5675#issuecomment-487378622
)
TO_SED_IN_PER_FILE=(
-e s'/ */ /g' # unclear whether this is actually needed for per-file timing; it's been here from the start
-e s'/\(Total.*\)-\(.*\)-/\1+\2+/g' # Overall time in the per-file timing diff should be around 0; if it comes out negative, we remove the sign
-e s'/- ko/ko/g' # for small amounts of memory, signs can flip, so we remove mem signs
)
TO_SED_IN_PER_LINE=(
-e s'/ */ /g' # Sometimes 0 will show up as 0m00.s, sometimes it'll end up being more like 0m00.001s; we must strip out the spaces that result from left-aligning numbers of different widths based on how many digits Coq's [-time] gives
-e s'/^ *//g' # the number of leading spaces can differ, e.g., as in the difference between ' 0m13.53s' vs '0m13.582s'
)
for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do
for ext in "" .desired; do
sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_FILE[@]}" ${file}${ext} > ${file}${ext}.processed
done
echo "cat $file"
cat "$file"
echo
diff -u $file.desired.processed $file.processed || exit $?
done
cd ../per-file-before
coq_makefile -f _CoqProject -o Makefile
make cleanall
make all TIMING=before -j2 || exit $?
cd ../per-file-after
coq_makefile -f _CoqProject -o Makefile
make cleanall
make all TIMING=after -j2 || exit $?
find ../per-file-before/ -name "*.before-timing" -exec 'cp' '{}' './' ';'
make all.timing.diff -j2 || exit $?
echo "cat A.v.before-timing"
cat A.v.before-timing
echo
echo "cat A.v.after-timing"
cat A.v.after-timing
echo
echo "cat A.v.timing.diff"
cat A.v.timing.diff
echo
file=A.v.timing.diff
for ext in "" .desired; do
sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_LINE[@]}" < "${file}${ext}" | sort > "${file}${ext}.processed"
done
diff -u "$file.desired.processed" "$file.processed" || exit $?
exit 0
|
