Xdoc
XDOC is a tool for documenting ACL2 books. You can use it to
access documentation about ACL2 and its books, to document your own books, and
to create custom web-based manuals.
Below we cover how to use XDOC to build manuals or document your
own ACL2::books. If you just want to browse the documentation, you
probably don't need to read any of this! Instead, see documentation.
Starting Points
A good, tutorial-style introduction to XDOC can be found in:
Jared Davis and Matt Kaufmann. Industrial Strength Documentation
for ACL2. ACL2 Workshop 2014. EPTCS 152. Pages 9-25.
See Building the Manual under ACL2::books-certification for
information on building the ACL2+Books manual. See testing for easy
instructions for how to test your XDOC strings.
To use XDOC to document your own books, the first step is:
(include-book "xdoc/top" :dir :system)
This book loads very quickly and requires no ttags. It gives you defxdoc and defsection, the basic commands for adding documentation.
It also installs a new :doc command, via ld-keyword-aliases, so
that you can see new documentation from the terminal.
For a possibly more convenient way to construct XDOC strings, do the
following:
(include-book "xdoc/constructors" :dir :system)
This book includes community book xdoc/top.lisp, and in addition
provides utilities to construct well-formed XDOC strings in a modular way. See
the documentation for more
details.
Once you have documented your books, you may wish to create a manual that
can be viewed from a web browser or from the ACL2::ACL2-doc Emacs-based
browser. You can do this quite easily with XDOC's save command.
This command can be embedded in an ordinary ACL2 book, so that your manual is
automatically regenerated when you build your project.
New Features
XDOC now supports katex-integration for writing LaTeX-like formulas
like
\left( \sum_{i=0}^{n} \sqrt{f(i)} \right) < \frac{n^2}{k}
within your documentation.
When writing documentation, you can now optionally have XDOC topics
automatically displayed as you submit new defxdoc forms—just
add:
(include-book "xdoc/debug" :dir :system)
to your ACL2::ACL2-customization file, or include it while you are
developing your book. Afterward, each defxdoc form you submit will be
immediately shown at the terminal, giving you a quick, text-mode preview that
may help you to diagnose any markup problems.
Subtopics
- Undocumented
- Placeholder for documentation topics that lack good :parents.
- Save
- Saves the XDOC database into files for web browsers, etc.
- Defsection
- Fancy (encapsulate nil ...) with a name and xdoc support.
- Markup
- The XML markup
language that is the basis of XDOC documentation strings.
- Preprocessor
- In addition to its markup language, XDOC includes a
preprocessor which can be used to interpret certain directives of the form
@(...).
- Emacs-links
- Instructions for integrating XDOC web pages with Emacs.
- Defxdoc
- Add documentation to the xdoc database.
- Katex-integration
- Support for LaTeX-like typesetting of mathematics in XDOC
topics. (experimental)
- Constructors
- Utilities to costruct
well-formed XDOC strings.
- Entities
- HTML entity support in XDOC.
- Save-rendered
- Saves the XDOC database into files for the acl2-doc browser
- Add-resource-directory
- Tell xdoc about directories of resources (e.g., images, PDF
files, etc.) that should be copied into manuals.
- Defxdoc+
- defxdoc+ extends defxdoc with some conveniences.
- Testing
- Testing new or revised XDOC strings
- Order-subtopics
- Control the ordering of subtopics in the XDOC display.
- Save-rendered-event
- Event that invokes save-rendered, supporting extra functionality
- Archive-matching-topics
- An event that saves documentation from certain events, filtered by customizable criteria.
- Archive-xdoc
- A means to save documentation from locally-included events.
- Xdoc-extend
- Extend an existing XDOC topic with additional content.
- Missing-parents
- Placeholder for documentation topics that lack :parents.
- Set-default-parents
- Set up default parents to use for xdoc.
- Defpointer
- Define an alias for a documentation topic.
- Defxdoc-raw
- Add documentation in raw mode.
- Xdoc-tests
- Topics that exist only to test XDOC functionality.
- Xdoc-prepend
- Extend an existing XDOC topic with additional content, at the front.
- Defsection-progn
- Fancy (progn ...) with a name and xdoc support.
- Gen-xdoc-for-file
- Generate xdoc using textual definitions from a .lisp file.
