Apalache Documentation

The Apalache documentation is written in markdown files in the ./src directory and compiled using mdbook.

To view the documentation, visit https://apalache.informal.systems/docs/ .

Building and previewing the documentation

To build the documentation into ../target/docs, run

mdbook build

To start a server that will present a live updated view of the book while you edit, run

mdbook serve

Notes on writing the documentation

Emoji

We have hacked together support for most GitHub emoji names in the docs. So, if you write

:duck:

then, after compiling in our CI during deployment, it will render as

🦆

Our CI uses the emojitsu CLI utility. You can also use this tool to lookup the name for an emoji if you have the unicode on hand or to see how a name will render.

Note that GitHub cheats in it's rendering: it replaces emojinames with pngs, and includes some emojis which are not supported by the unicode standard. We don't stand for this standardless stuff at the moment, because it would be too tedious to implement.

The Table of Contents

The ./src/SUMMARY.md specifies the table of contents shown in the sidebar of the documentation. Any top-level chapters must be linked from there.

Each chapter must link a file: internal links to anchors within files do not work. There is an open issue to fix this behavior.

Internal documentation

Design notes and memos that are part of the documentation of our design process or for reference by developers are collected in ./internal.