Zulip Chat Archive

Stream: new members

Topic: Invalid git url on natural number game


Sorin Suciu (Dec 14 2019 at 17:31):

Just FYI, I noticed on this page: https://github.com/ImperialCollegeLondon/natural_number_game
that the git url for the natural numbers game is not valid, e.g.
git clone git@github.com:ImperialCollegeLondon/natural_number_game.git is surely not valid URL (s/:/\//), I would replace it with:
git clone https://github.com/ImperialCollegeLondon/natural_number_game.git

Reid Barton (Dec 14 2019 at 17:34):

The current URL works for me, but maybe because I'm part of the leanprover-community organization?
At any rate the https URL will surely work for all

Kevin Buzzard (Dec 14 2019 at 17:39):

The natural number game has nothing to do with leanprover-community as far as I know. From the man page of git 2.17.1 on my Ubuntu machine:

GIT URLS
       In general, URLs contain information about the transport protocol, the
       address of the remote server, and the path to the repository. Depending
       on the transport protocol, some of this information may be absent.

       Git supports ssh, git, http, and https protocols (in addition, ftp, and
       ftps can be used for fetching, but this is inefficient and deprecated;
       do not use it).

       The native transport (i.e. git:// URL) does no authentication and
       should be used with caution on unsecured networks.

       The following syntaxes may be used with them:

       ·   ssh://[user@]host.xz[:port]/path/to/repo.git/

       ·   git://host.xz[:port]/path/to/repo.git/

       ·   http[s]://host.xz[:port]/path/to/repo.git/

       ·   ftp[s]://host.xz[:port]/path/to/repo.git/

@Sorin Suciu are you saying that you're using a version of git which does not accept this git protocol? The repo is public.

Reid Barton (Dec 14 2019 at 17:40):

I think it's actually the ssh protocol being used

Reid Barton (Dec 14 2019 at 17:41):

git is the user

Sorin Suciu (Dec 14 2019 at 17:46):

@Kevin Buzzard I guess you have to have git permissions to use that git URL, it works for me only using https...

Kevin Buzzard (Dec 14 2019 at 17:49):

Well I don't understand why that is but both of them work for me so I changed it to the thing which works for you as well. Thanks for pointing this out.

Johan Commelin (Dec 14 2019 at 17:50):

The difference is whether you've uploaded an ssh key to github at some point

Johan Commelin (Dec 14 2019 at 17:50):

You don't need to be part of any github organisation, but you do need an account there

Kevin Buzzard (Dec 14 2019 at 17:51):

So Sorin is correct in suggesting that I should change the installation instructions? [which I just did]

Johan Commelin (Dec 14 2019 at 17:52):

Yeah, I think it's better. Because it allows people without github account to easily clone it.

Sorin Suciu (Dec 14 2019 at 17:52):

The difference is whether you've uploaded an ssh key to github at some point

Indeed - just checked - the SSH public key I had uploaded is not present on my machine. However, I guess https would work for anyone...

Johan Commelin (Dec 14 2019 at 17:52):

People with a github account will be able to find the ssh-url if they want it

Sorin Suciu (Dec 14 2019 at 17:52):

So Sorin is correct in suggesting that I should change the installation instructions? [which I just did]

Thank you!

Johan Commelin (Dec 14 2019 at 17:53):

You only need the ssh-url version if you also want to push, and don't want to type passwords all the time

Kevin Buzzard (Dec 14 2019 at 17:53):

[like me]


Last updated: Dec 20 2023 at 11:08 UTC