High-level documentation

[sim642]

The conclusion is to use Read the Docs but documenting into docs directory of this repository in Markdown.

Ideas for tutorial-style documentation

• [x] Printing using Pretty
• [x] Tracing
• [x] Debugging using earlybird (issue #215, PR #216)
• [ ] Working with options (including --enable/--disable and --sets) and conf files
• [x] Running regression tests
• [x] Running domain tests
• [ ] Running goblint/bench benchmarks
• [x] Using HTML output
• [ ] Using witnesses and SV-COMP features (to be adapted from sv-comp directory).
• [ ] Using GobPie and the abstract debugger.
• [ ] How to implement and run an analysis using constants.ml?
• [ ] Overview of domain functors to avoid duplication (tuple, map, set, reverse, chain, etc.)
• [ ] Overview of the solvers and their advantages and drawbacks
• [x] C-Reduce
• [ ] Working with OPAM: upgrading (single) dependencies, pinning, applying pinned state, etc.
• [x] Developing goblint/cil locally and immediately using for Goblint.
• [ ] Using our Makefile support (via cilly)

• [ ] Developing using VS Code

I've been thinking about this for a while that Goblint has no high-level documentation that describes its overall structure and functioning. Some parts of the source code are commented (and few have OCaml documentation comments) but neither is useful for users and new developers, because you already have to know where to find something or which terms to grep for.

Possible platforms

1. GitHub Wiki.
   • Pro: Accessible right here on GitHub with this repository.
   • Pro: Uses Markdown (among other possibilities).
   • Con: No good organization and structuring.
   • Con: Separate from git repository (has its own git repository under the hood though, but the GitHub website hardly exposes the git functionality of it).
   • Con: No search.
2. GitHub repository Markdown files.
   • Pro: In the same repository, e.g. in a docs directory.
   • Pro: Rendered on GitHub website.
   • Con: Maybe not the nicest interface for browsing.
   • Con: Poor GitHub search.
3. OCaml documentation (odoc).
   • Pro: Together with source code.
   • Con: Uses obscure OCaml documentation markup language. Probably difficult to integrate any figures etc.
   • Con: Meant to just document public API of a library (only works now because goblint-lib is separated as a Dune library, Dune executables simply cannot have documentation).
   • Con: Organization isn't super flexible? Our unqualified module access means it's just a long list of modules.
   • Con: Must be hosted, although GitHub Pages would work.
   • Con: No search (?).
4. GitBook.
   • Pro: Uses Markdown.
   • Pro: Looks modern and easy to use.
   • Pro: Search.
   • Con: Vendor lock-in.
   • Con: Has its own proprietary (and ironically undocumented?) Markdown flavor. Lots of rich content features that aren't in any common Markdown.
   • Con: Heavily centered around its own editing environment, which includes version control and commenting off-GitHub, but can sync with it.
5. Readthedocs.
   • Pro: Uses Markdown (or preferrably reStructuredText).
   • Pro: Search.
   • Pro: No vendor lock-in.
   • Pro: Simple one way publishing process: editing etc just happens normally, the documentation files are just rendered for browsing.
   • Con: Community version apparently has advertising. Some can apparently be opted out from.
6. ...?

[sim642]

I see @michael-schwarz has just started documenting something for the SAS21 artifact (https://github.com/goblint/analyzer/tree/sas21_artifact_description), but we should probably have a broader strategy for this.

[ivanazuzic]

I strongly support the idea of documenting Goblint. :) I definitely want to help with this. We should pick the strategy that looks modern, is creates documentation that is easy to look through (well structured) and at the same time not causing use too much overhead to write and maintain. GitBook seems to me like a good solution.

[michael-schwarz]

I see @michael-schwarz has just started documenting something for the SAS21 artifact

Yes, we need to provide with the artifact a description of how to reproduce our results (for Validated badge) and a description of the structure of the source code and how to extend it (for the Extensible badge).

---

Generally, the goal to provide comprehensive documentation of Goblint is very laudable, but I fear that goal is very ambitious and we will fall short of it and our documentation will become out-of-sync with the code very soon.

Maybe something more realistic to aim for is the following three things:

• Providing a tutorial for Goblint (similar to what Zach Anderson did for CIL), that should not get outdated as fast as comprehensive documentation. This document could be split into Using Goblint and an Extending Goblint sections and would e.g. serve as the starting point for students.

• Equip every analysis with a description function unit -> string that returns a string describing what it does that is printed for all registered analyses when running goblint -h.

• Try to be more strict with ourselves when it comes to naming variables and modules and structuring our code so it becomes self-documenting

[sim642]

Of course there's no point in writing massive documentation just for the sake of it when it's too much to keep up to date, but the tutorial-like use case is probably the reasonable thing I had in mind anyway. And it would be good to have a well-defined place where to keep the code structure description that we need for the artifact, so we're not practically throwing it away.

It's just that if there's no clear place for such documentation, it's absolutely sure that nobody will document such things. Such "Extending Goblint" section would also be a good place for all kinds of utility things, like a very short overview of how to use Pretty.printf and all the Printable.pretty functions instead of writing print_endline stuff from scratch. There's a learning curve to some of these things, but no clear place to document them in the code if you already don't know about Cil.Pretty and where to find its API documentation, for example.

[michael-schwarz]

One should also document:

• Tracing
• Debugging
• Printing

[sim642]

I added these ideas into the issue itself, to have a nice TODO list at the top. If any others come about, feel free to edit the issue to extend the list.

[sim642]

I decided to set up Read the Docs now because it's actually quite unintrusive: all the documentation is based on the contents of the ./docs directory and can also be browsed on GitHub directly.

I also wrote up a bunch of the ideas collected in this issue.