Skip to content
TLA+ tools for Emacs
Branch: master
Clone or download
mrc Support for PlusCal processes and stuttering states.
PlusCal processes are indented like regular begin blocks. This seems
OK but doesn't match the style of "Practical TLA+", which does not
indent code inside the process block. Might have to revisit this.
Latest commit 7942288 May 12, 2019
Type Name Latest commit message Commit time
Failed to load latest commit information.
.gitignore Initial commit Apr 26, 2019
LICENSE Initial commit Apr 26, 2019 Updated readme. Apr 29, 2019
tla-pcal-mode.el Support for PlusCal processes and stuttering states. May 12, 2019
tla-tools.el Support for PlusCal processes and stuttering states. May 12, 2019


TLA+ tools for Emacs


Compilation-mode helper

Add the source directory to load-path and M-x load tla-tools. Or just eval the buffer.

Execute M-x tla-tools-error-regexp-add to add regexps for compilation mode.

Using tla-bin, a TLA+ source file can be checked with M-x compile, with a compile command of tlc <tla-file> or pcal <tla-file> && tlc <tla-file>.


tla-pcal-mode is a mixed mode for editing TLA+ and PlusCal source files. It depends on polymode.


  • Doesn't implement much except helping next-error/previous-error.
  • No support TLC reports errors just with the module name, the filename is guessed to be modulename.tla. Sany errors don't have the module name either (makes sense, it's syntax checking the file), so it's guessed from the "Parsing file ..." line. Multiple "Parsing file" lines could lead the errors to the wrong file. As a hack, there's a super ugly regexp which prevents matching filenames beginning with "/private/", which is where the temp files go on my installation. Sorry if you need to check /tmp instead, maybe the test function offers you some inspiration.
  • Error type (warning, error) is not guessed.
  • No extra support for "-tool" option (which makes tlc emit tool-readable messages.)
  • tlc requires a config file, and this package does nothing to help generate it.
  • It would be nice if it auto reverted the buffer after pcal (which rewrites the tla file.) Until something nicer is done, I'm using auto-revert-mode. Alternatively check out tlaplus-cli-template which keeps your source clean and puts the pcal translations into a target/ directory.

Running pcal and tlc

You can’t perform that action at this time.