; XDOC Documentation System for ACL2
; Copyright (C) 2009-2015 Centaur Technology
;
; Contact:
; Centaur Technology Formal Verification Group
; 7600-C N. Capital of Texas Highway, Suite 300, Austin, TX 78731, USA.
; http://www.centtech.com/
;
; License: (An MIT/X11-style license)
;
; Permission is hereby granted, free of charge, to any person obtaining a
; copy of this software and associated documentation files (the "Software"),
; to deal in the Software without restriction, including without limitation
; the rights to use, copy, modify, merge, publish, distribute, sublicense,
; and/or sell copies of the Software, and to permit persons to whom the
; Software is furnished to do so, subject to the following conditions:
;
; The above copyright notice and this permission notice shall be included in
; all copies or substantial portions of the Software.
;
; THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
; IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
; FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
; AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
; LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
; FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
; DEALINGS IN THE SOFTWARE.
;
; Original author: Jared Davis Below we cover how to use XDOC to build manuals or document your
own @(see acl2::books). If you just want to browse the documentation, you
probably don't need to read any of this! Instead, see @(see
documentation). A good, tutorial-style introduction to XDOC can be found in: See Building the Manual under @(see acl2::books-certification) for
information on building the ACL2+Books manual. See @(see testing) for easy
instructions for how to test your XDOC strings. To use XDOC to document your own books, the first step is: This book loads very quickly and requires no ttags. It gives you @(see
defxdoc) and @(see defsection), the basic commands for adding documentation.
It also installs a new @(':doc') command, via @(see ld-keyword-aliases), so
that you can see new documentation from the terminal. 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-doc Emacs-based browser (see
acl2::acl2-doc). You can do this quite easily with XDOC's @(see save) command.
This command can be embedded in an ordinary ACL2 book, so that your manual is
automatically regenerated when you build your project. XDOC now supports @(see 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 @(see defxdoc) forms—just
add: to your @(see acl2::acl2-customization) file, or include it while you are
developing your book. Afterward, each @(see 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. This topic has no @(':parents') and is just meant to ensure that
@(see missing-parents) is working correctly. Note: @('defxdoc') is very basic. You will usually want to
use @(see defsection) or @(see std::define) instead. @('Defxdoc') is the XDOC alternative to ACL2's built-in @('defdoc')
command. General form: Example: This function is similar to ACL2's built-in
@('count') function but is more limited: The @('name') of each documentation topic must be a symbol. All of the
keyword arguments are optional: The @('short') and @('long') strings may be written using the XDOC @(see
markup) language, and may also use @(see preprocessor) commands to insert
function definitions, theorems, topic links, and so on. Many examples of using XDOC can be found throughout the ACL2 books. See for
instance the @(see acl2::std), @(see acl2::std/strings) or @(see
acl2::std/osets) libraries. XDOC just stores its documentation in an ordinary ACL2 table, so if you want
to do something like automatically generate documentation from macros, you
might decide to bypass @('defxdoc') and just manipulate the table directly. It is not possible to directly use @('defxdoc') from raw Lisp, but you can
use @(see defxdoc-raw) instead. XDOC uses an XML markup language that is similar to a subset of HTML. Note that unlike HTML,
beginning and ending tags are case-sensitive and must match exactly. As in
HTML, you must escape characters like @('<') in text to distinguish them from
tags. Various tags allow you to control the font: The @(see preprocessor) allows you to insert function definitions, theorems,
etc., from the ACL2 world. This can help you avoid having to copy and paste
definitions into your documentation, which can help to keep your documentation
up to date. But sometimes you want to write other kinds of code fragments as examples.
The raw markup options are: However, it's often better to use the preprocessor's
@@('...') and @@({...}) macros, respectively. These are nice
because they automatically escape special HTML characters like < into
< and also automatically add hyperlinks to documented functions. Whenever you include Lisp code fragments in your documentation, you should
usually keep everything indented one space to prevent Emacs problems.
For instance: GOOD -- the form is indented one space: BAD -- the form is directly on the left-margin: Without this leading space, Emacs can become confused and think that
@('(my-lisp-form ...)'), rather than @('(defxdoc foo ...)'), is the top-level
expression. This can ruin syntax highlighting and also commands like @('C-t
e') for sending s-expressions to the @('*shell*') window. Internal links between documentation topics and Emacs tags-search
links into the source code are handled by the @(see preprocessor). You can add external links to web pages with ordinary HTML-style
links, e.g., Produces a link to Centaur
Technology. XDOC's fancy web viewer now has some support for LaTeX-like mathematics.
For instance, you can write formulas such as See @(see katex-integration) for details. Documentation topics can include inline images and (via hyperlinks) can
refer to other kinds of files, like PDF files. You have to tell XDOC where to
find these files; see @(see add-resource-directory). After setting up a
suitable resource directory, you can use @('img') tags such as: to produce output such as: @(' ') tags should be put around paragraphs. @(' Bulleted and numbered lists work as in HTML. The list itself begins with
@('Starting Points
Jared Davis and Matt Kaufmann. Industrial Strength Documentation
for ACL2. ACL2 Workshop 2014. EPTCS 152. Pages 9-25.
New Features
Note for Advanced Users
Formatting Text
Displaying Source Code
') tag for longer code examples that should be indented
and \"preformatted,\" i.e., newlines and spaces should be preserved.
How to format @('
|
|') blocks
| (my-lisp-form (foo ...)
| (bar ...))
|
|
|
|(my-lisp-form (foo ...)
| (bar ...))
|
})
Hyperlinks
Typesetting Mathematics (Experimental)
Images and other Resources
Structuring Documents
@('
') creates the biggest heading
@('
') the next biggest
@('
') a medium size heading (a good default)
@('
') a smaller heading
@('
') a very small heading
@('
') can be used to create indented paragraphs like
this one. (Let's put enough text here to make it word-wrap. Mumble mumble
mumble. Mumble. Mumble mumble.)
') can be used
to write haikus and so on
but is discouraged') (for bulleted lists) or @('
') (for numbered lists). Each list
element is an @('
Produces:
You can also use definition lists, which are comprised of @('
Produces:
These framed boxes are generated with the @('
A subset of HTML tables is implemented, including @('
'), and @(' | '). To encourage portability, this is a somewhat limited
facility—you cannot control widths, padding, etc. on table cells. Here is
an example table:
It's relatively easy to add new tags. There is undocumented support for images and icons, but this is currently awkward. In the future, we may add other tags that users request. ") (defxdoc preprocessor :short "In addition to its @(see markup) language, XDOC includes a preprocessor which can be used to interpret certain directives of the form @('@(...)')." :long "Functions and TheoremsTo look up function definitions (or pieces of definitions) from the ACL2 world and insert them into your documentation, you can use:
We expect that @('def') and @('body') directives will expand to large code
fragments, so they are automatically wrapped in @(' The @('call') directive is automatically wrapped in @('') tags, i.e.,
@('@(call fib)') might become @('(fib x)'). An alternative is to use
@('@(ccall fib)'), for \"code call,\" which inserts @(' The other directives just become plain text, and you can wrap whatever formatting commands you like around them and use them inline in paragraphs, etc. Adding Examples or Code FragmentsThere is special syntax to put in raw or verbatim text. This is especially useful for examples and code fragments, where you don't want to have to escape special character like @('<') with @('<').
These have a special feature for automatically linking to documented topics. For instance, @@('(consp x)') produces @('(consp x)'), and @@({ (consp x) }) produces: @({ (consp x) })Evaluating Lisp from Doc StringsThe preprocessor has a special backtick syntax for dynamically evaluating ACL2 expressions. This can be used to inject constants and examples into your documentation. For instance:
By default, the backtick syntax introduces @('') tags and automatically
escapes any special XML characters like @('<'). Sometimes this isn't what you
want. When the result of your evaluation is large, you can use a spcial
@(':code') prefix to insert @(' (Advanced) Introducing @('') tags also doesn't work well for certain, sophisticated uses of evaluation, e.g., to generate hyperlinks, etc. The special @(':raw') prefix can be used to insert exactly the contents of a string, with no automatic escaping. For instance: @(' @(`(:raw \"a < b\")`) ') produces @(`(:raw \"a < b\")`). Note that it is quite easy to use @(':raw') incorrectly; you have to escape things properly yourself! Emacs LinksThe @('@(srclink name)') directive inserts a source-code link for users who
have configured their web browser as described in @(see emacs-links). For
documentation in the acl2-doc browser @(see acl2::acl2-doc) or at the terminal,
the name is enclosed in angle brackets (@(' It is often unnecessary to use @('srclink') directly, because these links are automatically inserted by @('@(def fn)'). One good reason to use @('srclink') is to link to macros like @(srclink defxdoc), which often are written using backquote and hence do not display nicely. Source links are sometimes inappropriate, e.g., for definitions or theorems that are generated by macros. You can suppress the automatic source links on @('def') commands by using @('@(gdef fn)') instead. This stands for \"generated definition.\" Documentation LinksThe easiest way to link between topics is to use @('@(see name)'), which expands into a link to @('name'). The text shown to the reader is just the name of the topic, in lower case. Note also that @('@(csee name)') can be used for links whose first letter should be capitalized; that @('@(tsee name)') can be used for links that should appear in type-writer font; and that @('@(see? name)') is useful for macros, since a link is inserted if @('name') is documented but otherwise @('name') simply appears in typewriter font. For most purposes, @('@(see name)') is adequate and it is also recommended. Finer-grained control (e.g., changing the link text) is also possible, but then you have to understand how file names get mangled. The basic story is that @('@(see name)') expands to: @({Where:
So, to support custom links, we provide
You can use these to write your own @('
Escaping of @Since @('@(') is intercepted by the preprocessor, you may occasionally need to escape it. You can write @('@@') to generate a single @('@') sign. Besides @('@(') and @('@@'), the preprocessor leaves any other uses of @('@') in tact. So, most uses of @('@'), such as in email addresses, do not need to be escaped. ") (defxdoc save :short "Saves the XDOC database into files for web browsers, etc." :long "Once you have documented your books with @(see 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 @(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 \"This manual explains how to use my books... \") (xdoc::save \"./mylib-manual\" :error t) ;; write the manual })Notes about this example:
General Form@({ (saveThe 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:
Option Summary
Avoiding Unwanted DocumentationBy 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 @(see acl2::std/strings) and @(see oslib::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 \"This manual explains how to use my books... \") (xdoc::save \"./mylib-manual\" :error t) })") (defxdoc save-rendered :parents (XDOC) :short "Saves the XDOC database into a file for the acl2-doc browser" :long " @({ General Form: (save-rendered outfile header topic-list-name error state) })where @('outfile') is the pathname for the output file, @('header') is to be written to the top of @('outfile') (typically as a comment), and the value of @('topic-list-name') is a symbol that can be the first argument of @(tsee defconst), hence of the form @('*c*'). The value of @('error') should be @('t') or @('nil') to indicate whether or not (respectively) to cause an error upon encountering a syntax error in xdoc source (marked by \"xdoc error\"). Upon success this call returns the error-triple @('(mv nil (value-triple :ok) state)'); probably the value is unimportant except that it allows an @('xdoc::save-rendered') call to be placed inside @('make-event'), as displayed below. For example, the following form may be found in community book
@('books/doc/top.lisp'). Its evaluation creates the output file
@('books/system/doc/rendered-doc-combined.lsp\"'). That file starts with a
comment from the string, @('*rendered-doc-combined-header*'), then contains
@('(in-package \"ACL2\")'), and concludes with a form @('(defconst
*ACL2+BOOKS-DOCUMENTATION* ' The output file is typically used by the acl2-doc Emacs-based browser for XDOC. See @(see acl2::acl2-doc), specifically the discussion of custom manuals, which explains that the @('filename') argument of Emacs function @('extend-acl2-doc-manual-alist') is exactly the output file created by @('xdoc::save-rendered'). ") (defxdoc deploying-manuals :parents (save) :short "How to distribute XDOC manuals for other people to use." :long "After you have documented your books with XDOC and created a manual, you may wish to share your manual with coworkers, collaborators, customers, sponsors, etc. The best way to do this may depend on many factors. By default, the manuals created by @(see save) use only client-side JavaScript code. This makes deployment very easy: you can just copy the files to wherever you like, and you don't even need a web server. This approach—just copying the default manual—is well-suited for:
But the default manuals will perform badly on slow connections. So, if your users are going to read the manual over, e.g., VPNs or public web sites, then you may wish to read on. Server-Supported ManualsThe basic reason that the default manuals are slow is that they work by simply loading the data for every topic, at startup. As of October 2013, this comes to around 25 MB of data for the basic @('doc/top.lisp') manual. It's no big deal to load 25 MB from a local hard drive or a fast intranet connection, but it can be quite slow over the internet. The XDOC manuals created by @('save') can be reconfigured to just load the @(':long') sections as they are accessed. This results in a much faster-loading manual, and is how, for instance, the online XDOC manual at Centaur is deployed. This option requires a small amount of configuration, and you may need to coordinate with your network administrator to get certain software installed. If you want to use our scripts directly, you will need a web server that supports Perl scripts with the CGI, DBI, and DBD::SQLite modules installed. If for some reason this poses a problem, you may find that you can easily port these scripts to other popular languages, like PHP or Ruby, with SQLite support. Step 1: Create the DatabaseIn the manual directory you created with the @(see save) command, you should find a Perl script named @('xdata2sql.pl'). When you run this script, you should see something like the following output: @({ $ cd my-library/manual $ perl xdata2sql.pl ------------------------------------------------------------------------------- xdata2sql.pl: Convert xdata.js into xdata.db (an sqlite3 database) NOTE: Most folks don't need to run this at all! If you just want to: - browse an XDOC manual on your local hard drive, or - share an XDOC manual on your fast intranet then ignore this script and just see index.html. The main use for this script is to share XDOC manuals on the internet. In this scenario, just having the web browser load in the entire (generally 20+ MB) xdata.js file is not very practical, because some users will have slow connections and will take too long to load the file. There are many ways to solve this. Our approach is to convert xdata.js into an sqlite3 database, and then use a server-side script that will allow us to access topics only as they are requested. ------------------------------------------------------------------------------- ; Converting xdata.js ; Reading file ; Checking file ; Parsing JSON data. ; Creating new xdata.db. ; Creating xdoc_data table. ; Populating xdoc_data table. ; All done. To actually use the database, see xdataget.pl. })After this step, you should have a new file named @('xdata.db') in your manual directory. This is an SQLite3 database that has the information for your XDOC topics. It should be roughly as large as @('xdata.js'). If you are missing some required Perl modules, then instead of the above output you may see a message such as @({ Can't locate DBI.pm in @INC ... })In this case, you may need to ask your systems administrator to install the missing modules. Step 2: Set up the Web ServerOnce you have created the @('xdata.db') file, you will need to copy both it and a different script, @('xdataget.pl'), to some directory in your web server. Typically, for @('xdataget.pl') to work at all, it will need to have its executable bit set, and it may need to be in a special directory within your web server, typically named @('cgi-bin'). To make sure the script is working, you should now load it in your web browser by going to, e.g., @('http://my-server/cgi-bin/xdataget.pl'). If everything is working, you should see a page that looks like this: @({ {\"results\":[ ]} })If, instead, you see a message like Internal Server Error, then you may have a permissions problem, or your web server's version of Perl may be missing a require library, or something else may be wrong; ask your systems administrator for help. You may also wish to load, e.g.,: @({ http://my-server/cgi-bin/xdataget.pl?keys=ACL2____TOP })and make sure that you can see some text from your top topic. Step 3: Configure the Manual to use the ServerThe final step is to edit the file @('config.js') in your manual. This file contains comments with the example syntax. Basically you just need to change: @({ var XDATAGET = \"\"; })To have the right URL for your xdataget.pl script, e.g., into: @({ var XDATAGET = \"http://my-server/cgi-bin/xdataget.pl\"; })At this point, your manual should load topic data dynamically as needed. The result should be much faster for users on slow connections. ") (defxdoc emacs-links :short "Instructions for integrating XDOC web pages with Emacs." :long "@(csee preprocessor) directives such as @('@(def get-xdoc-table)') result in the introduction of special links for Emacs. Here's what these links look like: @(def get-xdoc-table)Depending on your environment, it may be easy to configure your web browser so that clicking on these links will cause Emacs to directly open up the appropriate source file and jump to the named function. The basic idea is:
The net effect is that clicking on these links will send you directly to the desired function in the source code. This is really slick if you can get it working. Configuring EmacsLoading the XDOC ElispThe XDOC directory includes a file called @('xdoc.el'), which tells emacs what to do with these xdoc-link files. To tell emacs to load this file at startup, you can just add a command to your @('.emacs') file like: @({ (load \"/path/to/acl2/books/xdoc/xdoc.el\") })This file will be loaded automatically if you load the file of emacs utilities that comes with ACL2: @({ (load \"/path/to/acl2/emacs/emacs-acl2.el\") })Managing your TAGS tablesFor emacs to make sense of the links you follow, it will need to have the appropriate tags tables loaded for all of the libraries you are using. If you aren't familiar with tags, you basically just need to:
Jared's Approach:
Setting up Emacsclient (recommended)You can set things up so that links open up in new instances of Emacs, or in new buffers of an already-running Emacs. If you want everything to open up in a new instance of Emacs, you can skip this section. But I prefer to use a single Emacs for everything, and just have links open up in new buffers. This is quite easy. First, add @('(server-start)') to your @('.emacs') file and restart Emacs. Next, to ensure everything is working properly, launch a separate terminal and type: @({ emacsclient --no-wait my-file })If all is well, @('my-file') will be loaded into your already-running emacs as a new buffer. Configuring the Web BrowserThe last thing we need to do is instruct your web browser to send xdoc-link files to Emacs. How to do this depends on your web browser and/or operating system. In some cases it may be hard to pass command-line options to emacs directly, so you may find it useful to use the script @('emacsclient-wrapper.sh'), found in the xdoc directory. The basic starting point is probably to try to click on an emacs link like @(srclink append) and try to tell your browser to open it with the @('emacsclient-wrapper.sh') script. If your browser opens it with some other program, you might need to edit the default file associations of your operating system or window manager. ") (defxdoc extract-keyword-from-args :parents (defsection) ; bozo hrmn, where should this go, really? :short "Get the value for a keyword argument like @(':foo value')." :long "@(call extract-keyword-from-args) is given @('kwd'), which should be a keyword symbol, and a list of @('args') which are typically the @('&rest args') given to a macro. It scans the list of @('args'), looking for the indicated keyword, and returns @('(kwd . value)'), or @('nil') if no such keyword is found. For instance, @({ (extract-keyword-from-args :bar '(:foo 3 :bar 5 :baz 7)) --> (:bar . 5) })This function is mainly useful for writing macros that mix @('&rest') parts with keyword arguments. See also @(see throw-away-keyword-parts). @(def extract-keyword-from-args)") (defxdoc throw-away-keyword-parts :parents (defsection) ; bozo hrmn, where should this go, really? :short "Throw away any keyword arguments and their values from a macro argument list." :long "@(call throw-away-keyword-parts) is given a list of arguments that are typically the @('&rest args') given to a macro. It scans the arguments for any keyword symbols such as @(':foo'), and throws away both the keyword and the argument that follows it. For instance, @({ (throw-away-keyword-parts '(x y z :foo 3 :bar 5 blah blah blah)) --> '(x y z blah blah blah) })This function is mainly useful for writing macros that mix @('&rest') parts with keyword arguments. See also @(see extract-keyword-from-args). @(def throw-away-keyword-parts)") (defxdoc defsection :short "Fancy @('(encapsulate nil ...)') with a name and @(see xdoc) support." :long "General Form@({ (defsection name [:parents parents] [:short short] [:long long] [:autodoc autodoc] [:extension topic] ... events and commentary ...) })Example@({ (defsection foo :parents (parent1 parent2 ...) :short \"@(call foo) is like @(see bar), but better when...\" :long \"The main differences between @('foo') and @('bar') are ... \" (defund foo (x) ...) (local (in-theory (enable foo))) (defthm foo-thm1 ...) (defthm foo-thm2 ...) \"NOTE: the next theorem is really useful, but we keep it disabled because it gets too expensive when... \" (defthmd foo-thm3 ...)) })Note: this example might be better written as a @(see std::define), which is much like a @('defsection') but has additional features. OverviewLike an @(see encapsulate), a @('defsection') introduces a new scope for @(see local) events. This is often useful when you are trying to prove a theorem that requires some lemmas: by proving the lemmas locally, you can prevent them from affecting the rest of your book. It is often useful to organize books into sections. There are a few minor reasons you might prefer using @('defsection') for this, instead of plain @('encapsulate')s. For instance,
But the main reasons to use @('defsection') are its documentation features. The definitions and theorems within a section can be automatically included in the documentation page for that section, along with any running commentary. This helps to avoid copying-and-pasting code into the manual, and keeps it up-to-date as the code changes. Ordinary SectionsThe @(':parents'), @(':short'), and @(':long') keywords are optional. If any of these keywords are provided, they will be used to introduce a @(see defxdoc) command; otherwise no documentation will be generated. By default, the @(':long') string you give will be automatically extended with a \"Definitions and Theorems\" part that lists all of the (non-local, non-redundant) definitions and theorems introduced in the section. For instance, in the above example, the @(':long') field would be extended with: @({Definition and Theorems@(def foo) @(thm foo-thm1) @(thm foo-thm2)NOTE: the next theorem is really useful, but we keep it disabled because it gets too expensive when... @(thm foo-thm3) })If you do not want this automatic documentation, you can turn it off with @(':autodoc nil'). Extended SectionsThe @(':extension') keyword allows you to say that this section is a continuation of a previously introduced concept. When @(':extension topic') is provided, then @('topic') must be the name of a previously documented @(see xdoc) section, and you are not allowed to use @(':parents') or @(':short') since the topic already exists. Note that whereas topics can have multiple parents, you can only extend a single topic at a time. The main purpose of an @(':extension') section is to add additional documentation, either via the @(':long') string or via the automatic events and commentary. The documentation obtained this way is just appended onto the existing @(':long') for the topic. For example, say we have already defined the above @('foo') section in some \"basic\" book. We might then want to add some additional \"advanced\" theorems about it in some other book. We could do this via: @({ (defsection advanced-theorems-about-foo :extension foo \"Additional theorems are also available in the @('advanced') book. (We don't include these in the basic book since they take a long time to prove.) \" (defthm foo-thm4 ...) (defthm foo-thm5 ...)) })This will result in the commentary and definitions of @('foo-thm4') and @('foo-thm5') being added onto the end of the documentation for @('foo'). ") (defxdoc defsection-progn :short "Fancy @('(progn ...)') with a name and @(see xdoc) support." :long "The @('defsection-progn') macro is like @(see defsection) except that it generates @({(progn ...)}) instead of an @({(encapsulate nil ...)}) This has a number of consequences, mostly having to do with the scope of @('local') events within the section. In short, a @('defsection-progn') does not introduce a new local scope, but a @('defsection') does. ") (defxdoc undocumented :short "Placeholder for documentation topics that lack good @(':parents')." :long "Many @(see acl2::macros) such as @(see std::deflist) and other @(see acl2::std/util) macros can automatically generate @(see xdoc) documentation topics. When someone uses these macros but doesn't give any @(':parents') for the resulting documentation, we put the resulting documentation here. This seems better than just dropping the documentation completely, since at least you can at least see the boilerplate documentation and any embedded documentation that the programmer did provide. As ongoing documentation improvement work, most topics here can benefit from being given more appropriate @(':parents'). ") (defxdoc missing-parents :short "Placeholder for documentation topics that lack @(':parents')." :long "If a @(see defxdoc) form ends up having no parents, it ends up being put here. See also @(see undocumented). Historic note. We used to put these topics directly underneath @(see top) instead. But we found that during development, this sometimes led to a strange-looking hierarchy where ``random'' topics were presented as top-level topics just because they were new or being moved around or because @(see set-default-parents) forms weren't quite in the right places. To avoid this, we now move these topics to @('missing-parents') and print notes about them when a manual is saved with @(see xdoc::save). ") (defxdoc set-default-parents :short "Set up default parents to use for @(see xdoc)." :long "When documenting a book of inter-related functions, you may sometimes wish to use the same @(':parents') across many @(see defxdoc) or @(see defsection) commands. This can sometimes get tedious. The macro @(call set-default-parents) can be used to set up a default list of parent topics to be automatically used by commands such as @(see defxdoc) and @(see defsection). Basic Example: @({ (local (set-default-parents fox-p)) (defxdoc make-fox ;; use default :parents, (fox-p) :short ... :long ...) (defsection feed-fox ;; use default :parents, (fox-p) :short ... :long ...) (defsection chase-mouse ;; use explicit :parents, (fox-p mouse-p) :parents (fox-p mouse-p) :short ... :long ...) (local (set-default-parents fox-p hawk-p)) (defsection bother-hawk ;; use default :parents, (fox-p hawk-p) :short ... :long ...) (local (set-default-parents nil)) (defxdoc zebra-p ;; use default :parents, nil :short ... :long ...) })Note that @('set-default-parents') is just a macro that expands to a @(see table) event. It's good practice to only locally set the default parents—otherwise the default parents can \"leak\" from your book and lead you to inadvertently set the parents of other, unrelated topics. ") (defxdoc xdoc-extend :short "Extend an existing XDOC topic with additional content." :long "Basic example: @({ (defxdoc foo :short \"Example of xdoc-extend.\" :long \"Foo is very important. \") (xdoc::xdoc-extend foo \"Note: you can't use Foo with Bar. \") })is roughly equivalent to just writing: @({ (defxdoc foo :short \"Example of xdoc-extend.\" :long \"Foo is very important. Note: you can't use Foo with Bar. \") })@(call xdoc-extend) requires that @('name') is an existing XDOC topic, e.g., it may have been introduced with @(see defxdoc), @(see defsection), or similar. We just look up that topic and extend its @(':long') string by appending the new @('long') fragment to it. This mechanism is barbaric and fragile. For instance:
Nevertheless, judiciously used, it can be a useful tool for connecting together related content that must be kept in separate files, e.g., for bootstrapping or other reasons. ") (defxdoc xdoc-prepend :short "Extend an existing XDOC topic with additional content, at the front." :long "@(call xdoc-prepend) is very much like @(see xdoc-extend), except that it extends the @(':long') string for @('name') at the front, instead of at the back. Basic example: @({ (defxdoc foo :short \"Example of xdoc-prepend.\" :long \"Foo is very important. \") (xdoc::xdoc-prepend foo \"Never use Foo, use Bar instead! \") })is roughly equivalent to just writing: @({ (defxdoc foo :short \"Example of xdoc-prepend.\" :long \"Never use Foo, use Bar instead! Foo is very important. \") })See @(see xdoc-extend) for related commentary. ") (defxdoc order-subtopics :short "Control the ordering of subtopics in the XDOC display." :long "@(call order-subtopics) allows you to specify what order the subtopics of @('name') will be presented in. For instance: @({ (xdoc::order-subtopics mini-tutorial (example syntax semantics gotchas references)) })By default, XDOC shows subtopics in an alphabetical order. For most reference-manual material this is generally fine. But, especially for tutorial guides, you sometimes intend your topics to be read in some particular order, and alphabetizing things gets in the way. The @('order-subtopics') command lets you specify the exact subtopic ordering that should be used for a particular topic. One general form is: @({ (xdoc::order-subtopics parent (subtopic1 subtopic2 ... subtopicn)) })You don't have to give a complete order. Any subtopics that aren't mentioned will be listed last, in the usual alphabetical order. A second general form has an optional argument of @('t'). This specifies that the order for unspecified child topics is the order in which the topics were defined, rather than alphabetical. @({ (xdoc::order-subtopics parent (subtopic1 subtopic2 ... subtopicn) t) })A special case of that second general form lists no subtopics, thus specifying simply that all children are to be listed in the order in which they were defined. @({ (xdoc::order-subtopics parent nil t) })We require @('parent') to refer to some defined topic, but the subtopics don't need to be defined at @('order-subtopics') time. This makes it easy to keep the subtopic ordering close to the defxdoc command, e.g., you can write: @({ (defxdoc mini-tutorial ...)) (order-subtopics mini-tutorial (example syntax ...)) (defxdoc example ...) (defxdoc syntax ...) })We do at least warn about undefined topics when you @(see save) a manual. ") #|| (in-package "ACL2") (include-book "debug") (defconst *foo* 3) (include-book "centaur/vl/util/print" :dir :system) (defxdoc basic-test :short "Hello" :long "1 + 2 = @(`(+ 1 2)`) *foo* is @(`*foo*`) parse error is @(`(+ 1 2) (+ 2 3)`) parse error 2 is @(`(undefined::blah)`) 1 + 2 + 3 = @(`(+ 1 2 3)`) (mv 1 2 3 state) is @(`(mv 1 2 3 state)`) (mv 1 2 3 state vl::ps) is @(`(mv 1 2 3 state vl::ps)`) (repeat 'a 100) is @(`(:code (repeat 'a 100))`) ") ||# (defxdoc xdoc-tests :short "Topics that exist only to test XDOC functionality.") (local (set-default-parents xdoc-tests)) (defxdoc test-of-entities :short "Placeholder topic for testing out HTML entity support in XDOC." :long "Here are the entities that XDOC allows: Normal XML entities:
Additional entities allowed by XDOC:
Test of `single' and ``double'' smart quoting for legacy topics. Test of ‘single’ and “double” smart quoting for regular old entities. Test of `single' and ``double'' quotes in a @('') tag and in
a @(' `single' and ``double''
Test of @(' `single' and ``double'' ') quotes in inline preprocessor stuff, and in preprocessor blocks here: @({ `single' and ``double'' quotes ! })Test of primes in math: @($ foo' $) and @([ foo' ])That should probably about do it. ") (order-subtopics xdoc-tests (order-test-w order-test-o order-test-r order-test-z-intentionally-missing order-test-k order-test-s)) (defxdoc order-test-s :short "S") (defxdoc order-test-w :short "W") (defxdoc order-test-r :short "R") (defxdoc order-test-o :short "O") (defxdoc order-test-k :short "K") (defxdoc xdoc-test-order-subtopics-flg :short "Parent topic for testing chronological order of subtopics.") (order-subtopics xdoc-test-order-subtopics-flg (order-test-flg-move-to-front) t) (local (set-default-parents xdoc-test-order-subtopics-flg)) (defxdoc order-test-flg-w :short "W") (defxdoc order-test-flg-o :short "O")(defxdoc order-test-flg-o :short "O") (defxdoc order-test-flg-move-to-front :short "Move to front") (defxdoc order-test-flg-r :short "R") (defxdoc order-test-flg-k :short "K") (defxdoc order-test-flg-s :short "S") (local (set-default-parents xdoc)) (defxdoc katex-integration :short "Support for LaTeX-like typesetting of mathematics in XDOC topics. (experimental)" :long "Experimental. This whole thing is experimental. Jared reserves the right to decide it is a bad idea and remove support for it. The Khan Academy has developed a very nice Javascript library, KaTeX, for rendering mathematical formulas in the web browser. We have now integrated KaTeX into XDOC's fancy web-based viewer, allowing you to typeset basic formulas. Basic UsageTo typeset block-style formulas, you can use the @('@([...])') @(see preprocessor) directive, e.g.,: @({ @([ c = \\pm\\sqrt{a^2 + b^2} ]) })Produces an indented block of mathematics: @([ c = \\pm\\sqrt{a^2 + b^2} ])You can also write inline math using @('@($...$)') directive, for instance: @({ The product @($a \\times b$) is even. })Produces text such as: the product @($a \\times b$). Tips and TricksFast Preview.The KaTeX Preview page lets you interactively type in your formula and see how it will be typeset. It may be especially helpful since KaTeX only supports a particular subset of LaTeX. Escaping Help.LaTeX-style formulas may be especially hard to type in ordinary ACL2 string literals because you have to escape all the backslashes. For instance, you have to remember to write @('\\\\sqrt{x}') instead of @('\\sqrt{x}'). You can avoid this headache by using the @(see acl2::fancy-string-reader). Invalid Formulas.Invalid formulas will display as an ugly error message. For instance, here is an invalid @('@([ ... ])') style formula: @([ { there is no closing brace ])And here is an invalid @('@($...$)') style formula, @($ { there is no closing brace $), embedded in a paragraph. Miscellaneous NotesThe preprocessor directives expand into @(' All of this is fundamentally limited to the web-based viewer. It seems very
unlikely that @(' Examples: @({ (defpointer acl2 acl2-sedan) (defpointer guard-hints xargs t) })General Form: @({ (defpointer new-topic target-topic [keyword-p]) })This is a simple macro that expands to a @(see defxdoc) form. It introduces a new @(see xdoc) topic, @('new-topic'), that merely links to @('target-topic'). The new topic will only be listed under @(see pointers). ") (defxdoc add-resource-directory :short "Tell @(see xdoc) about directories of resources (e.g., images, PDF files, etc.) that should be copied into manuals." :long "Occasionally you may wish to include images or other files within an XDOC documentation topic. For this to work, XDOC's @(see save) command needs to know about these files so that it can copy them into the manual it produces. The @('add-resource-directory') command lets you tell XDOC which directories to copy and what to name them. ExampleSuppose that in the @('vl') library there are some images that we want to include in the manual. We can put these images into a directory, say @('images'), and then do: @({ (xdoc::add-resource-directory \"vl\" \"images\") })This will cause the @(see xdoc::save) command to copy everything from the @('images') directory into the @('res/vl') directory of our manual. To refer to these images, we can then write @(see markup) such as: @({ })These resource directories might also contain files other than images, for instance, PDF files. You can at provide hyperlinks to these files by just linking into the @('res') directory, for instance: @({ See the Slides! })General form@({ (xdoc::add-resource-directory dirname path) })
Working exampleThe directory @('books/xdoc/centaur') contains a @('centaur-logo.png') file. The file @('xdoc/topics.lisp') adds this directory as a resource directory. If all is well, you should see the logo below: ") (add-resource-directory "centaur" "centaur") (defxdoc testing :short "Testing new or revised XDOC strings" :long "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 @(tsee 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 @(see 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 @(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 @(see 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. ") (defpointer build-the-manual xdoc) |
---|