Page MenuHomePhabricator

Set up https://github.com/mediawiki/core mirror
Closed, ResolvedPublic

Description

Branching off from bug 35497, which is about setting up an easy-as-possible pull-request link to Gerrit once the mirror is set up


Version: unspecified
Severity: normal

Details

Reference
bz38196

Event Timeline

bzimport raised the priority of this task from to Needs Triage.Nov 22 2014, 12:57 AM
bzimport added a project: Gerrit.
bzimport set Reference to bz38196.
bzimport added a subscriber: Unknown Object (MLST).

(Cite bug 35497 comment #13)

So, some ideas:

  • Don't use github.com/mediawiki/core as name
    • means we duplicate user groups/rights with the org "Wikimania" at github
    • means we're going to promote ourselves as "core". e.g.

github.com/Krinkle/core.

  • any advantages? hashar mentioned we want to be able to allow volunteers to help out with the

handling of pull-request and that to grant them rights we'd want to have it
outside the @wikimedia organization. However this is not needed because:

  • github allows collaboration without any rights at all. You can leave

inline comments, and stuff on any pull request anywhere

  • as in comment 12, they are pull-able in many different formats including

plain "git pull" so anyone can pull it locally, and if they have a labs ldap
account they can also push straight to gerrit for review.

  • github supports auto-closing of pull-requests when the commit hash is

pushed into the repo, so no maintenance there either. And if the commit has to
be amended, including "fixes GH-123" or "closes GH-123" will also close the
relevant PR as soon as it is merged. And if all else fails, a repo collab in
@wikimedia (of which there are many[1]) can just push "Close" manually on
github

So volunteers have complete access without needing to be manually added to

anything, this is what made GitHub works. And if its only about closing some
exceptional ones, then I'm sure we'll manage that.

  • Use github.com/wikimedia/mediawiki-core
    • ideally we'd have some kind of auto-push from gerrit or jenkins, otherwise

just set up a 30 minute cron somewhere to pull gerrit -f and `push github
-f`.

  • admin settings: pull-request: true, issues: false, wiki: false

[1] https://github.com/wikimedia

How is this not a duplicate of bug 35429? I'll be doing all the repos at once when I setup replication, not one-by-one.

(In reply to comment #2)

How is this not a duplicate of bug 35429? I'll be doing all the repos at once
when I setup replication, not one-by-one.

I didn't say it wasn't a dupe. But since it appears there is no clarity yet on how the gerrit or jenkins replication is going, I figured we may be able to set up at least something on the short term for mediawiki-core so that its out there and we can start experimenting with how to solve other issues such as what and if we need a tool for pulling in pull-requests (or that git pull github.com...; git push gerrit HEAD:refs/for/master/gh-123/some-feature; is sufficient).

I mean.. I could just ask for the repo and set a cron up to mirror and get it going. Seems low hanging fruit. But if bug 35429 can be done within say 2 weeks, then by all means dupe it.