Beyond the tools available through tla2tools.jar, would it also be possible to include tlapm [1] and perhaps also Apalache [2]?StephanOn 5 Apr 2026, at 23:29, Andrew Helwer <andrew...@xxxxxxxxx> wrote:I think this is a great initiative! Thank you for starting it.Personally I would like to have an all-in-one command of the form "tla <verb> <parameters>", similar to the design you proposed in the PR. The only fundamental change I would make would be unlinking the verb names from the tool names; nobody actually needs to know that the Java-based TLA+ parser is called SANY, for example. Instead, they could just run "tla parse MyFile.tla" which would invoke java tla2sany.SANY.I also don't think we should aim for 100% option coverage off the bat. It is a good idea to cover the most common 80% of use cases, which would likely be:1. Parsing TLA+2. Model-checking TLA+ using TLC in breadth-first mode3. Translating PlusCalPeople can always fall back to calling the Java tools directly if they need a specific option.AndrewOn Sun, Apr 5, 2026 at 12:46 PM Pierre-Louis Suckrow <suckro...@xxxxxxxxx> wrote: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:
- What should an official TLA+ CLI aim to cover?
- Should it simply wrap the existing Java entrypoints, or present a more unified interface?
- How much compatibility with existing command line behavior should be preserved?
- etc...
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--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/704fd11b-8830-4857-a6d6-2fe58b54b66dn%40googlegroups.com.
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUU%2B8zm6_KHPrun0Y6Rc0jnD%3DNW_4daRyVnqG8xson2MJQ%40mail.gmail.com.