Login required for TLA toolbox?

[Alex Stangl]

Hi. I recently installed the TLA Toolbox on a Mac. It kept complaining about JVM versions although I have 4 different JVMs installed, including 1.8, and in fact 1.8 is my default. Eclipse apparently thinks otherwise. I managed to override it with -vm argument in toolbox.ini and got past the JVM incompatibility dialog. 

 

But then a Login required dialog pops up, requesting username/password for lamport.org. I didn't see this mentioned anywhere, in the help, in the GitHub issues, in Bugzilla, in Google searches, etc. I also didn't see anywhere on the site to sign up for a login. Despite the dialog box title "Login Required", is this something I could/should just click Cancel and can proceed without actually logging in?

I emailed Leslie Lamport about this, and he suggested I ask on this group.

Thanks!

Alex

 

[Markus Alexander Kuppe]

On 06.11.2017 16:38, Alex Stangl wrote:
> Hi. I recently installed the TLA Toolbox on a Mac. It kept
> complaining about JVM versions although I have 4 different JVMs
> installed, including 1.8, and in fact 1.8 is my default. Eclipse
> apparently thinks otherwise. I managed to override it with -vm
> argument in toolbox.ini and got past the JVM incompatibility dialog.
>
>
>
> But then a Login required dialog pops up, requesting
> username/password for lamport.org. I didn't see this mentioned
> anywhere, in the help, in the GitHub issues, in Bugzilla, in Google
> searches, etc. I also didn't see anywhere on the site to sign up for
> a login. Despite the dialog box title "Login Required", is this
> something I could/should just click Cancel and can proceed without
> actually logging in?

Hi Alex,

the login dialog that you describe shouldn't come up. If you are still
able to reproduce it, can you send me a screenshot (privately)? Please
also let me know if lamport.org resolves to 205.233.73.65 on your
machine. Do you normally have to configure a proxy server in System
Preferences or in your browser?


With regards to the JVM selection on macOS, I'm unfortunately not aware
of anything better than setting the "-vm" parameter (if one has multiple
JVMs).

Thanks
Markus

[loki der quaeler]

Hi - that is very odd.  Which version of Mac OS are you running?

Can you attach a screenshot of the login panel?

Is it still occurring? There are assets in that domain (e.g an update site), but none should require credentials; if it's not still occurring, perhaps somehow temporarily there was directory access restriction in place.

-loki

[Alex Stangl]

I'm using MacOS 10.12.6. lamport.org does resolve to 205.233.73.65 for me. I don't use a proxy server in the browser, but at work our requests do go through ForcePoint. TLA Toolbox seems to start up OK for me at home, but comes up with the login when I try to run it from work. (Screenshot attached.) 

Using Wireshark, I see an HTTP GET to 205.233.73.65 for /tlatoolbox/toolboxUpdate/p2.index, which gets an HTTP 307 Authentication Required response. When I make the same request from a browser I get an HTTP 302 redirect to http://tla.msr-inria.inria.fr/tlatoolbox/toolboxUpdate/p2.index, which works. Strange...  seems like ForcePoint is messing it up somehow, but not sure why it works OK from the browser, unless ForcePoint is varying its behavior based on the User-Agent header or something like that.

 

Thanks!

Alex

[Markus Alexander Kuppe]

Hi Alex,

my assumption is that your browser (macOS) auto-configures itself to use
Forcepoint (e.g. via [1]). The Toolbox on the other hand fails to
configure itself and thus shows the login dialog when it tries to access
the network (when checking for updates).

Unfortunately, the Toolbox does not include the preference page to
manually configure proxies (which is part of the Eclipse SDK). I opened
an issue [2] to address this problem.


Temporarily you can try to create a file called /Applications/TLA+
Toolbox.app/Contents/Eclipse/configuration/.settings/org.eclipse.core.net.prefs
with content:

eclipse.preferences.version=1

org.eclipse.core.net.hasMigrated=true

systemProxiesEnabled=true

That might convince the Toolbox to use your system's proxy servers. I
couldn't test this though.


You can also just ignore the dialog at set the Toolbox to skip the
update check. That's done via TLA+ Preferences > Preferences... > 
Automatic Update and uncheck "Automatically find new updates and notify
me". You then have to manually install the next Toolbox release from the
zip file once it's out in a few month.

Thanks

Markus

[1]
https://www.websense.com/content/support/library/web/hosted/getting_started/endpoint_mac_os.aspx

[2] https://www.forcepoint.com/

[Markus Alexander Kuppe]

On 07.11.2017 17:16, Markus Alexander Kuppe wrote:
> Unfortunately, the Toolbox does not include the preference page to
> manually configure proxies (which is part of the Eclipse SDK). I opened
> an issue [2] to address this problem.

Hi Alex,

the most recent nightly build [1] includes the proxy preference page.
You might want to give it a try.

Thanks

Markus

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

[Alex Stangl]

Hi Markus,

The most recent nightly build seems to clear up the problem with that dialog box popping up. Thanks!

Alex