two github questions

Stream: general

[Kevin Buzzard]

1) I have a student in China who is having real problems getting Mathematics in Lean working; their Imperial VPN doesn't work because Apple has stopped supporting the system we use or something (PPTP? no clue) and they are getting timeouts with some other VPN they have. Are there any workarounds for this? I can certainly transfer files to the student via an Imperial file transfer service.
2) I have a student in the UK who wants to set up a Lean repo on github. Do they now have to set up things like ssh keys in order to pull/push? They tried to push and got an error about password authentication no longer being supported.

[Tobias Grosser]

WIth respect to 1), years ago SSH connections where still possible from china to somewhere. If that is possible, the option -D gives you a proxy that is pretty easy to use:

     -D [bind_address:]port
             Specifies a local “dynamic” application-level port forwarding.  This works by allocating a
             socket to listen to port on the local side, optionally bound to the specified
             bind_address.  Whenever a connection is made to this port, the connection is forwarded
             over the secure channel, and the application protocol is then used to determine where to
             connect to from the remote machine.  Currently the SOCKS4 and SOCKS5 protocols are sup‐
             ported, and ssh will act as a SOCKS server.  Only root can forward privileged ports.  Dy‐
             namic port forwardings can also be specified in the configuration file.

             IPv6 addresses can be specified by enclosing the address in square brackets.  Only the su‐
             peruser can forward privileged ports.  By default, the local port is bound in accordance
             with the GatewayPorts setting.  However, an explicit bind_address may be used to bind the
             connection to a specific address.  The bind_address of “localhost” indicates that the lis‐
             tening port be bound for local use only, while an empty address or ‘*’ indicates that the
             port should be available from all interfaces.

Any SSH-accessible machine either at Imperial or a free cloud node should be able to serve as SSH target.

[Tobias Grosser]

With respect to 2) I feel I heard that GH needs SSH keys.

[Scott Morrison]

If outbound ssh is allowed, and they have somewhere to ssh to (e.g. any account at Imperial), they should look into sshuttle, which works like a dream, seamlessly tunnelling all your network traffic through an ssh connection.

In particular this is much easier to use than the bare ssh -D option.

[Julian Berman]

Two other things/workarounds which may help --

for 1), they may want to check if things work via their browser perhaps. It's not going to let them pull from the repo (or treat it as a git repo in general), but if all they want is a copy they can play with, just using the "Download ZIP" may just unblock things -- i.e. https://github.com/leanprover-community/mathematics_in_lean/archive/refs/heads/master.zip

Otherwise yeah SSH SOCKS proxying is always a decent way around silly networking restrictions.

For 2) I think there's a chance that if you have the student download GitHub desktop -- https://desktop.github.com/ -- and log in through there that may obviate them from needing to learn how to generate SSH keys themselves. I definitely don't recall whether the app will automatically add the SSH key to their GH account (I suspect not :/) but yeah it may at least simplify the process. Again though not sure.

[Jireh Loreaux]

For GitHub it's not necessary to use SSH because you can just create access tokens for your account add use those.

[Notification Bot]

4 messages were moved from this topic to #new members > starting a new project by Scott Morrison.

[Matthew Ballard]

Another one to file under “if I have a computer elsewhere” is tailscale. You can set the elsewhere computer as a traffic exit node.

[Sebastian Ullrich]

The official gh CLI client also makes it simple to authenticate via the browser

[Niels Voss]

I use Git Credential Manager, which, once installed, lets you authenticate with a browser. Like Jireh Loreaux said, you can also generate a Personal Access Token here and then you would use that wherever a passwords was expected. SSH is possible to use but more difficult to set up.

[Kevin Buzzard]

Thanks a lot for all these comments! Hopefully my students can now make progress in both of these situations.