Trouble Running Toolbox on macOS Sierra

[Daniel Gregoire]

Hi everyone,

I've looked through the list and I believe my scenario is distinct from the other macOS-related problems folks have brought up.

I'm trying to use the latest TLA+ Toolbox and macOS version 10.12.6. Whether I double-click the "TLA+ Toolbox.app" or run the toolbox executable directly (at "/Applications/TLA+ Toolbox.app/Contents/MacOS/toolbox"), I see the same behavior: the TLA+ splash screen appears and the top menu populates with "File", "Window", and "Help". After the splash disappears, only the chrome of a tiny window with the minimize/maximize/close buttons appears (just big enough to house those three buttons), then the process just sits there. The actual Toolbox window never appears.

When running from the command-line, I see logging that shows the underlying Jetty server starts up, etc., but then nothing happens, no obvious errors or stack traces, it just stays put, occasionally logging about scavenging a session.

I've tried Java versions 7, 8, and 9, all of which behave as described above on my machine.

Here is the Java 8 version I'm using:

Java version:
java version "1.8.0_131"
Java(TM) SE Runtime Environment (build 1.8.0_131-b11)
Java HotSpot(TM) 64-Bit Server VM (build 25.131-b11, mixed mode)

And TLA+ Toolbox logs over stdout and stderr using that version of Java to run it: https://gist.github.com/semperos/a0709c010645fc2a5a6ba250f97e184a

Any thoughts?

Regards,
Daniel

[Markus Alexander Kuppe]

Hi Daniel,

I'm a little at loss here. Can you check if the bug persists with the
latest nightly build of the Toolbox [1]? The nightly builds use a newer
Eclipse release internally.

Thanks

Markus

[1] http://tla.msr-inria.inria.fr/tlatoolbox/ci/products/

[rap...@schindler.io]

I, too, find the TLA+ Toolbox not to work. I am on macOS High Sierra (Version 10.13). But where the OP does not even see the Toolbox window, I do see the window; however it is unresponsive: the link "Getting Started," e.g., doesn't work. The menu is also unresponsive (i.e. when the app is active, I cannot, e.g., get the 'File' menu to drop down; a click just doesn't register.)

Raphael

[Daniel Gregoire]

Markus,

Thank you! I hadn't thought to try the nightly build, it works as expected. I just tried out the SimpleProgram spec from the video course and everything runs.

I really appreciate the quick response. Yesterday I stood up a Linux VirtualBox guest on my Mac just to run the TLA+ Toolbox, this will be much more convenient :)

Regards,

Daniel

[Markus Alexander Kuppe]

On 28.09.2017 20:15, rap...@schindler.io wrote:
> I, too, find the TLA+ Toolbox not to work. I am on macOS High Sierra (Version 10.13). But where the OP does not even see the Toolbox window, I do see the window; however it is unresponsive: the link "Getting Started," e.g., doesn't work. The menu is also unresponsive (i.e. when the app is active, I cannot, e.g., get the 'File' menu to drop down; a click just doesn't register.)

Hi Raphael,

you too should try a nightly build [1]. We recently fixed a bug with a
similar description [2].

Thanks

Markus

[1] http://tla.msr-inria.inria.fr/tlatoolbox/ci/products/

[2] https://github.com/tlaplus/tlaplus/issues/74

[rap...@schindler.io]

Thank you, Markus: your suggestion to try the nightly build fixed my problem (it's version 1.5.4, to be precise).

Best,
Raphael

[daveu...@gmail.com]

I had the same issue, so then I downloaded 1.5.4 instead (nightly build). However, now I get this on launching:

An error has occurred.
See the log file
null.

Just be clear on the steps I followed:

Downloaded the 1.5.4 nightly.
Unzipped in my downloads folder.
Moved TLA+ Toolbox.app to my Applications folder.
Launched from there.

Looking inside the package, there doesn't seem to be a log file like before (I assume that's where the null comes from?)

Any advice would be greatly appreciated!

[Markus Alexander Kuppe]

Hi,

starting with 1.5.4 the .log file is locate in your user home directory
at ~/.tlaplus/.metadata/.log.

Markus

[daveu...@gmail.com]

Hi Markus

Thanks for that. I actually don't have a .tlaplus directory in my home directory. Is it automatically created?

Kind regards

Dave

[Markus Alexander Kuppe]

On 05.10.2017 23:15, daveu...@gmail.com wrote:
> Thanks for that. I actually don't have a .tlaplus directory in my home
> directory. Is it automatically created?
>

Hi Dave,

yes the directory is create automatically. Your Toolbox appears to be
seriously broken. What do you get when you launch the Toolbox from the
Terminal with:

/Applications/TLA+\ Toolbox.app/Contents/MacOS/toolbox -debug -consoleLog

Markus

[daveu...@gmail.com]

Hi Markus

I pasted the output in pastebin: https://pastebin.com/R3X0DrJi

One thing that I noticed is this line:

-vm /Library/Java/JavaVirtualMachines/jdk-9.jdk/Contents/Home/bin/../lib/server/libjvm.dylib

I read somewhere that JDK 9 will be supported by the version 1.5.4 of the toolbox, but is it worth trying to force it to JDK 8, or is there something else going on with the security exception in the trace?

Kind regards

Dave

[Markus Alexander Kuppe]

On 06.10.2017 12:15, daveu...@gmail.com wrote:
>
> I pasted the output in pastebin: https://pastebin.com/R3X0DrJi
>
> One thing that I noticed is this line:
> -vm
> /Library/Java/JavaVirtualMachines/jdk-9.jdk/Contents/Home/bin/../lib/server/libjvm.dylib
>
> I read somewhere that JDK 9 will be supported by the version 1.5.4 of
> the toolbox, but is it worth trying to force it to JDK 8, or is there
> something else going on with the security exception in the trace?

The problem could be traced back to a bad nightly build. The most recent
nightly build (10/04) does not exhibit the issue.

M.