Check which domains 'lake' accesses?

Stream: new members

[Alex Gu]

I am working on a compute cluster that blocks some domains, preventing Lean from working. However, these domains can be whitelisted, and I am trying to figure out what they are. Is there a way to easily figure out which domains are trying to be accessed when toolchains are installing?

When I run elan -v show, I get the following, which hangs because some domain seems to be blocked. Is there a way to get this information somehow?

verbose: installing toolchain 'leanprover/lean4:v4.19.0-rc3'
verbose: toolchain directory: '/home/gua/.elan/toolchains/leanprover--lean4---v4.19.0-rc3'

And I cannot do lake -v either because it hangs as well :(

[Sebastian Ullrich]

github.com should be the only one

[Alex Gu]

Do you know if there is a way to show more logs to see what commands it is running when accessing Github? I did basic sanity checks and things like cloning repos seem to be fine

[Sebastian Ullrich]

I think you're asking for strace?