{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/7442","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/7442/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/7442/comments","events_url":"https://api.github.com/repos/coq/coq/issues/7442/events","html_url":"https://github.com/coq/coq/pull/7442","id":320607366,"number":7442,"title":"Gitlab: build docker image in pipeline and use througn registry.","user":{"login":"SkySkimmer","id":2461932,"avatar_url":"https://avatars1.githubusercontent.com/u/2461932?v=4","gravatar_id":"","url":"https://api.github.com/users/SkySkimmer","html_url":"https://github.com/SkySkimmer","followers_url":"https://api.github.com/users/SkySkimmer/followers","following_url":"https://api.github.com/users/SkySkimmer/following{/other_user}","gists_url":"https://api.github.com/users/SkySkimmer/gists{/gist_id}","starred_url":"https://api.github.com/users/SkySkimmer/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/SkySkimmer/subscriptions","organizations_url":"https://api.github.com/users/SkySkimmer/orgs","repos_url":"https://api.github.com/users/SkySkimmer/repos","events_url":"https://api.github.com/users/SkySkimmer/events{/privacy}","received_events_url":"https://api.github.com/users/SkySkimmer/received_events","type":"User","site_admin":false},"labels":[{"id":723611231,"url":"https://api.github.com/repos/coq/coq/labels/kind:%20enhancement","name":"kind: enhancement","color":"0e8a16","default":false},{"id":649047024,"url":"https://api.github.com/repos/coq/coq/labels/kind:%20infrastructure","name":"kind: infrastructure","color":"006b75","default":false},{"id":493098247,"url":"https://api.github.com/repos/coq/coq/labels/needs:%20testing","name":"needs: testing","color":"c2e0c6","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":null,"comments":4,"created_at":"2018-05-06T16:36:10Z","updated_at":"2018-05-06T18:34:53Z","closed_at":null,"author_association":"CONTRIBUTOR","pull_request":{"url":"https://api.github.com/repos/coq/coq/pulls/7442","html_url":"https://github.com/coq/coq/pull/7442","diff_url":"https://github.com/coq/coq/pull/7442.diff","patch_url":"https://github.com/coq/coq/pull/7442.patch"},"body":"A docker-boot job is added which builds the docker image and pushes it\r\nto the registry, the other jobs running on the image from the\r\nregistry.\r\n\r\nThe boot job reuses the already pushed image if it exists and matches,\r\nthis is important to cut down its runtime.\r\n\r\nMaking a new image takes 30min for all the switches\r\nhttps://gitlab.com/SkySkimmer/coq/-/jobs/66650546\r\nFor testing I removed all jobs except boot and main build, and after\r\nthat run I built only the standard switch.\r\n\r\nBuilding 1 switch takes around 20min\r\nhttps://gitlab.com/SkySkimmer/coq/-/jobs/66656942\r\nWhen the registry is up to date it takes 2min\r\nhttps://gitlab.com/SkySkimmer/coq/-/jobs/66658790\r\n(I don't know about all switches but probably no more than 5min)\r\n\r\nEach pipeline pushes the image to $CI_REGISTRY_IMAGE:$CI_PIPELINE_ID\r\nwhich is eg registry.gitlab.com/skyskimmer/coq:21557176 and is what\r\nthe other jobs use to run themselves.\r\n\r\nFor caching it pulls from and pushes to a constant name, in this test\r\n$CI_REGISTRY_IMAGE:$CACHEKEY. We might also want to pull from the main\r\ncoq repo to avoid redoing work.\r\n\r\nThe question of having 1 image or 1 image/switch remains open.\r\n\r\nUsing the gitlab registry doesn't really work for circle CI, so the\r\ndockerhub account would have to remain (or circle could return to an\r\nopam-boot job, or be removed from our CI). There are similar concerns\r\nwith travis if we want to move it to docker.\r\n"},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/386902043","html_url":"https://github.com/coq/coq/pull/7442#issuecomment-386902043","issue_url":"https://api.github.com/repos/coq/coq/issues/7442","id":386902043,"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},"created_at":"2018-05-06T18:34:53Z","updated_at":"2018-05-06T18:34:53Z","author_association":"MEMBER","body":"> Better question, what's your use case?\r\n\r\nUse case is as follows:\r\n1. I update dockerfile.\r\n2. I submit a pull request -> that will trigger a pull request.\r\n3. The CI system detects that I have push rights to `hub.docker.com/coqci`, then it pushes it there."}}
{"actor":{"display_login":"ejgallego"}}