Struggling to follow the TLA+ Toolbox install instructions

[Michael Angelozzi]

TLA+ sounds like a great tool. I am going through the videos.

I am trying to follow the directions here on how to download and install the toolbox, on Ubuntu 20.04:

https://lamport.azurewebsites.net/tla/toolbox.html?unhideBut=hide-obtain&unhideDiv=obtain

It says:

"Below is a link to a page from which you can download the versions of the Toolbox for various systems, the name of the file indicating which system it is for.  For example,  TLAToolbox-1.4.5-linux.gtk.x86_64.zip  is for 64-bit Linux.  Please thank Microsoft and HP for the open-source release of the code by reading the following agreement."

But the github link only has 3 files:

1. tla2tools.jar
2. Source code (zip)
3. Source code (tar.gz)

The instructions say "Extract the contents of the zip file to a convenient directory.  Open the toolbox subdirectory.  You can then run the Toolbox by executing the toolbox file in that subdirectory."

So I downloaded Source code.zip, extracted it, in the toolbox folder is no "toolbox" file.

There just folders like "org.lamport.tla.toolbox". I am guessing because this the source code and not a release.

I tried downloading tla2tools.jar. I made the file executable, but when I double click on it it asks if I would like to run in with Java runtime 11, I choose yes, nothing happens.

Maybe  "Extract the contents of the zip file to a convenient directory.  Open the toolbox subdirectory.  You can then run the Toolbox by executing the toolbox file in that subdirectory." means I take "tla2tools.jar" and place it within "tlaplus-1.7.2/toolbox" and then try run it from there. Tried that but it it did not work.

Not sure how to get it working.

I seem to be theonly one struggling with these instructions that can't connect the instructions to the files.

[Rodrigo Castelan Carlson]

Hi, Michael,

You could try the zip file in the alternate download site:

https://tla.msr-inria.inria.fr/tlatoolbox/products/

Rodrigo