Recently I updated TLA+ Toolbox from 1.5.7 to 1.6.0 (thank you for the new version!). Both the Toolbox and TLAPS are installed in ~/opt. I can no longer use TLAPS from the Toolbox. The workaround is to place a symbolic link to tlapm in /usr/local/bin. Please find below more details.
My OS is Debian GNU/Linux 10 (buster), version 10.0
Description of the installation of TLA+ Toolbox and TLAPS:
- TLA+ Toolbox is installed in /home/ivstojic/opt/TLAToolbox/toolbox.
- TLAPS is installed in /home/ivstojic/opt/TLAPS/tlaps.
- /home/ivstojic/opt/TLAPS/tlaps/bin/ is in the PATH
- Running tlapm from the command line works fine:
$ which tlapm
/home/ivstojic/opt/TLAPS/tlaps/bin/tlapm
$ tlapm --version
1.4.3 (build 34695)
With the above setup, running TLAPS from TLA+ Toolbox 1.5.7 works fine:
However, with the same setup, in TLA+ Toolbox 1.6.0, the TLAPS menu entries are disabled (in the following screenshot, note that the top three submenu items are disabled, while e.g. "Focus on step" is enabled) and the keyboard shortcuts (e.g. Ctrl-g Ctrl-g) do not work. It is therefore not possible to use TLAPS from the TLA+ Toolbox.
I was able to work around this bug by creating a symbolic link /usr/local/bin/tlapm -> /home/ivstojic/opt/TLAPS/tlaps/bin/tlapm. With this symbolic link in place, in TLA+ Toolbox 1.6.0 the TLAPS menu entries and the keyboard shortcuts work as expected:
Best regards,
Ivan