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
|
#! /bin/sh
# This script should be run by executing
# make DOC
# or
# make HTML
# from the main ACL2 directory. The make variable PREFIX is used in this script.
rm -f doc/workxxx
# It is our convention to keep the .fig and .gif files in acl2/graphics/
# (note version independence). As part of this creation, we copy the *.gif
# files from that source to the doc/HTML subdirectory where they will
# reside for convenient HTML access. We delete the copies on doc/HTML
# every time we rebuild, because the definitive copies are on acl2/graphics/.
rm -f doc/HTML/*.gif
# The next two non-blank lines should be commented out if we don't want to
# destroy the preceding version.
rm -rf doc/HTML-old
mv -f doc/HTML doc/HTML-old
mkdir doc/HTML
chmod 775 doc/HTML
# Now copy the definitive .gif files over to doc/HTML.
cp ../graphics/*.gif doc/HTML
# Copy the license down to the doc/HTML so the home page can reference it.
cp LICENSE doc/HTML/LICENSE
# Copy down the files we are allowed to change without rebuilding.
cp new.html doc/HTML/new.html
cp installation.html doc/HTML/installation.html
cp other-releases.html doc/HTML/other-releases.html
cp workshops.html doc/HTML/workshops.html
# Ok, now we are ready!
cd doc/HTML
# Some ACL2 images start up inside LP; some don't. (value :q) always gets us
# out of the loop, and should also be harmless when executed in raw Lisp.
# However, note that Lispworks requires that the two forms not all be on the
# same line.
echo '(value :q)' > workxxx
echo '(lp)' >> workxxx
echo '(certify-book "../write-acl2-html")' >> workxxx
echo '(write-html-file :file "acl2-doc")' >> workxxx
echo ':q' >> workxxx
../../${PREFIX}saved_acl2 < workxxx
# Make all files world-readable.
chmod a+r *
# To debug bad documentation:
# cd /projects/acl2/v2-9/doc/HTML
# ../../large-saved_acl2
# (certify-book "/projects/acl2/v2-9/doc/write-acl2-html")
# or if it hasn't been changed since it was certified, just
# (include-book "/projects/acl2/v2-9/doc/write-acl2-html")
# Redefine whatever you need in the image, e.g., *home-page*.
# Apply DEFDOC to fix bad documentation.
# (write-html-file :file "acl2-doc")
|
