File: run.sh

package info (click to toggle)
coq-doc 8.20.0-2
  • links: PTS, VCS
  • area: non-free
  • in suites: forky, sid, trixie
  • size: 46,708 kB
  • sloc: ml: 234,429; sh: 4,686; python: 3,359; ansic: 2,644; makefile: 842; lisp: 172; javascript: 87; xml: 24; sed: 2
file content (31 lines) | stat: -rw-r--r-- 870 bytes parent folder | download | duplicates (2)
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
#!/usr/bin/env bash

. ../timing-template/init.sh

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 $?

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