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

Re: [tlaplus] Re: Login required for TLA toolbox?

On 07.11.2017 15:31, Alex Stangl wrote:
> I'm using MacOS 10.12.6. lamport.org does resolve to 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 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.

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+
with content:




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.




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