In the admin module we currently have a bunch of users who set some form of the following in the login profile http_proxy-http://webproxy:8080. The most complete of which comes from alex (updated slightly to make use of the dns search path)
function set_proxy {
export HTTP_PROXY=http://webproxy:8080
export HTTPS_PROXY=http://webproxy:8080
export http_proxy=http://webproxy:8080
export https_proxy=http://webproxy:8080
export NO_PROXY=127.0.0.1,::1,localhost,.wmnet,.wikimedia.org,.wikipedia.org
export no_proxy=127.0.0.1,::1,localhost,.wmnet,.wikimedia.org,.wikipedia.org
}
function clear_proxy {
unset HTTP_PROXY
unset HTTPS_PROXY
unset http_proxy
unset https_proxy
unset NO_PROXY
unset no_proxy
}This ticket is to discuss if we should have this capability globally or at least every all locations required to use the proxy and if we do how should that look.
The first question to ask is What are the use cases for using the proxy manually on a production host? It possible we can fix theses use cases else where
however if we decide theses are useful for production:
do we need to add theses settings as a function so users explicitly set/unset the parameters (as above) or can we just set theses values in explicitly in /etc/profile.d/ and /etc/zsh/zshenv
If we think we should have theses as functions would it be make senses to automaticity call set_proxy on an interactive login?
Looking at this from a different side perhaps we should just add the config to the tools that most often need theses settings e.g.
http_proxy = http://webproxy:8080 https_proxy = http://webproxy:8080
I don't think curl has this option global so we would probably have to set up some global alias (which dosn't sound good)
finally i have noticed that some users add wikimedia.org to the list of no_proxy domains and some don't. Both methods work however depending on expectations one may be preferred over the other. There are likley also some edge cases for instance including wikimedia.org in the no_proxy list will me that some of the externally hosts sites e.g. https://wikitech-static.wikimedia.org wouldn't be available. however the amount of theses sites is i believe quite small and the benefit of having a direct connection may be preferred in this case?