New to TLA+ Trying to install 1.7.3 from Github

[Andrew Frances]

Hi Folks:

I am new to TLA+. I don't do much Java these days. I downloaded 1.7.3 and untarred it. I looked at the Linux instructions. I have looked at the Read.me. I cannot seem to find instructions on stuff like setting up the classpath. How do I run the toolbox? Any help would be appreciated. Also perhaps I can help update the Linux instructions?

Thank you,

Andrew

[Jones Martins]

Hi Andrew,

The latest TLA+ release is available here: https://github.com/tlaplus/tlaplus/releases/latest

This release page says the latest TLA+ Toolbox is available here: https://github.com/tlaplus/tlaplus/releases/tag/v1.7.1#latest-tla-files

Since you're on Linux, I'd recommend you install the Toolbox through the .deb file. That's how I did it haha

If you can't install the Toolbox through the .deb file:

- Download the TLAToolbox .zip file,

- Extract the toolbox directory, and either:

   - Add this directory to your PATH variable or

   - Create a symlink in some directory that belongs to your PATH variable, maybe ~/.local/bin.

I can also recommend you use tla-bin to download and install the most recent TLC version, and add a tlc command to your command line. This is their URL with further documentation: https://github.com/pmer/tla-bin

As an alternative to the TLA+ Toolbox, you might also like the VSCode TLA+ extension.

Best,

Jones

[Andrew Frances]

Hi Jones:

Thanks for the advice. I'll install the .deb if all other means fail.

>Add this directory to your PATH variable or

>  - Create a symlink in some directory that belongs to your PATH variable, maybe ~/.local/bin.

There is no CLASSPATH involved?

Which file(s) are the executable binaries? I am looking at the /tlaplus-1.7.3/toolbox directory.

Cheers,

Andrew

--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/x8seO38f2mk/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/7b52b3f3-97f1-4926-a244-d2e76a860742n%40googlegroups.com.

[Jones Martins]

The executable binary is toolbox inside the toolbox/ directory.

I just ran it on my computer and everything works as usual, but I didn't go further and add toolbox to my PATH because I had already installed it with the .deb file.

I never had to configure a CLASSPATH, either.

Best,

Jones

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CANYrJ%3DQrCLiY-OsOxXesPyW3Ox1i7ZAg9gNKb82Zub3xq7xkfA%40mail.gmail.com.