{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/6919","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/6919/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/6919/comments","events_url":"https://api.github.com/repos/coq/coq/issues/6919/events","html_url":"https://github.com/coq/coq/issues/6919","id":302410396,"number":6919,"title":"[CI] Meta-Issue for Gitlab migration","user":{"login":"ejgallego","id":7192257,"avatar_url":"https://avatars2.githubusercontent.com/u/7192257?v=4","gravatar_id":"","url":"https://api.github.com/users/ejgallego","html_url":"https://github.com/ejgallego","followers_url":"https://api.github.com/users/ejgallego/followers","following_url":"https://api.github.com/users/ejgallego/following{/other_user}","gists_url":"https://api.github.com/users/ejgallego/gists{/gist_id}","starred_url":"https://api.github.com/users/ejgallego/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ejgallego/subscriptions","organizations_url":"https://api.github.com/users/ejgallego/orgs","repos_url":"https://api.github.com/users/ejgallego/repos","events_url":"https://api.github.com/users/ejgallego/events{/privacy}","received_events_url":"https://api.github.com/users/ejgallego/received_events","type":"User","site_admin":false},"labels":[{"id":661181694,"url":"https://api.github.com/repos/coq/coq/labels/help%20wanted","name":"help wanted","color":"fff06a","default":true},{"id":649047024,"url":"https://api.github.com/repos/coq/coq/labels/kind:%20infrastructure","name":"kind: infrastructure","color":"006b75","default":false}],"state":"open","locked":false,"assignee":{"login":"ejgallego","id":7192257,"avatar_url":"https://avatars2.githubusercontent.com/u/7192257?v=4","gravatar_id":"","url":"https://api.github.com/users/ejgallego","html_url":"https://github.com/ejgallego","followers_url":"https://api.github.com/users/ejgallego/followers","following_url":"https://api.github.com/users/ejgallego/following{/other_user}","gists_url":"https://api.github.com/users/ejgallego/gists{/gist_id}","starred_url":"https://api.github.com/users/ejgallego/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ejgallego/subscriptions","organizations_url":"https://api.github.com/users/ejgallego/orgs","repos_url":"https://api.github.com/users/ejgallego/repos","events_url":"https://api.github.com/users/ejgallego/events{/privacy}","received_events_url":"https://api.github.com/users/ejgallego/received_events","type":"User","site_admin":false},"assignees":[{"login":"ejgallego","id":7192257,"avatar_url":"https://avatars2.githubusercontent.com/u/7192257?v=4","gravatar_id":"","url":"https://api.github.com/users/ejgallego","html_url":"https://github.com/ejgallego","followers_url":"https://api.github.com/users/ejgallego/followers","following_url":"https://api.github.com/users/ejgallego/following{/other_user}","gists_url":"https://api.github.com/users/ejgallego/gists{/gist_id}","starred_url":"https://api.github.com/users/ejgallego/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ejgallego/subscriptions","organizations_url":"https://api.github.com/users/ejgallego/orgs","repos_url":"https://api.github.com/users/ejgallego/repos","events_url":"https://api.github.com/users/ejgallego/events{/privacy}","received_events_url":"https://api.github.com/users/ejgallego/received_events","type":"User","site_admin":false}],"milestone":{"url":"https://api.github.com/repos/coq/coq/milestones/12","html_url":"https://github.com/coq/coq/milestone/12","labels_url":"https://api.github.com/repos/coq/coq/milestones/12/labels","id":3139321,"number":12,"title":"8.8.0","description":"","creator":{"login":"maximedenes","id":647105,"avatar_url":"https://avatars1.githubusercontent.com/u/647105?v=4","gravatar_id":"","url":"https://api.github.com/users/maximedenes","html_url":"https://github.com/maximedenes","followers_url":"https://api.github.com/users/maximedenes/followers","following_url":"https://api.github.com/users/maximedenes/following{/other_user}","gists_url":"https://api.github.com/users/maximedenes/gists{/gist_id}","starred_url":"https://api.github.com/users/maximedenes/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/maximedenes/subscriptions","organizations_url":"https://api.github.com/users/maximedenes/orgs","repos_url":"https://api.github.com/users/maximedenes/repos","events_url":"https://api.github.com/users/maximedenes/events{/privacy}","received_events_url":"https://api.github.com/users/maximedenes/received_events","type":"User","site_admin":false},"open_issues":4,"closed_issues":0,"state":"open","created_at":"2018-02-23T14:53:53Z","updated_at":"2018-03-05T18:28:24Z","due_on":"2018-04-16T07:00:00Z","closed_at":null},"comments":5,"created_at":"2018-03-05T18:28:24Z","updated_at":"2018-03-05T19:20:32Z","closed_at":null,"author_association":"MEMBER","body":"It is not a secret that Coq CI demands are pretty high. As of today we need more than 10 hours build time of a medium-size CPU instance to test one PR. Would we do more serious testing this constraint would easily multiply by 10, so free plans are not an option. Custom commercial plans could be considered, however, Gitlab offers the possibility of running our own runners in our own servers. This is very attractive for several reasons:\r\n\r\n- No time limit per build: we can test developments that take a few hours to compile.\r\n- No limit on the number of instances: Gitlab can spin spot AWS instances so latency is minimal.\r\n- Open source: Gitlab is the only mature CI infrastructure that is open source.\r\n- Cleanup of the CI system: right now we support 3 different systems and we cannot standardize on a single platform, with the overhead this implies.\r\n\r\nMost of the work to migrate to Gitlab is already in place thanks to @SkySkimmer . I have setup a couple of reasonably powerful runners on MINES test servers so we should be covered in this sense too. The runners have been tested and they do seem to work and don't involve any undesired hack. A possible plan of action is:\r\n\r\n- setup a proper Coq mirror at https://gitlab.com/coq/coq , register the `etilio` runner [32 cores/32GiB RAM].\r\n- add notifications to Github interface.\r\n- setup AWS on spot instances so extra capacity is there when needed.\r\n- find a new server / fully more to AWS.\r\n\r\nThis should solve the following issues #6347 #6229 #5602. Issue #6807 needs attention after completing this."},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/370532128","html_url":"https://github.com/coq/coq/issues/6919#issuecomment-370532128","issue_url":"https://api.github.com/repos/coq/coq/issues/6919","id":370532128,"user":{"login":"Zimmi48","id":1108325,"avatar_url":"https://avatars2.githubusercontent.com/u/1108325?v=4","gravatar_id":"","url":"https://api.github.com/users/Zimmi48","html_url":"https://github.com/Zimmi48","followers_url":"https://api.github.com/users/Zimmi48/followers","following_url":"https://api.github.com/users/Zimmi48/following{/other_user}","gists_url":"https://api.github.com/users/Zimmi48/gists{/gist_id}","starred_url":"https://api.github.com/users/Zimmi48/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/Zimmi48/subscriptions","organizations_url":"https://api.github.com/users/Zimmi48/orgs","repos_url":"https://api.github.com/users/Zimmi48/repos","events_url":"https://api.github.com/users/Zimmi48/events{/privacy}","received_events_url":"https://api.github.com/users/Zimmi48/received_events","type":"User","site_admin":false},"created_at":"2018-03-05T19:20:32Z","updated_at":"2018-03-05T19:20:32Z","author_association":"CONTRIBUTOR","body":"I think a mirror is not what we need anyways. We need a repository on which a bot (force-)pushes to branches corresponding to PRs opened on the GitHub repository. I can try to look into this and also the GitHub status updates.\r\n\r\nI said it orally before but I wouldn't mind BTW if this repository was deleted with all the duplicate issues it contains then recreated but not as a mirror. I think you said I was an admin on the GitLab Coq organization. Should I go ahead and do it?"}}
{"actor":{"display_login":"Zimmi48"}}