Invalid git url on natural number game

Stream: new members

[Sorin Suciu]

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]

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]

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]

I think it's actually the ssh protocol being used

[Reid Barton]

git is the user

[Sorin Suciu]

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

[Kevin Buzzard]

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]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Johan Commelin]

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

[Sorin Suciu]

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]

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

[Sorin Suciu]

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

Thank you!

[Johan Commelin]

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]

[like me]