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

sto...@fbk.eu

unread,

Jul 30, 2019, 12:49:23 PM7/30/19

to tlaplus

Hi,

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:

1.5.7-no-bug.png

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.

1.6.0-bug.png

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:

1.6.0-workaround.png

Best regards,

Ivan

--

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.

loki der quaeler

unread,

Jul 30, 2019, 1:08:22 PM7/30/19

to tlaplus

Hi -

Sorry about the problems you've encountered. If you remove the symbolic link, and launch the Toolbox from the command line with the same shell environment in which tlapm is on the path, is the Toolbox then able to find tlapm?

-loki

sto...@fbk.eu

unread,

Jul 31, 2019, 4:12:12 AM7/31/19

to tlaplus

Hi, also in this case the Toolbox is not able to find tlapm, I encounter the same problem:

$ echo $PATH

/home/ivstojic/bin:/usr/local/bin:/usr/bin:/bin:/usr/local/games:/usr/games:/home/ivstojic/opt/TLAPS/tlaps/bin/

$ which tlapm

/home/ivstojic/opt/TLAPS/tlaps/bin//tlapm

$ tlapm --version

1.4.3 (build 34695)

$ /home/ivstojic/opt/TLAToolbox/toolbox/toolbox

SLF4J: Class path contains multiple SLF4J bindings.

SLF4J: Found binding in [bundleresource://258.fwk1074389766:1/org/slf4j/impl/StaticLoggerBinder.class]

SLF4J: Found binding in [bundleresource://258.fwk1074389766:2/org/slf4j/impl/StaticLoggerBinder.class]

SLF4J: See http://www.slf4j.org/codes.html#multiple_bindings for an explanation.

SLF4J: Actual binding is of type [org.slf4j.helpers.NOPLoggerFactory]

(TLA+ Toolbox:10741): GLib-CRITICAL **: 10:06:17.577: g_base64_encode_step: assertion 'in != NULL' failed

(TLA+ Toolbox:10741): GLib-CRITICAL **: 10:06:17.578: g_base64_encode_step: assertion 'in != NULL' failed

(TLA+ Toolbox:10741): GLib-CRITICAL **: 10:06:17.583: g_base64_encode_step: assertion 'in != NULL' failed

(TLA+ Toolbox:10741): GLib-CRITICAL **: 10:06:17.585: g_base64_encode_step: assertion 'in != NULL' failed

(TLA+ Toolbox:10741): GLib-CRITICAL **: 10:06:17.586: g_base64_encode_step: assertion 'in != NULL' failed

(TLA+ Toolbox:10741): GLib-CRITICAL **: 10:06:17.593: g_base64_encode_step: assertion 'in != NULL' failed

(TLA+ Toolbox:10741): Gtk-CRITICAL **: 10:06:19.707: gtk_box_gadget_distribute: assertion 'size >= 0' failed in GtkScrollbar

(TLA+ Toolbox:10741): Gtk-CRITICAL **: 10:06:20.041: gtk_box_gadget_distribute: assertion 'size >= 0' failed in GtkScrollbar

$

loki der quaeler

unread,

Jul 31, 2019, 1:54:31 PM7/31/19

to tlaplus

Thank you for the reply and investigation (and thank you for posting a work around for others until we implement an improvement!)

loki der quaeler

unread,

Aug 1, 2019, 4:57:44 PM8/1/19

to tlaplus

This will be tracked at https://github.com/tlaplus/tlaplus/issues/345

Reply all

Reply to author

Forward