File: create-acl2-texinfo

package info (click to toggle)
acl2 3.1-1
  • links: PTS
  • area: main
  • in suites: etch, etch-m68k
  • size: 36,712 kB
  • ctags: 38,396
  • sloc: lisp: 464,023; makefile: 5,470; sh: 86; csh: 47; cpp: 25; ansic: 22
file content (93 lines) | stat: -rwxr-xr-x 2,693 bytes parent folder | download
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
#! /bin/sh
# A. Flatau  9-Jul-1993; modified by M. Kaufmann, 26-Oct-1993, also 8/94 and 10/94, etc.
#

# This script should be run by executing
#   make DOC
# or
#   make TEXINFO
# from the main ACL2 directory.  The make variable PREFIX is used in this script.

rm -f doc/workxxx

# The following lines should be commented out if we don't want to
# destroy what's in the saved/ subdirectories.  (As they currently stand,
# we have already arranged not to save doc/TEX.)

rm -rf doc/EMACS-old
## rm -rf doc/LEMACS-old
# rm -rf doc/TEX-old

mv -f doc/EMACS doc/EMACS-old
## mv -f doc/LEMACS doc/LEMACS-old

# mv -f doc/TEX doc/TEX-old
rm -rf doc/TEX

# Now that directories have been moved, re-create them.

mkdir doc/EMACS
## mkdir doc/LEMACS
mkdir doc/TEX
chmod 775 doc/EMACS
## chmod 775 doc/LEMACS
chmod 775 doc/TEX

# 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)' > doc/workxxx
echo '(lp)' >> doc/workxxx

echo '(certify-book "doc/write-acl2-texinfo")' >> doc/workxxx

echo '(write-texinfo-file :dir-string "doc/EMACS/" :file "acl2-doc-emacs" :tex-only-flg nil :non-lucid-flg t)' >> doc/workxxx

## echo '(write-texinfo-file :dir-string "doc/LEMACS/" :file "acl2-doc-lemacs" :tex-only-flg nil)' >> doc/workxxx

echo '(write-tex-file :dir-string "doc/TEX/" :file "acl2-book")' >> doc/workxxx

echo ':q' >> doc/workxxx

${PREFIX}saved_acl2 < doc/workxxx

## emacs -batch "doc/EMACS/acl2-doc-emacs.texinfo" -l "../make-texinfo.el" -f texinfo-format-buffer-and-save

# Replacement for "emacs -batch ..." command above:
cd doc/EMACS ; makeinfo acl2-doc-emacs.texinfo ; cd ../..

## emacs -batch "doc/LEMACS/acl2-doc-lemacs.texinfo" -l "../make-texinfo.el" -f texinfo-format-buffer-and-save

cd doc/TEX

cp ../texinfo.tex .
texi2dvi acl2-book.tex

# We do it again because otherwise some index entries are wrong.

texi2dvi acl2-book.tex

dvips acl2-book.dvi -o acl2-book.ps

gzip acl2-book.dvi
gzip acl2-book.ps

# Make all files world-readable after changing back to doc/.

cd ..

chmod a+r EMACS/*
## chmod a+r LEMACS/*
chmod a+r TEX/*

# To debug bad documentation:
# Start up ACL2 in the source directory.
# (include-book "doc/write-acl2-texinfo")
# Apply DEFDOC to fix bad documentation.
# (write-texinfo-file :dir-string "doc/EMACS/" :file "acl2-doc-emacs" :tex-only-flg nil :non-lucid-flg t)
# One can write others too:
#
## # (write-texinfo-file :dir-string "doc/LEMACS/" :file "acl2-doc-lemacs" :tex-only-flg nil)
# (write-tex-file :dir-string "doc/TEX/" :file "acl2-book")