High-level documentation

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

Ideas for tutorial-style documentation

• Printing using Pretty
• Tracing
• Debugging using earlybird (issue #215, PR #216)
• Working with options (including --enable/--disable and --sets) and conf files
• Running regression tests
• Running domain tests
• Running goblint/bench benchmarks
• 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
• C-Reduce
• Working with OPAM: upgrading (single) dependencies, pinning, applying pinned state, etc.
• 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. ...?