Skip to content

Latest commit

 

History

History
89 lines (58 loc) · 4.1 KB

README.md

File metadata and controls

89 lines (58 loc) · 4.1 KB

TLA+ formatter

CI

temporary tla+ formatter logo

This is a formatter for the TLA+ language.

It uses tlaplus tools' SANY library to parse your specification, and it applies some (at the moment) predefined format to it.

Project Goals:

  • A formatter for the TLA+ language. Pluscal is (currently) not a priority.
  • Configurable: provide sane defaults.
  • Minimal: never add useless chars (no extra spaces or extra newlines)
  • Reliable: It should never break any spec nor change its meaning. No configuration permutation should ever lead to a broken specs.
  • Stable: Applying the formatter to the output of a previous formatter run should not change it.
  • Fast.

Configurations:

If you have specific requests for configuration options you would like to have, please consider opening an issue.

Currently, the idea is to follow the same ideas behind rustfmt. A user level formatter config and a project level formatter config.

Example

To see some examples of current reformatting, compare:

More examples are in the test/java/resources/{inputs|outputs} folders. These sources are taken from the TLA+ Examples repo.

How to run

Download the latest JAR from the Releases page, or from the artifacts section of the latest CI build.

You will need at least Java 11 (the same requirement as tlatools).

Unzip the file, and you can invoke the formatter like this:

java -jar tlaplus-formatter.jar <INFILE> [OUTFILE]

It will print your reformatted spec in output. If the optional "OUTFILE" parameter is specified, it will write the output to that file. You can use the input file as the output file as well. Run with -help parameter for the help text.

Module search paths

If your spec uses EXTENDS to reference modules that are not in the same directory (e.g., TLAPS, Community Modules, or custom libraries), you can pass their locations via the -DTLA-Library JVM system property:

java -DTLA-Library=/path/to/tlaps/library:/path/to/CommunityModules -jar tlaplus-formatter.jar MySpec.tla

Multiple paths are separated by : on Linux/macOS or ; on Windows. Standard modules (Naturals, Sequences, FiniteSets, TLC, etc.) are bundled with the formatter and do not need to be specified.

VSCode integration

The formatter is integrated into the TLA+ VSCode extension. Use the standard "Format Document" command (Shift+Alt+F) to format TLA+ files. The extension automatically passes your configured tlaplus.moduleSearchPaths to the formatter.

You can disable the formatter via the tlaplus.formatter.enabled setting.

Limitations

Because it uses SANY underneath (TLC's parser), your spec needs to first succeed SANY's parsing process; otherwise the formatter won't be able to reformat your file.

Acknowledgments

This project uses prettier4j by Opencast Software, which does the heavy lifting of implementing the Wadler-Lindig pretty-printing algorithm in Java.