7 unstable releases (3 breaking)
new 0.4.0 | Mar 24, 2025 |
---|---|
0.3.2 | Mar 17, 2025 |
0.2.1 | Mar 7, 2025 |
0.2.0 | Feb 26, 2025 |
0.1.0 | Feb 23, 2025 |
#92 in Development tools
795 downloads per month
700KB
3K
SLoC
tlafmt
A formatter for TLA+ specs.
It looks like this:
Add(t, k, v) == \* Using transaction t, add value v to the store under key k.
/\ t \in tx
/\ snapshotStore[t][k] = NoVal
/\ snapshotStore' = [snapshotStore EXCEPT ![t][k] = v]
/\ written' = [written EXCEPT ![t] = @ \union {k}]
/\ UNCHANGED << tx, missed, store >>
Some TLA specs are hand-crafted works of art - but not all of them - this tool is for those ugly specs!
- Optimises for easily readable output.
- Consistent formatting across different teams and authors.
- Helpful but not forceful - small tweaks, not big rewrites!
- Fast rendering - suitable for "format on save" in interactive editors.
Install
Download pre-built binaries from the releases page.
Or if you have Rust installed, compile it yourself: cargo install tlafmt
.
Usage
Format a file and print the formatted result to stdout:
% tlafmt bananas.tla
Or overwrite the input file with the formatted result:
% tlafmt --in-place bananas.tla
To check if a file is formatted and return an error if it isn't, use --check
:
% tlafmt --check bananas.tla
# Exits code 3 for unformatted code.
Check out the --help
text too.
Style
This formatter doesn't aim to enforce a prescriptive, universal style across the whole spec. Instead it aims to improve consistency by making small changes, respecting the general style of the input spec.
Formatting is being iterated on - please report any undesirable rendering as an issue.
Dependencies
~54MB
~1M SLoC