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
|
#!/bin/sh
# This script fully qualifies all the 'Require' statements of the given
# targets (or the current directory if none).
#
# It assumes that all the prerequisites are already installed. The
# install location is found using the COQLIB, COQC, COQBIN variables if
# set, 'coqc' otherwise.
#
# Option --exclude can be used to ignore a given user contribution. In
# particular, it can be used to ignore the current set of files if it
# happens to be already installed.
#
# Option --stdlib can be used to also qualify the files from the standard
# library.
if test ! "$COQLIB"; then
if test ${COQBIN##*/}; then COQBIN=$COQBIN/; fi
if test ! "$COQC"; then COQC=`which ${COQBIN}coqc`; fi
COQLIB=`"$COQC" -where`
fi
stdlib=no
exclude=""
scan_dir () {
(cd $1 ; find $3 -name '*.vo' |
sed -e "s,^./,$2,;s,\([^./]*\)/,\1.,g;s,\([^.]*\).vo,\1,")
}
scan_all_dir () {
if test $stdlib = yes; then
scan_dir "$COQLIB/theories" "Coq."
scan_dir "$COQLIB/plugins" "Coq."
fi
scan_dir "$COQLIB/user-contrib" "" "$exclude"
}
create_script () {
echo "BEGIN {"
scan_all_dir |
while read file ; do
echo $file | sed -e "s,\(.*\)[.]\([^.]*\), t[\"\2\"] = \"\1.\2\","
done
cat <<EOF
}
\$1 ~ "Require" {
for (i = 2; i <= NF; ++i) {
if (\$i ~ /[.]\$/) {
s = substr(\$i,1,length(\$i)-1)
if (t[s]) \$i = t[s] "."
break
} else if (t[\$i]) \$i = t[\$i]
}
print
next
}
{ print }
EOF
}
usage () {
cat <<EOF
Usage: $0 [OPTION...] [TARGET...]
The default TARGET is the current directory.
Available options:
--exclude CONTRIB Do not qualify path to the given CONTRIB
--stdlib Qualify files from the standard library
--help Display this message
EOF
}
dir=""
while : ; do
case "$1" in
"")
break;;
-h|--help)
usage
exit 0;;
--exclude)
exclude="$exclude -path ./$2 -prune -type f -o"
shift;;
--stdlib)
stdlib=yes;;
-*)
echo "Unknown option $1" 1>&2
exit 1;;
*)
dir="$dir $1";;
esac
shift
done
script=`tempfile`
create_script > $script
find $dir -name '*.v' |
while read file; do
mv $file $file.bak
awk -f $script $file.bak > $file
done
|
