; 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 ; topics.lisp ; ; This is the actual xdoc documentation for the xdoc system. We put the topics ; here, instead of in top.lisp, in a probably silly effort to minimize the load ; time of top.lisp. (in-package "XDOC") (include-book "top") (defxdoc xdoc :parents (documentation) :short "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." :long "

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).

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 @(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:

@({ (include-book \"xdoc/top\" :dir :system) })

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.

New Features

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:

@({ (include-book \"xdoc/debug\" :dir :system) })

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.

") (defxdoc missing-parents-test :short "A topic with no @(':parents')." :long "

This topic has no @(':parents') and is just meant to ensure that @(see missing-parents) is working correctly.

") (local (set-default-parents xdoc)) (defxdoc defxdoc :short "Add documentation to the @(see xdoc) database." :long "

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:

@({ (defxdoc name [:parents parents] [:short short] [:long long]) })

Example:

@({ (defxdoc duplicity :parents (std/lists defsort count no-duplicatesp) :short \"@(call duplicity) counts how many times the element @('a') occurs within the string @('x').\" :long \"

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.

Note for Advanced Users

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.

") (defxdoc markup :short "The XML markup language that is the basis of XDOC documentation strings." :long "

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.

Formatting Text

Various tags allow you to control the font:

Displaying Source Code

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 &lt; 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:

@({ |(defxdoc foo | :long \"

How to format @('') blocks

| |

GOOD -- the form is indented one space:

| | (my-lisp-form (foo ...) | (bar ...)) | | |

BAD -- the form is directly on the left-margin:

| |(my-lisp-form (foo ...) | (bar ...)) | })

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.

Hyperlinks

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.,

@({ Centaur Technology })

Produces a link to Centaur Technology.

Typesetting Mathematics (Experimental)

XDOC's fancy web viewer now has some support for LaTeX-like mathematics. For instance, you can write formulas such as

@([ c = \\pm\\sqrt{b^2 + a^2} ])

See @(see katex-integration) for details.

Images and other Resources

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:

Structuring Documents

@('

') creates the biggest heading

@('

') the next biggest

@('

') a medium size heading (a good default)

@('

') a smaller heading

@('
') a very small heading

@('

') tags should be put around paragraphs.

@('
') 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

Bulleted and numbered lists work as in HTML. The list itself begins with @('

    ') (for bulleted lists) or @('
      ') (for numbered lists). Each list element is an @('
    1. ') tag. For instance,

      @({
      • one
      • two
      • three
      })

      Produces:

      • one
      • two
      • three

      You can also use definition lists, which are comprised of @('

      '), @('
      '), and @('
      ') tags. For instance,

      @({
      Inputs
      x, the list we are traversing
      max, limit on how many we can accumulate
      acc, accumulator for our results
      })

      Produces:

      Inputs
      x, the list we are traversing
      max, limit on how many we can accumulate
      acc, accumulator for our results

      These framed boxes are generated with the @('') tag.

      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:

      Color Land Power Source
      White Plains Goodness, order and light, all that is richeous and holy. Adversary of evil and chaos.
      Blue Islands Air and water, knowledge and control, illusion and sleight of hand. Adversary of chaos and nature.
      Black Swamps Evil, darkness and despair, ambition and will, suffering and death. Adversary of nature and goodness.
      Red Mountains Fire and chaos, impulsiveness and fury, freedom and whimsy. Adversary of goodness and control.
      Green Forests Life and nature, growth and fertility. Adversary of control and death.

      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 Theorems

      To look up function definitions (or pieces of definitions) from the ACL2 world and insert them into your documentation, you can use:

      @('@(def fn)') insert the definition of fn
      (also works for theorems, macros, ...)
      @('@(body fn)') just the body of fn
      @('@(formals fn)') just the formals of fn
      @('@(measure fn)') just the measure of fn
      @('@(call fn)') a generic function call of fn

      We expect that @('def') and @('body') directives will expand to large code fragments, so they are automatically wrapped in @('') blocks.

      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 @('') tags instead; this could be more appropriate for functions with many arguments.

      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 Fragments

      There 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 @('<').

      • @@('...') inserts @('...') into @('') tags.
      • @@({...}) inserts @('...') into @('') tags.

      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 Strings

      The 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:

      • @('@(`(+ 1 2 3)`)') produces @(`(+ 1 2 3)`)
      • @('@(`(mv 'a 10 state)`)') produces @(`(mv 'a 10 state)`)
      • @('@(`acl2::*pkg-witness-name*`)') produces @(`acl2::*pkg-witness-name*`)

      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 @('') tags instead. For instance: @('@(`(:code (make-list 100))`)') produces:

      @(`(:code (make-list 100))`)

      (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 Links

      The @('@(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 (@('')), which essentially represent a source-code link when using the acl2-doc `@('/')' command.

      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 Links

      The 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:

      @({ printed-topic-name })

      Where:

      • @('mangled-topic-name') is a canonical, url/file-name friendly, human-hostile mangling of @('name')'s package and symbol names, and
      • @('printed-topic-name') is an XML-escaped variant of @('name'), e.g., where @('<') becomes @('<'), etc.; depending on the package of the current topic's name, it may or may not include the package portion of @('name').

      So, to support custom links, we provide

      • @('@(url name)'), which expands to @('mangled-topic-name')
      • @('@(sym name)'), which expands to @('printed-topic-name')
      • @('@(csym name)'), like @('sym'), but with the first letter capitalized

      You can use these to write your own @('') tags. You should probably never write a @('') tag yourself without using @('@(url ...)'). Some examples:

      • @('@(url defxdoc)') expands to @(url defxdoc)
      • @('@(sym defxdoc)') expands to @(sym defxdoc)
      • @('@(csym defxdoc)') expands to @(csym defxdoc)

      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:

      • 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 @(see acl2::embedded-event-form)s. 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 @(see deploying-manuals).

      General Form

      @({ (save [:redef-okp bool] ;; default is nil [:zip-p bool] ;; default is t [:logo-image path] ;; default is nil [:error bool] ;; 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.
      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 @(see 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\").

      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 @(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* ')'), where @('') is an alist representing the XDOC database.

      @({ (make-event (time$ (xdoc::save-rendered (extend-pathname (cbd) \"../system/doc/rendered-doc-combined.lsp\" state) *rendered-doc-combined-header* '*acl2+books-documentation* t ; cause error upon encountering xdoc error state))) })

      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:

      • Browsing from your local hard-drive, or
      • Browsing from a fast NFS drive or intranet server

      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 Manuals

      The 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 Database

      In 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 Server

      Once 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 Server

      The 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:

      • Each Emacs link generates a Data URIs that tells your web browser to download a new, generated file whose MIME type is @('application/x-acl2-xdoc-link').
      • You configure your web browser to send @('application/x-acl2-xdoc-link') files to Emacs.
      • You configure your Emacs to carry out a tags search instead of loading these files.

      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 Emacs

      Loading the XDOC Elisp

      The 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 tables

      For 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:

      • Occasionally generate @('TAGS') files for your libraries, using the command @('etags *.lisp') or similar.
      • Tell Emacs to \"visit\" these tags tables with @('visit-tags-table').
      Jared's Approach:
      • I add a @('TAGS') target to my Makefiles, so that when I build my library the @('etags *.lisp') command is re-run and the @('TAGS') file is kept up to date. The Makefile syntax is: @({ TAGS: $(wildcard *.lisp) etags *.lisp })
      • Then, in my @('.emacs') file, I have a series of commands like the following: @({ (ignore-errors (visit-tags-table \"/path/to/acl2/TAGS\")) (ignore-errors (visit-tags-table \"/path/to/acl2/books/xdoc/TAGS\")) (ignore-errors (visit-tags-table \"/path/to/my/stuff/TAGS\")) }) This ensures that the relevant @('TAGS') files are loaded every time I start Emacs. The use of @('ignore-errors') prevents Emacs from complaining if one of these @('TAGS') files was deleted in a \"make clean\" or similar.
      • One final addition to the @('.emacs') file is: @({ (setq tags-revert-without-query t) }) which tells Emacs to go ahead and reload these files when they are rebuilt by Make, instead of prompting you if you want to reload them.

      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 Browser

      The 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.

      Overview

      Like 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,

      • It is easier to identify in the @(':pbt') history, and
      • It indents more nicely than @('encapsulate') in a vanilla emacs.

      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 Sections

      The @(':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 Sections

      The @(':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:

      • You can't put the new content anywhere except at the end of the current @('long') string. (But see @(see xdoc-prepend) if you want to extend the beginning of a topic).
      • If you extend a topic several times in different books, the resulting text may differ depending on the particular @(see include-book) order that happens to be used.

      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:

      • @('&') becomes &
      • @('<') becomes <
      • @('>') becomes >
      • @('"') becomes "
      • @(''') becomes '

      Additional entities allowed by XDOC:

      • @(' ') becomes   (this one can be hard to see)
      • @('—') becomes —
      • @('→') becomes →
      • @('‘') becomes ‘
      • @('’') becomes ’
      • @('“') becomes “
      • @('”') becomes ”

      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 @('') tag:

      `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 Usage

      To 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 Tricks

      Fast 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 Notes

      The preprocessor directives expand into @('') and @('') tags. But you will probably want to stick to the preprocessor syntax, rather than directly using @('') tags, because if you try to use raw @('') tags then you have to remember to escape XML characters like @('<') with @('<'), which just isn't very readable.

      All of this is fundamentally limited to the web-based viewer. It seems very unlikely that @('') formulas will ever look nice when shown at the terminal with @(':doc') or in the ACL2-Doc Emacs viewer.

      ") (defxdoc defpointer :short "Define an alias for a documentation topic." :long "

      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.

      Example

      Suppose 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) })
      • dirname controls where the directory will be placed in within the manual's @('res') directory. In the example above, the @('dirname') is @('\"vl\"') so the files will be copied into @('\"res/vl\"').
      • path controls where the files will be copied from. We recommend always using a simple path such as the name of an immediate subdirectory.

      Working example

      The 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)