[Proposal] Improve doc and code links in doc

[bendyarm]

💥 Proposal

Improve documentation links and code links in xdoc. How do we want them to look?

I see this proposal as a place we can discuss the issues and when there is some consensus we can improve the doc.

If you would prefer to let me know your opinions by a DM (Zulip, etc.) that is also fine.

Background

In xdoc, if the doc was defined in a community book, under the topic there is currently a code link. For example, for the doc for dm::primep the code link text looks like

kestrel/number-theory/primep-def-doc.lisp :DIR :SYSTEM

and the link target looks like

https://github.com/acl2/acl2/tree/master/books/kestrel/number-theory/primep-def-doc.lisp

There have been some requests for making the link text into an include-book form that you could cut and paste into your program. One problem with that is that the current source file link goes to the source of the xdoc, not necessarily the source of the code. Including that source file with include-book will not bring in the definition in the documentation, and so it could be considered a documentation bug.

Considerations and Objectives

There are three main ways to read the doc:

1. web interface
2. :doc at the ACL2 command line
3. m-x acl2-doc in Emacs

The kinds of link targets are currently:

• no link target available (xdoc defined interactively)
• containing file was a system community book; the link text adds :DIR :SYSTEM to the relative filename
• containing file was in a project directory in the sense of project-dir-alist; the link text adds :DIR <project-dir> to the relative filename
• containing file was somewhere else; the link text passes through the file name unchanged and does not add a link target (if the developer wants a link target, they can define a project; see :doc project-dir-alist.

Some design principles:

• make the defaults convenient for most developers
• allow developers to override the defaults
• make it clear to users what the links are for

Questions

Are there more xdoc topics documenting definitions where (A) the xdoc is defined in the same source file as the
definition being documented, or (B) the xdoc is defined in a different source file than the definition being documented?

Proposal 1

• First, change the source link text by prefixing it with "doc source: ". This makes the current behavior more clear.
• Add a feature to xdoc-carrying definitions where the developer can add a separate "code source: " link. It could be called :code-source, and would be relative to the same system/project as the xdoc source file. (*). We could also allow :code-source :none to mean there is no source code to link to.
• Make a list of places where the xdoc describes a definition that is in a different source file, and encourage the owners to add "code source: " links, or make PRs for them to review.
  (*) I think it is not necessary to allow cross-project xdoc-source/code-source files. If an xdoc really wants to talk about a definition in another project, it can do that in the body of the xdoc.
• Once all those PRs are in, I think it would be reasonable to make a change to how the links are displayed. If there is no :code-source defined, we could now presume the code is in the same file as the xdoc, and the sole link in the rendered doc could be preceded with source: instead of doc source:.
• Note that this proposal does not add the include-book form. There are a few possibilities that we can consider later but I think they need the additional information from this change.

[MattKaufmann]

Here are some comments.

(1) Regarding the first bullet in Proposal 1:

... change the source link text by prefixing it with "doc source: ".

Just to be explicit (this might not be news), that's close to what acl2-doc currently does (but not :doc at the terminal or web-based xdoc).

(2) The :code-source proposal seems reasonable to me in principle. A first step might be to find all books named *-doc.lisp and, for many of them, add such a :code-source marking (example: books/kestrel/apt/casesplit-doc.lisp). But some such files call xdoc::archive-matching-topics (example: books/centaur/aig/top-doc.lisp); I haven't thought about what would be involved there. My own view is that it's only worth undertaking this :code-source project if either most owners respond to an "encourage the owners" prod as in bullet 3 of Proposal 1, or else a volunteer (@bendyarm ?) takes responsibility for doing most of the :code-source marking, or some good combination of the two.

(3) I don't want to be involved in this project personally. Although I have at times messed with xdoc display code, I don't recall it and I have plenty to do pertaining to the ACL2 system (which does not include xdoc). So please remove me as an assignee. I can live with whatever the community decides on this, provided it doesn't break anything for :doc at the terminal or meta-x acl2-doc.

[MattKaufmann]

It occurs to me that finding the code source can probably be found using the book-of-event utility defined in books/kestrel/utilities/book-of-event.lisp. So maybe the process of generating :code-source could be automated, by using book-of-event somehow in books/doc/top below its include-book forms.

[MattKaufmann]

P.S. Oh, sorry, only some of the code source can be found using book-of-event in books/doc/top below its include-book forms, since often the code being documented is actually not included in books/doc/top. But much of that code-source info could be generated after including books/top, I think.

[ericwhitmansmith]

I think this proposal is very good, and I'm willing to add :code-source links for doc topics I've created (and perhaps for some other topics, such as those whose authors are no longer active in the community). Having the code source will allow us to generate the right include-book forms right in the xdoc, which will be very helpful to users of the documented libraries/tools/functions.

[ericwhitmansmith]

An easy first step could be to have defxdoc accept the :code-source keyword, even if the info supplied is ignored until we decide how to use it. This would let us start adding the info.

[ericwhitmansmith]

Taking Matt's example of casesplit, here's how the doc topic could look on the web (imagine it has the usual nice fonts, headings, etc):

"Casesplit
Code: (include-book "kestrel/apt/casesplit" :dir :system)
Doc: (include-book "kestrel/apt/casesplit-doc" :dir :system)

APT case splitting transformation: rephrase a function definition by cases.

...rest of the doc topic..."

Here both of the include-books would be clickable links to the corresponding files in github master.

[acoglio]

I think this is a good proposal, and I'd be happy to add :code-source information to XDOC topics that don't reside in the same file as the code they document.

[solswords]

This seems fine to me.

[bendyarm]

I really meant the "assigning" as "reviewing" but they don't have a "reviewing" list for proposals (at least not by default), so I removed the "assignments". Thanks for everyone's reviews!

[bendyarm]

PR #1459 implements the first part of this.