{"action":"closed","number":6908,"pull_request":{"url":"https://api.github.com/repos/coq/coq/pulls/6908","id":172715286,"html_url":"https://github.com/coq/coq/pull/6908","diff_url":"https://github.com/coq/coq/pull/6908.diff","patch_url":"https://github.com/coq/coq/pull/6908.patch","issue_url":"https://api.github.com/repos/coq/coq/issues/6908","number":6908,"state":"closed","locked":false,"title":"Move VM global tables from C to ML","user":{"login":"ppedrot","id":1202327,"avatar_url":"https://avatars1.githubusercontent.com/u/1202327?v=4","gravatar_id":"","url":"https://api.github.com/users/ppedrot","html_url":"https://github.com/ppedrot","followers_url":"https://api.github.com/users/ppedrot/followers","following_url":"https://api.github.com/users/ppedrot/following{/other_user}","gists_url":"https://api.github.com/users/ppedrot/gists{/gist_id}","starred_url":"https://api.github.com/users/ppedrot/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ppedrot/subscriptions","organizations_url":"https://api.github.com/users/ppedrot/orgs","repos_url":"https://api.github.com/users/ppedrot/repos","events_url":"https://api.github.com/users/ppedrot/events{/privacy}","received_events_url":"https://api.github.com/users/ppedrot/received_events","type":"User","site_admin":false},"body":"This PR moves the VM global tables from the C implementation to the ML implementation. We declare them in ML code and pass them as an argument to the C reduction functions. This is a first step towards being able to synchronize this state with the Coq summary, so as to free unused memory, as well as locally replacing the value of a global, e.g. to implement local opacity in the VM.\r\n\r\nThis also makes the code slightly cleaner, e.g. automatically properly initializing the rel tables without them containing dummy data.\r\n\r\nI was afraid that this might have been slower due to the C compiler performing less optimizations, but it doesn't seem to be the case after all. I guess it makes sense, as the pointer is allocated by the OCaml GC anyways.\r\n\r\nBench:\r\n```\r\n┌──────────────────────────┬─────────────────────────┬─────────────────────────────────────┬───────────────────────────────────────┬─────────────────────────┬─────────────────┐\r\n│                          │      user time [s]      │             CPU cycles              │           CPU instructions            │  max resident mem [KB]  │   mem faults    │\r\n│                          │                         │                                     │                                       │                         │                 │\r\n│             package_name │     NEW     OLD PDIFF   │           NEW           OLD PDIFF   │            NEW            OLD PDIFF   │     NEW     OLD PDIFF   │ NEW OLD PDIFF   │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤\r\n│    coq-mathcomp-fingroup │   60.44   60.80 -0.59 % │  166428584127  166896752508 -0.28 % │   231469653541   231593430204 -0.05 % │  529468  529564 -0.02 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤\r\n│   coq-mathcomp-odd_order │ 1338.04 1343.05 -0.37 % │ 3722799312064 3730030746943 -0.19 % │  6591138192844  6588931938305 +0.03 % │ 1002808 1074176 -6.64 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤\r\n│   coq-mathcomp-character │  262.67  263.37 -0.27 % │  728361468299  730425121020 -0.28 % │  1074466695631  1074665224701 -0.02 % │  984344  984600 -0.03 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤\r\n│               coq-geocoq │ 3047.73 3051.96 -0.14 % │ 8476299150818 8486750182257 -0.12 % │ 13965502296280 13967856271799 -0.02 % │ 1240308 1242196 -0.15 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤\r\n│             coq-compcert │  814.51  814.76 -0.03 % │ 2273965839896 2272410670086 +0.07 % │  3424265355466  3425603069430 -0.04 % │ 1368320 1369244 -0.07 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤\r\n│     coq-mathcomp-algebra │  169.31  169.32 -0.01 % │  467079817224  466856454705 +0.05 % │   656166961721   656018828796 +0.02 % │  588608  588768 -0.03 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤\r\n│         coq-fiat-parsers │  659.88  659.57 +0.05 % │ 1840217524385 1843765680640 -0.19 % │  2957382112931  2958206304060 -0.03 % │ 3374380 3348048 +0.79 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤\r\n│           coq-coquelicot │   75.43   75.39 +0.05 % │  207446521549  207965394423 -0.25 % │   259630758430   259967721173 -0.13 % │  660052  656348 +0.56 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤\r\n│              coq-bignums │   75.10   75.05 +0.07 % │  208687387455  208352870670 +0.16 % │   283223957401   283302640068 -0.03 % │  526356  526552 -0.04 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤\r\n│                coq-color │  570.68  570.26 +0.07 % │ 1586587466967 1585912435822 +0.04 % │  1989591666968  1990298191910 -0.04 % │ 1438704 1439344 -0.04 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤\r\n│                 coq-hott │  309.40  309.14 +0.08 % │  842513689729  842397799466 +0.01 % │  1375685832726  1376007763700 -0.02 % │  496448  496576 -0.03 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤\r\n│ coq-mathcomp-real_closed │  165.54  165.34 +0.12 % │  459517066767  458971705800 +0.12 % │   699295227362   699416163376 -0.02 % │  714956  715232 -0.04 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤\r\n│                coq-flocq │   59.36   59.23 +0.22 % │  163587367310  163808903677 -0.14 % │   211527066041   211563117381 -0.02 % │  664056  660820 +0.49 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤\r\n│       coq-mathcomp-field │  441.04  439.72 +0.30 % │ 1223911680284 1220353697453 +0.29 % │  2024761406182  2024961143264 -0.01 % │  713300  713760 -0.06 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤\r\n│                 coq-corn │ 1479.40 1474.02 +0.36 % │ 4106968669794 4102830785496 +0.10 % │  6397483028130  6400106610373 -0.04 % │  839512  835800 +0.44 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤\r\n│    coq-mathcomp-solvable │  190.59  189.75 +0.44 % │  526621150340  526430860914 +0.04 % │   761548805325   761445630119 +0.01 % │  716420  716156 +0.04 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤\r\n│            coq-fiat-core │  102.73  102.20 +0.52 % │  290549062565  290036335676 +0.18 % │   378266514772   378135129211 +0.03 % │  500864  501416 -0.11 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤\r\n│   coq-mathcomp-ssreflect │   40.70   40.48 +0.54 % │  111612473841  111675287704 -0.06 % │   137656515666   137869727221 -0.15 % │  478660  478812 -0.03 % │   0   0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤\r\n│      coq-formal-topology │   34.33   34.08 +0.73 % │   94943536842   94961475070 -0.02 % │   125133046104   125084139188 +0.04 % │  483396  483864 -0.10 % │   0   0  +nan % │\r\n└──────────────────────────┴─────────────────────────┴─────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┴─────────────────┘\r\n\r\n\r\nPDIFF = proportional difference between measurements done for the NEW and the OLD Coq version\r\n      = (NEW_measurement - OLD_measurement) / OLD_measurement * 100%\r\n\r\nNEW = 3c38a282d505ed2ced734ac2f212c9328d704b6a\r\nOLD = df9d3a36e71d6d224286811fdc529ad5a955deb7\r\n```","created_at":"2018-03-04T11:40:25Z","updated_at":"2018-04-20T15:27:18Z","closed_at":"2018-04-20T15:27:18Z","merged_at":"2018-04-20T15:27:18Z","merge_commit_sha":"93c8e14d0c9bc233b2dcf213485b62a533b34580","assignee":{"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},"assignees":[{"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}],"requested_reviewers":[{"login":"barras","id":1170140,"avatar_url":"https://avatars2.githubusercontent.com/u/1170140?v=4","gravatar_id":"","url":"https://api.github.com/users/barras","html_url":"https://github.com/barras","followers_url":"https://api.github.com/users/barras/followers","following_url":"https://api.github.com/users/barras/following{/other_user}","gists_url":"https://api.github.com/users/barras/gists{/gist_id}","starred_url":"https://api.github.com/users/barras/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/barras/subscriptions","organizations_url":"https://api.github.com/users/barras/orgs","repos_url":"https://api.github.com/users/barras/repos","events_url":"https://api.github.com/users/barras/events{/privacy}","received_events_url":"https://api.github.com/users/barras/received_events","type":"User","site_admin":false}],"requested_teams":[],"labels":[{"id":485985791,"url":"https://api.github.com/repos/coq/coq/labels/kind:%20cleanup","name":"kind: cleanup","color":"3366ff","default":false},{"id":723611231,"url":"https://api.github.com/repos/coq/coq/labels/kind:%20enhancement","name":"kind: enhancement","color":"0e8a16","default":false}],"milestone":{"url":"https://api.github.com/repos/coq/coq/milestones/7","html_url":"https://github.com/coq/coq/milestone/7","labels_url":"https://api.github.com/repos/coq/coq/milestones/7/labels","id":2647743,"number":7,"title":"8.9+beta1","description":"The date of the feature freeze has not been announced yet.","creator":{"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},"open_issues":135,"closed_issues":58,"state":"open","created_at":"2017-07-18T15:03:25Z","updated_at":"2018-04-20T15:27:18Z","due_on":null,"closed_at":null},"commits_url":"https://api.github.com/repos/coq/coq/pulls/6908/commits","review_comments_url":"https://api.github.com/repos/coq/coq/pulls/6908/comments","review_comment_url":"https://api.github.com/repos/coq/coq/pulls/comments{/number}","comments_url":"https://api.github.com/repos/coq/coq/issues/6908/comments","statuses_url":"https://api.github.com/repos/coq/coq/statuses/93c8e14d0c9bc233b2dcf213485b62a533b34580","head":{"label":"ppedrot:vm-local-state","ref":"vm-local-state","sha":"93c8e14d0c9bc233b2dcf213485b62a533b34580","user":{"login":"ppedrot","id":1202327,"avatar_url":"https://avatars1.githubusercontent.com/u/1202327?v=4","gravatar_id":"","url":"https://api.github.com/users/ppedrot","html_url":"https://github.com/ppedrot","followers_url":"https://api.github.com/users/ppedrot/followers","following_url":"https://api.github.com/users/ppedrot/following{/other_user}","gists_url":"https://api.github.com/users/ppedrot/gists{/gist_id}","starred_url":"https://api.github.com/users/ppedrot/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ppedrot/subscriptions","organizations_url":"https://api.github.com/users/ppedrot/orgs","repos_url":"https://api.github.com/users/ppedrot/repos","events_url":"https://api.github.com/users/ppedrot/events{/privacy}","received_events_url":"https://api.github.com/users/ppedrot/received_events","type":"User","site_admin":false},"repo":{"id":10340342,"name":"coq","full_name":"ppedrot/coq","owner":{"login":"ppedrot","id":1202327,"avatar_url":"https://avatars1.githubusercontent.com/u/1202327?v=4","gravatar_id":"","url":"https://api.github.com/users/ppedrot","html_url":"https://github.com/ppedrot","followers_url":"https://api.github.com/users/ppedrot/followers","following_url":"https://api.github.com/users/ppedrot/following{/other_user}","gists_url":"https://api.github.com/users/ppedrot/gists{/gist_id}","starred_url":"https://api.github.com/users/ppedrot/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ppedrot/subscriptions","organizations_url":"https://api.github.com/users/ppedrot/orgs","repos_url":"https://api.github.com/users/ppedrot/repos","events_url":"https://api.github.com/users/ppedrot/events{/privacy}","received_events_url":"https://api.github.com/users/ppedrot/received_events","type":"User","site_admin":false},"private":false,"html_url":"https://github.com/ppedrot/coq","description":"Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. ","fork":true,"url":"https://api.github.com/repos/ppedrot/coq","forks_url":"https://api.github.com/repos/ppedrot/coq/forks","keys_url":"https://api.github.com/repos/ppedrot/coq/keys{/key_id}","collaborators_url":"https://api.github.com/repos/ppedrot/coq/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/ppedrot/coq/teams","hooks_url":"https://api.github.com/repos/ppedrot/coq/hooks","issue_events_url":"https://api.github.com/repos/ppedrot/coq/issues/events{/number}","events_url":"https://api.github.com/repos/ppedrot/coq/events","assignees_url":"https://api.github.com/repos/ppedrot/coq/assignees{/user}","branches_url":"https://api.github.com/repos/ppedrot/coq/branches{/branch}","tags_url":"https://api.github.com/repos/ppedrot/coq/tags","blobs_url":"https://api.github.com/repos/ppedrot/coq/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/ppedrot/coq/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/ppedrot/coq/git/refs{/sha}","trees_url":"https://api.github.com/repos/ppedrot/coq/git/trees{/sha}","statuses_url":"https://api.github.com/repos/ppedrot/coq/statuses/{sha}","languages_url":"https://api.github.com/repos/ppedrot/coq/languages","stargazers_url":"https://api.github.com/repos/ppedrot/coq/stargazers","contributors_url":"https://api.github.com/repos/ppedrot/coq/contributors","subscribers_url":"https://api.github.com/repos/ppedrot/coq/subscribers","subscription_url":"https://api.github.com/repos/ppedrot/coq/subscription","commits_url":"https://api.github.com/repos/ppedrot/coq/commits{/sha}","git_commits_url":"https://api.github.com/repos/ppedrot/coq/git/commits{/sha}","comments_url":"https://api.github.com/repos/ppedrot/coq/comments{/number}","issue_comment_url":"https://api.github.com/repos/ppedrot/coq/issues/comments{/number}","contents_url":"https://api.github.com/repos/ppedrot/coq/contents/{+path}","compare_url":"https://api.github.com/repos/ppedrot/coq/compare/{base}...{head}","merges_url":"https://api.github.com/repos/ppedrot/coq/merges","archive_url":"https://api.github.com/repos/ppedrot/coq/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/ppedrot/coq/downloads","issues_url":"https://api.github.com/repos/ppedrot/coq/issues{/number}","pulls_url":"https://api.github.com/repos/ppedrot/coq/pulls{/number}","milestones_url":"https://api.github.com/repos/ppedrot/coq/milestones{/number}","notifications_url":"https://api.github.com/repos/ppedrot/coq/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/ppedrot/coq/labels{/name}","releases_url":"https://api.github.com/repos/ppedrot/coq/releases{/id}","deployments_url":"https://api.github.com/repos/ppedrot/coq/deployments","created_at":"2013-05-28T16:46:07Z","updated_at":"2017-03-30T19:08:42Z","pushed_at":"2018-04-18T08:44:05Z","git_url":"git://github.com/ppedrot/coq.git","ssh_url":"git@github.com:ppedrot/coq.git","clone_url":"https://github.com/ppedrot/coq.git","svn_url":"https://github.com/ppedrot/coq","homepage":"http://coq.inria.fr/","size":90270,"stargazers_count":0,"watchers_count":0,"language":"OCaml","has_issues":false,"has_projects":true,"has_downloads":true,"has_wiki":false,"has_pages":false,"forks_count":0,"mirror_url":null,"archived":false,"open_issues_count":0,"license":{"key":"other","name":"Other","spdx_id":null,"url":null},"forks":0,"open_issues":0,"watchers":0,"default_branch":"master"}},"base":{"label":"coq:master","ref":"master","sha":"e128900aee63c972d7977fd47e3fd21649b63409","user":{"login":"coq","id":621198,"avatar_url":"https://avatars1.githubusercontent.com/u/621198?v=4","gravatar_id":"","url":"https://api.github.com/users/coq","html_url":"https://github.com/coq","followers_url":"https://api.github.com/users/coq/followers","following_url":"https://api.github.com/users/coq/following{/other_user}","gists_url":"https://api.github.com/users/coq/gists{/gist_id}","starred_url":"https://api.github.com/users/coq/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/coq/subscriptions","organizations_url":"https://api.github.com/users/coq/orgs","repos_url":"https://api.github.com/users/coq/repos","events_url":"https://api.github.com/users/coq/events{/privacy}","received_events_url":"https://api.github.com/users/coq/received_events","type":"Organization","site_admin":false},"repo":{"id":1377159,"name":"coq","full_name":"coq/coq","owner":{"login":"coq","id":621198,"avatar_url":"https://avatars1.githubusercontent.com/u/621198?v=4","gravatar_id":"","url":"https://api.github.com/users/coq","html_url":"https://github.com/coq","followers_url":"https://api.github.com/users/coq/followers","following_url":"https://api.github.com/users/coq/following{/other_user}","gists_url":"https://api.github.com/users/coq/gists{/gist_id}","starred_url":"https://api.github.com/users/coq/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/coq/subscriptions","organizations_url":"https://api.github.com/users/coq/orgs","repos_url":"https://api.github.com/users/coq/repos","events_url":"https://api.github.com/users/coq/events{/privacy}","received_events_url":"https://api.github.com/users/coq/received_events","type":"Organization","site_admin":false},"private":false,"html_url":"https://github.com/coq/coq","description":"Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. ","fork":false,"url":"https://api.github.com/repos/coq/coq","forks_url":"https://api.github.com/repos/coq/coq/forks","keys_url":"https://api.github.com/repos/coq/coq/keys{/key_id}","collaborators_url":"https://api.github.com/repos/coq/coq/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/coq/coq/teams","hooks_url":"https://api.github.com/repos/coq/coq/hooks","issue_events_url":"https://api.github.com/repos/coq/coq/issues/events{/number}","events_url":"https://api.github.com/repos/coq/coq/events","assignees_url":"https://api.github.com/repos/coq/coq/assignees{/user}","branches_url":"https://api.github.com/repos/coq/coq/branches{/branch}","tags_url":"https://api.github.com/repos/coq/coq/tags","blobs_url":"https://api.github.com/repos/coq/coq/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/coq/coq/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/coq/coq/git/refs{/sha}","trees_url":"https://api.github.com/repos/coq/coq/git/trees{/sha}","statuses_url":"https://api.github.com/repos/coq/coq/statuses/{sha}","languages_url":"https://api.github.com/repos/coq/coq/languages","stargazers_url":"https://api.github.com/repos/coq/coq/stargazers","contributors_url":"https://api.github.com/repos/coq/coq/contributors","subscribers_url":"https://api.github.com/repos/coq/coq/subscribers","subscription_url":"https://api.github.com/repos/coq/coq/subscription","commits_url":"https://api.github.com/repos/coq/coq/commits{/sha}","git_commits_url":"https://api.github.com/repos/coq/coq/git/commits{/sha}","comments_url":"https://api.github.com/repos/coq/coq/comments{/number}","issue_comment_url":"https://api.github.com/repos/coq/coq/issues/comments{/number}","contents_url":"https://api.github.com/repos/coq/coq/contents/{+path}","compare_url":"https://api.github.com/repos/coq/coq/compare/{base}...{head}","merges_url":"https://api.github.com/repos/coq/coq/merges","archive_url":"https://api.github.com/repos/coq/coq/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/coq/coq/downloads","issues_url":"https://api.github.com/repos/coq/coq/issues{/number}","pulls_url":"https://api.github.com/repos/coq/coq/pulls{/number}","milestones_url":"https://api.github.com/repos/coq/coq/milestones{/number}","notifications_url":"https://api.github.com/repos/coq/coq/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/coq/coq/labels{/name}","releases_url":"https://api.github.com/repos/coq/coq/releases{/id}","deployments_url":"https://api.github.com/repos/coq/coq/deployments","created_at":"2011-02-17T05:49:37Z","updated_at":"2018-04-19T21:09:02Z","pushed_at":"2018-04-20T15:26:56Z","git_url":"git://github.com/coq/coq.git","ssh_url":"git@github.com:coq/coq.git","clone_url":"https://github.com/coq/coq.git","svn_url":"https://github.com/coq/coq","homepage":"https://coq.inria.fr/","size":108673,"stargazers_count":1136,"watchers_count":1136,"language":"OCaml","has_issues":true,"has_projects":true,"has_downloads":true,"has_wiki":true,"has_pages":false,"forks_count":244,"mirror_url":null,"archived":false,"open_issues_count":1526,"license":{"key":"lgpl-2.1","name":"GNU Lesser General Public License v2.1","spdx_id":"LGPL-2.1","url":"https://api.github.com/licenses/lgpl-2.1"},"forks":244,"open_issues":1526,"watchers":1136,"default_branch":"master"}},"_links":{"self":{"href":"https://api.github.com/repos/coq/coq/pulls/6908"},"html":{"href":"https://github.com/coq/coq/pull/6908"},"issue":{"href":"https://api.github.com/repos/coq/coq/issues/6908"},"comments":{"href":"https://api.github.com/repos/coq/coq/issues/6908/comments"},"review_comments":{"href":"https://api.github.com/repos/coq/coq/pulls/6908/comments"},"review_comment":{"href":"https://api.github.com/repos/coq/coq/pulls/comments{/number}"},"commits":{"href":"https://api.github.com/repos/coq/coq/pulls/6908/commits"},"statuses":{"href":"https://api.github.com/repos/coq/coq/statuses/93c8e14d0c9bc233b2dcf213485b62a533b34580"}},"author_association":"OWNER","merged":true,"mergeable":null,"rebaseable":null,"mergeable_state":"unknown","merged_by":{"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},"comments":25,"review_comments":0,"maintainer_can_modify":false,"commits":3,"additions":70,"deletions":113,"changed_files":10}}
{"actor":{"display_login":"maximedenes"}}