Getting copilot from leanprover-community

Stream: general

[Bolton Bailey]

When I look into trying GitHub Copilot, it tells me that I can "Get Copilot from an organization" and one of the organization from which I can "Ask admin for access" is leanprover-community.

Does this mean we are paying for this / someone has given us access to Copilot? If so, is it free to add people to it?

[Scott Morrison]

No, we are not paying for it nor do we have access. (I think?)

[Alex J. Best]

If you have any form of academic affiliation you should be able to get it through github education / github campus (I think)

[Bolton Bailey]

Yeah thanks, I’m looking into that, it’s a bit of a rigamarole.

[Bolton Bailey]

Seems you have to sign up for "GitHub Global Campus", but I did that a ~few weeks ago, and now I don't know what to do to get Copilot. It seems to think all I have to do is go back to the Copilot page, but that is still asking for credit card info.

[Eric Wieser]

I think my GitHub education discount might have been inherited by the leanprover-community organization

[Kevin Buzzard]

So the moment you graduate you'll be picking up the tab for everyone's use?

[Alex J. Best]

Bolton Bailey said:

Seems you have to sign up for "GitHub Global Campus", but I did that a ~few weeks ago, and now I don't know what to do to get Copilot. It seems to think all I have to do is go back to the Copilot page, but that is still asking for credit card info.

If you just install the copilot plugin and sign in with your github account does it just work?

[Siddhartha Gadgil]

"Teachers" get it free. You have to signup for the Github classroom with verification and log in with the same account. I have used it this way for over an year now (I forget the signup details but it was fairly smooth).

It is also free for students.

[Bolton Bailey]

Alex J. Best said:

Bolton Bailey said:

Seems you have to sign up for "GitHub Global Campus", but I did that a ~few weeks ago, and now I don't know what to do to get Copilot. It seems to think all I have to do is go back to the Copilot page, but that is still asking for credit card info.

If you just install the copilot plugin and sign in with your github account does it just work?

I get "No access to GitHub Copilot found. You are currently logged in as BoltonBailey."

[Bolton Bailey]

The top of this page directs me to this page. This then tells me to apply to global campus. I can go to their site and even see the "developer pack" but I don't see copilot there.

[Bolton Bailey]

This help site seems out of date, I don't see "Sign Up for the student developer pack" or "Select Get Student Benefit" anywhere.

[Alex J. Best]

I signed up as a teacher, I did find it confusing that there wasn't copilot listed for me, but then it did start working

[Yaël Dillies]

I signed up with the Github campus thing as a student and immediately got access.

[Bolton Bailey]

Yaël Dillies said:

I signed up with the Github campus thing as a student and immediately got access.

Recently? I get the sense it's changed somehow from when they started the program.

[Bolton Bailey]

Ok weird. I went to the sign up page for copilot again today and was told I was eligible for free copilot.

[Yaël Dillies]

I did it about 11 months ago.