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
|
#!/bin/sh
if [ -z "${ACL2_SOURCES}" ] ; then \
echo "ERROR: Environment variable ACL2_SOURCES must have a non-empty string"
echo " as its value. Perhaps you intended to call"
echo " $0"
echo " from GNUmakefile using \"make STATS\"."
exit 1 ;\
fi
# Here we remove doc.lisp from the sources, since its contents are a
# direct extraction of the contents of books/system/doc/acl2-doc.lisp,
# whose size is reported separately. Actually, this step isn't
# necessary (as of this writing) when executing "make STATS" in the
# parent directory (i.e., the ACL2 sources directory), because
# doc.lisp is explicitly excluded from ACL2_SOURCES there. But
# because we exclude doc.lisp ourselves, we do not depend on that
# exclusion.
actual_sources=`echo $ACL2_SOURCES | sed 's/doc.lisp//'`
if [ "$DEBUG" != "" ] ; then
echo "actual_sources = $actual_sources"
fi
echo 'Computing code size statistics.'
if [ "$ACL2" = "" ] ; then
echo "Note: Setting variable ACL2 to the default: acl2."
ACL2=acl2
fi
echo '; Lines / Characters' > doc/acl2-wc.txt
echo '; Code lines (whitespace followed by non-whitespace other than ; ):' >> doc/acl2-wc.txt
# The following commands assume that the only whitespace characters
# are newlines and spaces. We check for that in write-acl2-code-size.
# We also assume that there are no multi-line comments, but we don't
# check this because we have one in a :doc string, as displayed just
# below. We could perhaps, with some effort, count those and also
# count them in :doc strings, and make sure the difference is 0; but
# we haven't done so. For now, one can do something like the
# following, manually:
# % grep -a '^[^;]*#|' *.lisp
# doc.lisp: including books, for example in multi-line comments (#|..|#).
# %
# Similarly we can check for tabs as follows; never mind the ones in doc.lisp.
# % grep -aP "^[^;]*\t" *.lisp
# doc.lisp: Declaration | Type-Spec |
# doc.lisp: (type string x y z) | string |
# doc.lisp: (type (integer 0 7) x) | (integer 0 7) |
# doc.lisp: (type rational x) | rational |
# doc.lisp: (type (rational 1 *) x) | (rational 1 *) |
# %
# Note the use of the -a option. Without it, the results can be
# way off, at least on Linux, because of the line
# ; Francisco J. MartÃn Mateos
# under "PRINTING and READING" in axioms.lisp -- the accented "i" is the culprit.
(cat ${actual_sources} | grep -a '^[ ]*[^ ;]' | wc -lc) >> doc/acl2-wc.txt
echo '; Comment lines ( ; preceded only by whitespace):' >> doc/acl2-wc.txt
(cat ${actual_sources} | grep -a '^[ ]*;' | wc -lc) >> doc/acl2-wc.txt
echo '; Blank lines (only whitespace):' >> doc/acl2-wc.txt
(cat ${actual_sources} | grep -a '^[ ]*$' | wc -lc) >> doc/acl2-wc.txt
echo '; TOTAL:' >> doc/acl2-wc.txt
(cat ${actual_sources} | wc -lc) >> doc/acl2-wc.txt
wc -lc books/system/doc/acl2-doc.lisp >> doc/acl2-wc.txt
cd doc
echo '(value :q)' > workxxx.create-acl2-code-size
echo '(lp)' >> workxxx.create-acl2-code-size
echo '(certify-book "write-acl2-code-size")' >> workxxx.create-acl2-code-size
echo '(acl2::write-acl2-code-size "acl2-wc.txt" "acl2-code-size.txt")' >> workxxx.create-acl2-code-size
echo ':q' >> workxxx.create-acl2-code-size
echo '(acl2::quit)' >> workxxx.create-acl2-code-size
${ACL2} < workxxx.create-acl2-code-size
# We could remove acl2-wc.txt at this point, but it seems harmless to leave it.
rm -f workxxx.create-acl2-code-size
echo ''
echo 'Finished computing code size statistics.'
|
