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
|
#!/bin/bash
#
# This file is part of Proof General.
#
# © Copyright 2021 Hendrik Tews
#
# Authors: Hendrik Tews
# Maintainer: Hendrik Tews <hendrik@askra.de>
#
# SPDX-License-Identifier: GPL-3.0-or-later
#
# See function usage for documentation.
set -e
#set -x
function usage(){
cat <<-EOF
usage: compile-test-start-delayed key prog args...
Start program prog with arguments args with some delay. There
must be at least one argument in args and the last one must be
a file or something that becomes a file when ".v" is appended.
The delay is taken from a line in that file that
contains the key, followed by a space and the delay in seconds
(maybe somewhere in the middle of the line). The file must
contain at most one line containing key. When there is no line
containing key the delay is zero. As a special case, a delay
equal to X means to record the fact that prog has been called
on file by creating a file with suffix ".X" added to the name
of file. The absence of this .X file can then be used, for
instance, to check that prog has not been called on file. With
delay equal to X, the real delay is 0.
Fractional delays are properly handled.
EOF
}
if [ $# -lt 3 ] ; then
usage
exit 1
fi
# echo compile-test-start-delayed "$@"
key="$1"
file="${@: -1}"
#echo key $key file "\"$file\""
shift
# vio2vo needs a module name or a .vio file on the command line
# support only module names for now
if [ ! -f "$file" ] ; then
if [ -f "$file.v" ] ; then
file="$file.v"
else
exit 22
fi
fi
delay=$(sed -ne "/$key/ s/.*$key \([X0-9.]*\).*/\1/p" $file)
if [ -z "$delay" ] ; then
# echo compile-test-start-delayed: key $key not found in $file >&9
delay=0
elif [ "$delay" = "X" ] ; then
echo compile-test-start-delayed: delay X for $file >&9
delay=0
touch $file.X
fi
# use string comparison on $delay to permit fractional values
if [ $delay != 0 ] ; then
date "+compile-test-start-delayed %T delay $delay for $*" >&9
sleep $delay
date "+compile-test-start-delayed %T start now $*" >&9
else
date "+compile-test-start-delayed %T start without delay $*" >&9
fi
#set -x
#echo "$@"
set +e
exec "$@"
|
