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
|
#! /bin/sh
# This script should be run by executing
# make DOC
# from the main ACL2 directory. The environment variable ACL2 is used
# in this script; it MUST be set. To run this script directly in the
# doc/ directory, submit something like this:
# (export ACL2=~/acl2/devel/saved_acl2 ; ./create-doc)
if [ "$ACL2" = "" ] ; then
echo "Note: Setting variable ACL2 to the default: acl2."
ACL2=acl2
fi
# It is our convention to keep the .fig and .gif files in graphics/
# (under the main ACL2 source directory. The present script copies
# the *.gif files from that source to the doc/HTML subdirectory where
# they will reside for convenient HTML access.
if [ ! -d HTML ] ; then
mkdir HTML
chmod 775 HTML
# Now copy the definitive .gif files over to HTML.
cp -p ../graphics/*.gif HTML
# At one time we copid the license down to the HTML so the home
# page can reference it, but this no longer seems necessary.
# cp ../LICENSE HTML/LICENSE
# Copy down the files we are allowed to change without rebuilding.
cp ../new.html HTML/new.html
mkdir HTML/installation
cp ../installation/ccl.html HTML/installation/
cp ../installation/installation.html HTML/installation/
cp ../installation/misc.html HTML/installation/
cp ../installation/obtaining-and-installing.html HTML/installation/
cp ../installation/requirements.html HTML/installation/
cp ../installation/using.html HTML/installation/
cp ../installation/windows7.html HTML/installation/
cp ../installation/windows-gcl-jared.html HTML/installation/
cp ../installation/installing-make.html HTML/installation/
cp ../other-releases.html HTML/other-releases.html
cp ../workshops.html HTML/workshops.html
cp ../LICENSE HTML/LICENSE
fi
# Ok, now we are ready!
# We expect ACL2 images to start up inside LP. But rather than count
# on that, we submit (value :q) to get us out of the loop and then
# (lp) to get us back into the loop.
echo '(value :q)' > workxxx
echo '(lp)' >> workxxx
echo '(certify-book "home-page")' >> workxxx
echo ':u' >> workxxx
echo '(include-book "home-page")' >> workxxx
echo '(write-home-page-top)' >> workxxx
echo ':q' >> workxxx
echo '(acl2::quit)' >> workxxx
echo "ACL2 = $ACL2"
echo "Certifying home-page.lisp and writing home-page.html; see home-page.out..."
$ACL2 < workxxx > home-page.out
echo "Done"
cp home-page.html HTML/
rm -f workxxx
|
