CBMC documentation campaign #1090
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
* The existing HTML documentation under doc/html-manual has been converted to Markdown. This was done automatically using Pandoc, plus some manual work to give identifiers to sections and changing internal links to point to those sections with \ref. * The Doxygen front page now contains some content: a link to the doxygen-ated HTML manual, and a note about the API documentation. The intention here is that the entire Doxygen site could be hosted publicly, serving both users of and contributors to CBMC from a single site. * The doxyfile is updated to enable these changes.
Doxygen module groups that did not contain any documentation are removed from the codebase. There are still a few module groups remaining, which do contain useful content. This commit declutters the Doxygen Modules section in preparation for a commit introducing per-directory module documentation.
This commit introduces a module.md file for several CProver directories. Each of these is turned into a page under the Modules section in the generated Doxygen documentation. The intention is that developers wishing to contribute to one specific aspect of CProver can get a high-level architectural overview of a particular directory; the documentation describes the input to and output from that directory, and introduces the main classes or entry points. By way of a "table of contents," the file cbmc/module.md contains a diagram describing how each of the directories is invoked by CBMC in order, and the nodes of the diagram hyperlink to the appropriate documentation. The intention is that developers wishing to contribute to CBMC as a whole can understand the entire process, from source files to bug reports and counterexample production. This documentation is derived from Mark Tuttle's notes on a talk given by Michael Tautschnig.
A practical tutorial on getting started with CProver development is added and linked to from the front page. The tutorial contains an overview of the codebase and a few preliminary programming exercises, intended to give would-be CProver contributors an introduction to the key data structures used throughout the codebase.
The CBMC Guide (previously a TeX file) is now part of the Doxygen codebase.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This patchset adds new material to the Doxygen documentation, and converts CProver's existing HTML manual into markdown so that it's also part of the Doxygen documentation. Reviewers can view the generated docs here: http://karkhaz.com/tmp/html/
The main things to note are:
The intention is that, given that we're now using Doxygen heavily (per #869), why not have all of CBMC's documentation in the same place---to ensure that it is always up-to-date, and to allow hosting both API documentation, user tutorials, and architectural documentation in a single place. It also allows easy hyperlinking between higher-level documentation and the appropriate API docs, and the Doxygen tool itself can warn about when the links go stale.
There is scope for moving stuff around, moving some of the documentation into the appropriate .h files instead of having them at the directory top-level, etc. But I'm hoping that this patchset is the first step in this process; in particular, it establishes where the documentation lives and the conventions for how the markdown files are organised.
Big thanks to Michael Tautschnig for the lectures from which the CBMC tour is based on, and Mark R Tuttle for taking notes on all of this.