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

To view the documentation, visit https://apalache-mc.org/docs/.

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

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 its rendering: it replaces emoji names 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 ./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.

We provide a custom TLA+ syntax highlighting plugin for highlight.js in highlightjs-tlaplus.

The plugin is checked in with the source code, and you generally shouldn't need to rebuild it unless you need to make a change or update the plugin.

To build, check out the main highlight.js into a separate directory. Symlink the TLA+ language definition into the highlight.js extra directory:

$ git clone https://github.com/highlightjs/highlight.js.git
$ cd highlight.js
$ ln -s path/to/apalache/docs/highlightjs-tlaplus/ ./extra/

Next, fetch the highlight.js dependencies and build:

$ npm install
$ node ./tools/build.js -t cdn

The minified CDN distributable is now available in highlightjs-tlaplus/dist/.

For more packaging information, see the highlight.js packaging instructions.

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