[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] BUG: Can not use TLAPS in TLA+ Toolbox 1.6.0 when TLAPS installed in ~/opt


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
    $ 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,

Le informazioni contenute nella presente comunicazione sono di natura privata e come tali sono da considerarsi riservate ed indirizzate esclusivamente ai destinatari indicati e per le finalità strettamente legate al relativo contenuto. Se avete ricevuto questo messaggio per errore, vi preghiamo di eliminarlo e di inviare una comunicazione all’indirizzo e-mail del mittente.
The information transmitted is intended only for the person or entity to which it is addressed and may contain confidential and/or privileged material. If you received this in error, please contact the sender and delete the material.

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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/3b25dc30-c9e5-46e8-93da-61e8ef76a43c%40googlegroups.com.