		Search-engine friendly clone of the ACL2 documentation.

Xdoc

Testing

Testing new or revised XDOC strings

Contributors to the XDOC manual should check that their XDOC strings are well-formed. This topic shows an easy way to check well-formedness of XDOC strings, without the need to build the manual. Also discussed is a way to check for the absence of broken links by building the manual.

To test a topic, first submit a suitable in-package form if necessary, and then to test your topic named, say, FOO:

(include-book "xdoc/top" :dir :system)
(defxdoc ...) ; or whatever form you have that includes an XDOC string
:doc foo ; a bit noisy and slow the first time, but could do this twice

The output should be free of obvious errors. Otherwise, you can use the error message to debug the error; then submit your form and :doc foo again.

A XDOC feature (the second ``NEW'' feature in the xdoc documentation) avoids the need to invoke :doc explicitly. In brief: you can simply include community-book xdoc/debug, for example by putting its include-book form in your acl2-customization file (see ACL2::ACL2-customization).

Checking for broken links requires you to build the manual; for instructions, see the section ``Building the manual'' in the topic ACL2::books-certification. This build will create a file books/doc/top.cert.out. Search in that file for the word ``broken'' and you will find the following report of a broken link:

;;; ACL2____SOME-BROKEN-LINK:
;;;    from ACL2-DOC

If any other broken links are reported, you can modify the parent topic (e.g., ACL2-DOC just above — but please leave that one in place!) to fix the indicated broken link.

The :short and :long strings, if supplied, must consist entirely of standard characters (see standard-char-p), except that tabs are also allowed. Making this check requires you to build the manual (as described just above).