#! /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 doc/HTML/*.gif

# The next two non-blank lines should be commented out if we don't want to
# destroy what's in the saved/ subdirectory.

rm -f doc/HTML/saved/*
touch doc/HTML/temp.temp
mv -f doc/HTML/*.* doc/HTML/saved

# 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

# Next, copy to ACL2's reports/ subdirectory the papers referenced in
# the home page.  Note that we here rename the papers by author initials
# and dates because their native names sometimes conflict.

# Warning:  If you add more reports to this list or change the names used,
# it would be kind to make the corresponding additions to deflabel bibliography
# in axioms.lisp.

# It would be best to insure that the papers under /home/moore/ut/publications
# are copies of the papers on my UT home page.  That is where the "official"
# versions live now.  See ut/publications/README.

cp /home/moore/ut/publications/bm96.ps reports/bm96.ps
cp /home/moore/ut/publications/bkm96.ps reports/bkm96.ps
cp /home/moore/ut/publications/km97.ps reports/km97.ps
cp /home/moore/ut/publications/km97a.ps reports/km97a.ps

cp /usr/cli/reports/report-101/acl2-design.ps reports/km94.ps
cp /usr/cli/reports/report-116/tse-version/omic-acl2.ps reports/y96a.ps
cp /usr/cli/notes/note-327/autopilot.ps reports/y96b.ps

# Now copy reports to doc/HTML/reports so the home page can refer to them
# with pathnames BELOW that for the home page itself.  In a typical
# installation of ACL2, the home page, doc/HTML/acl2-doc.html, will sit
# below the acl2-sources directory and ../../reports would be visible.
# But at CLI, where we distribute it, the acl2-sources directory structure
# is not present. Just the tar files are present.  So we have to duplicate
# the reports/ subdirectory.

rm -r doc/HTML/reports
mkdir doc/HTML/reports
cp reports/* doc/HTML/reports/

# 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 (:RELATIVE :BACK "write-acl2-html"))' >> workxxx

echo '(write-html-file :file "acl2-doc")' >> workxxx

echo ':q' >> workxxx

../../${PREFIX}saved_acl2 < workxxx

# To debug bad documentation:
# cd /slocal/src/acl2/v1-9/doc/HTML
# ../../large-saved_acl2
# (certify-book "/slocal/src/acl2/v1-9/doc/write-acl2-html")
# or if it hasn't been changed since it was certified, just
# (include-book "/slocal/src/acl2/v1-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")