VSCode Dev Containter for TLA+

By Kevin Sullivan. University of Virginia Department of Computer Science. Building with gratitude on work by many others, esp LL.

What this is

• A TLA+ development environment through VSCode, Docker, and Dev Containers
• Good enough for this Gentle Introduction to TLA+ (not mine): [https://www.youtube.com/watch?v=D_sh1nnX3zY].
• TLA+ environment based on this installer (not mine): [https://github.com/lemmy/ewd998/blob/main/.devcontainer/install.sh]
• Installed and running in a generic, official Ubuntu 22.04 container
• Tested on Windows and Intel Mac host machines.

Dependencies

• Install and run Docker Desktop if you haven't already got it running
• Install VSCode if necessary, then open a new VSCode editor process
• Get yourself a GitHub account if you don't already have one and log in
• At GitHub, fork this repository into your GitHub account (do not skip)

How to get it

• In VSCode, install the remote development extension if it's not already installed
• Use the remote-containers "Clone into container" command to clone your fork into our container
• Click in the lower right if you want to see the container build, which takes maybe 5-10 minutes.

How to start using it

• Open the test/test.tla file in VSCode.
• The files you have to start are as at the end of the video tutorial.
• Change the name of the color variable to colour. Save the file. There should be an error.
• Fix the error by undoing the change in spelling. Save. All should be well again.
• Now start the video and follow along, emptying test.tla to synch it with the start of the video.
• If you want to flag issues or suggest or contribute improvements, please use GitHub issues and send PRs.

A Video installation walk-through

Thank you to Ben for producing this video: https://www.youtube.com/watch?v=sLGY7_agg4E

Nice features (as you will see in the video)

• format and preview specifications in LaTeX
• generate and preview dot/graphviz state machine visualizations
• automatically reparse .tla files whenever they're saved
• See the .devcontainer/Dockerfile for what's being set up

To disable auto-parse on file save

• change setting from true to false in .vscode/settings.json for tlaplus

Regarding bugs and suggested repairs

• Report issues using the issues tab in this GitHub-hosted repo
• I welcome pull requests

Contact

Kevin Sullivan Department of Comp. Sci. University of Virginia [email protected]