Save
Saves the XDOC database into files for web browsers, etc.
Once you have documented your books with defxdoc, you may
wish to create a manual that can be viewed from a web browser or from the
acl2-doc Emacs-based browser (see ACL2::ACL2-doc).
Basic Example
;; my-manual.lisp - a book that creates a manual
(in-package "MYPKG")
(include-book "my-library1") ;; load books I want in the manual
(include-book "my-library2") ;; (documented with xdoc)
(include-book "xdoc/save" :dir :system) ;; load xdoc::save
(defxdoc acl2::top ;; create a "top" topic
:short "My Manual"
:long "<p>This manual explains how to use my books...</p>")
(xdoc::save "./mylib-manual" :error t) ;; write the manual
Notes about this example:
- The xdoc::save command will export all currently-loaded, documented
topics. Because of this, you can mostly control what goes into the manual
just by including books, but see below for additional notes about how to
control what goes in a manual.
- The save command is a macro that expands into ACL2::embedded-event-forms. Typically, you just put it into a new book (e.g.,
my-manual.lisp above) so that your manual will be regenerated as part of
building your project.
- The save requires certain trust
tags. You may need to enable trust tags in your build system to certify
the my-manual book. For instance, cert.pl users may need a
.acl2 file with a line such as:
; cert-flags: ? t :ttags :all
- After saving a manual, you should be able to view it by going to, e.g.,
mylib-manual/index.html in your web browser. If you want to share your
manual with others, you should read about deploying-manuals.
General Form
(save <target-dir>
[:redef-okp bool] ;; default is nil
[:zip-p bool] ;; default is t
[:logo-image path] ;; default is nil
[:error bool] ;; default is nil
[:broken-links-limit nil-or-nat] ;; default is nil
)
The only (required) argument to the save command is the name of a
directory where the want the manual to go. All arguments are evaluated.
As might be expected:
- If the target directory does not exist, it will be created.
- If the target directory already exists, it will be
overwritten. (WARNING: So, the
target directory should not be one containing files that you want to keep, such
as the directory containing the file that invokes xdoc::save, or its
parent directory (or its parent, etc.).)
Option Summary
- redef-okp
- By default, the save command will complain if any topic is defined
more than once. This is often annoying when you are developing books,
especially if your books are slow to certify and you don't want to have your
build fail just because of a documentation problem. So, if you want to
suppress this error (and turn it into a printed warning), you can set
:redef-okp t.
- zip-p
- To support the Download this Manual
feature (normally accessed from the toolbar button) the save command will
zip up the manual to create .tar.gz, .tar.bz2, and .zip files.
If you don't care about generating these files and want to avoid the time to
build them, you can set :zip-p nil.
- :logo-image
- You can provide a custom image to use as the logo for the top topic.
The path you provide should be relative to whatever book contains the save
command.
- :error
- The value is t or nil, to indicate whether or not (respectively)
to cause an error upon encountering a syntax error in xdoc source (marked with
"xdoc error").
- :broken-links-limit
- The value is nil by default. Otherwise, it is a natural number
specifying the maximum allowed number of broken links; if the ``broken topic
link'' report shows more broken links than that limit, an error occurs.
Avoiding Unwanted Documentation
By default, the save command will generate a manual that covers the
documentation for all books that you have loaded. This usually works well
as long as you know all of the books that you need to include.
One caveat is that xdoc/save includes some supporting books that are,
themselves, documented. Accordingly, you may find that your manual includes
documentation from libraries like ACL2::std/strings and ACL2::oslib in your output even if you haven't loaded these libraries
yourself. If you really want precise control over what goes into your manual,
then, you may want to do something like this:
;; nothing-extra-manual.lisp - manual with nothing extra
(in-package "MYPKG")
(include-book "my-library1") ;; load books I want in the manual
(include-book "my-library2") ;; (documented with xdoc)
(make-event ;; save current documentation
`(defconst *just-my-documentation*
',(xdoc::get-xdoc-table (w state))))
(include-book "xdoc/save" :dir :system)
;; clobber any docs that were added due to xdoc/save
(table xdoc::xdoc 'xdoc::doc *just-my-documentation*)
(defxdoc acl2::top ;; create a "top" topic
:short "My Manual"
:long "<p>This manual explains how to use my books...</p>")
(xdoc::save "./mylib-manual" :error t)Subtopics
- Deploying-manuals
- How to distribute XDOC manuals for other people to use.
