Hey everyone,
After some helpful exchange with Andrew Helwer following a PR I opened to add CLI bindings to TLA+ via tla2tools.jar, I wanted to start a broader discussion about a possible roadmap for more modern command line tooling around TLA+.
I think many of us value being able to work in our preferred editor and development workflow. It would be great if that flexibility extended more fully to TLA+ as well. One thing that still feels missing to me is a simple, official way to run model checking, generate PDFs, and use related tooling directly from the CLI. It would also be valuable if such tooling were easy to install through package managers such as Homebrew.
I know that tlacli already exists, and it is a useful point of reference. Still, I found myself hesitant to adopt it on my system, especially since installing Python based tools system wide is not always ideal.
That led me to wonder why there is no official CLI entrypoint for the existing tooling. So I thought I could add it through a small PR: a thin wrapper that exposes the commands already available through tla2tools.jar, while keeping the jar itself as the source of truth. This would also allow to distribute the tooling through package managers such as Homebrew.
I also think this could be especially useful for server side or CI based TLA+ workflows.
After I opened the PR, Andrew pointed out that this is probably something worth designing more deliberately, with a more future facing and durable approach. If there is going to be an official CLI, it is worth stepping back and thinking carefully about what interaction with TLA+ tooling from the command line should look like.
So this post is meant as a starting point for that conversation.
Some questions that seem worth discussing:
I would be very interested in hearing thoughts from others, especially from people who use TLA+ outside the Toolbox, in CI environments, or through custom editor setups. The design decisions from tlacli would be also very valuable in shaping the tool.
Best,
Pierre