[RFC] High-level plan for documentation

[tautschnig]

[Edited version of a comment originally posted in #7005]

My opinion (and I do by no means claim to be authoritative on this, just my own thoughts):

1. Users new to verification and with a focus on the overall process start with https://model-checking.github.io/cbmc-training/.
2. If you know what verification is about, but you better want to understand the workflow with and use of CBMC, https://model-checking.github.io/cbmc-training/ has some information, but https://www.cprover.org/cprover-manual/ is likely the right place. Note that, as far as I understand, any files newly added to doc/cprover-manual still require manual intervention by @kroening.
3. If you know what tools you need to use, but need to understand all the options available with each tool, look at each tool's man page. (This is no longer an overview across tools, it's now very specific to a single tool.) The man page should be a place to document all command-line options (indeed my various recent PRs are an effort to ensure this is the case). The exception shall be options that we intentionally exclude from any kind of documentation (including --help output). That said, the man pages still are in need of love, and a lot more text is yet to be written. Only very few of them are in a shape that perhaps I'd like them to be in (Add crangler man page #6938 is somewhat close to that, as is the goto-analyzer man page that's already merged).
4. If you want to contribute to the development or understand some internals, go to http://cprover.diffblue.com/. We, however, need to fix whatever job there is to actually keep this up to date with respect to the repository (@peterschrammel ?)

The first two items might be consider a "User's Manual". Item three is a "Reference Manual." Item four would then be seen as a "Developer's Manual."

@NlightNFotis said: However, in that case, guidance should be given on where pieces of documentation like the one that we are adding now should go, given that the other folders under doc/ seem less appropriate for this piece of documentation (say, ADR/ which is for Architectural Decision Records, not user documentation, or architectural/ which is describing CBMC internals). It seems that the only other appropriate place is a new folder, which doesn't seem ideal.

I don't want us to start the discussion from where in the source tree a piece of documentation will go. I expect that discussion to start from the potential consumer of such documentation. When that is determined, we can find a suitable place in the source tree. If the audience (as I think is the case here) is a CBMC user (as opposed to a contributor/developer), then it needs to fit with the level of abstraction that is covered by a particular (collection of) document(s). If there is no so suitable collection, then perhaps we need to create a new one. But I want to make sure we don't just end up dumping text in the repository: we have a lot of documentation across the code base, but largely lack consistency. And we should aim to improve on this, not make it even worse just so that we can tick some "documentation" checkbox.

[tautschnig]

As an implementation-level note: I do wonder whether we could use GitHub pages to host some of the documentation. At present, there is the always-failing "pages build and deployment" job that I have no idea where it originates from or how to configure it.

[peterschrammel]

We have cprover.github.io which is currently unused.

[jimgrundy]

I'd like to see us move to using GitHub hosted pages including GitHub hosted Doxygen output. User and reference material is needed as well, but can we do at least this?

[martin-cs]

To me it is more important that the documentation is accessible and up-to-date (including making it as easy as possible for developers to keep it up to date) and covers both external / user and internal / developer needs, than what form it takes. I am willing to support any proposal / plan / suggestion / layout / split that achieves this.

[markrtuttle]

I'm working on a proposal to publish documentation from github.com/diffblue/cbmc to diffblue.github.io/cbmc.

The publication part is easy. If you look at my cbmc-documentation copy of cbmc, and if you look at the develop branch there, you can see a training directory and a publish.yaml workflow that runs doxygen and publishes the result to my markrtuttle.github.io/cbmc-documentation.

What is in progress is a method of moving from current documentation to the future. What I want is a menu on the left that contains

• Installation
• User guide
• Reference guide (the man pages)
• Developer guide
• cprover (which opens up to show the current doxygen documentation)
• Classes
• Namespaces
• Files

The idea is that we can move over time the documentation from under cprover up into the correct user or reference guide. Most important, people currently writing documentation have a place to hang what they write. For example, someone working on module M can in one directory put M and the user guide contribution for M and the developer guide contribution for M. And the latter two can insert themselves into the correct place in the user and developer guides.

The main problem right now is that the documentation produced by doxygen and the documentation in cprover.diffblue.com does not match, and the current documentation depends on an older version of doxygen. Differences with the latest version include some unused variables in doxyfile that are now obsolete, and 500+ new warnings of the form

cbmc/src/util/std_types.h:736: 
   warning: unable to resolve reference to 'code_typet.\ifile' for \ref command

The second main problem is that current doxygen inserts itself into the grouping in an inconsistent manner, making it hard to impose a new top-level home page in a surgical manner.

[jimgrundy]

This sounds like great progress. I guess we need to resolve the warnings, or at least have a plan for resolving the warnings (which could involve farming the work out to various people to clean up certain files), but I'm excited.

[NlightNFotis]

I really like Mark's approach on his repository, and I think this is the way forward for now - it allows us to get some documentation up quick, and allows us to iterate to start improving it.

A couple of things I have found out during my research:

1. The \ref warnings need to be examined (and fixed?) over time - they might be because of stale documentation, or because of some missing Doxygen configuration. It's not worth it in my opinion to hold the initial release of this over these warnings (what they effectively complain about is the inability to create some hyperlinks in the html output - doesn't sound that catastrophic to me).

2. Doxygen allows us to fine tune the output, by giving access to the default pages and stylesheets it creates, allowing a user to modify them.

I haven't found a way to edit the tree view in particular, but it should be somewhere there. Also worth considering the fact that Doxygen allows for hiding of some of the HTML elements (such as the treeview or the top navigation bar) so that a specific look for the page can be achieved.

I suggest as a way forward that @markrtuttle creates a PR with his changes against this repository. We can then deploy that first version, and start ironing over wrinkles such as docs locations or layout or the warnings.