Automatic documentation support for svex symbolic test vectors.
Symbolic test vectors are integrated into ACL2::xdoc so that you
can generate attractive explanations of your setup. This is often useful when
communicating with logic designers.
NOTE: the topics here cover how we generate this documentation. If
you just want to document your own SVTVs, you don't need to know about any of
this—just give a :parents, :short, or :long argument to
These functions don't do much error checking. We expect that we only are
going to generate documentation after successfully processing the SVTV, so we
generally just expect things to be well-formed at this point.
The XML we generate is not documented in ACL2::xdoc's xdoc::markup, and is not supported by tools like :xdoc. How these new
tags get rendered into HTML is controlled by, e.g.,
- Top-level routine to generate a nice XML description of an STV.
- Encode a single value from an STV line.
- Encode one full line from the STV into XML for XDOC.
- Encode all the values from an STV line.
- Encode the name of an STV line.