{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/8811","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/8811/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/8811/comments","events_url":"https://api.github.com/repos/coq/coq/issues/8811/events","html_url":"https://github.com/coq/coq/pull/8811","id":373389364,"node_id":"MDExOlB1bGxSZXF1ZXN0MjI1MzI5MTU3","number":8811,"title":"EConstr-aware functions to produce kernel entries","user":{"login":"SkySkimmer","id":2461932,"node_id":"MDQ6VXNlcjI0NjE5MzI=","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":485985791,"node_id":"MDU6TGFiZWw0ODU5ODU3OTE=","url":"https://api.github.com/repos/coq/coq/labels/kind:%20cleanup","name":"kind: cleanup","color":"3366ff","default":false},{"id":723611231,"node_id":"MDU6TGFiZWw3MjM2MTEyMzE=","url":"https://api.github.com/repos/coq/coq/labels/kind:%20enhancement","name":"kind: enhancement","color":"0e8a16","default":false},{"id":777223550,"node_id":"MDU6TGFiZWw3NzcyMjM1NTA=","url":"https://api.github.com/repos/coq/coq/labels/needs:%20benchmarking","name":"needs: benchmarking","color":"c2e0c6","default":false}],"state":"open","locked":false,"assignee":{"login":"ppedrot","id":1202327,"node_id":"MDQ6VXNlcjEyMDIzMjc=","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},"assignees":[{"login":"ppedrot","id":1202327,"node_id":"MDQ6VXNlcjEyMDIzMjc=","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}],"milestone":{"url":"https://api.github.com/repos/coq/coq/milestones/16","html_url":"https://github.com/coq/coq/milestone/16","labels_url":"https://api.github.com/repos/coq/coq/milestones/16/labels","id":3512681,"node_id":"MDk6TWlsZXN0b25lMzUxMjY4MQ==","number":16,"title":"8.10+beta1","description":"","creator":{"login":"Zimmi48","id":1108325,"node_id":"MDQ6VXNlcjExMDgzMjU=","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":118,"closed_issues":352,"state":"open","created_at":"2018-07-20T18:48:13Z","updated_at":"2018-12-06T18:06:44Z","due_on":null,"closed_at":null},"comments":8,"created_at":"2018-10-24T09:30:25Z","updated_at":"2018-12-06T18:19:32Z","closed_at":null,"author_association":"CONTRIBUTOR","pull_request":{"url":"https://api.github.com/repos/coq/coq/pulls/8811","html_url":"https://github.com/coq/coq/pull/8811","diff_url":"https://github.com/coq/coq/pull/8811.diff","patch_url":"https://github.com/coq/coq/pull/8811.patch"},"body":"This is in some way similar to #7530 (evarutil.finalize) but more high level / less flexible. As such it is used in less places (eg fixpoints are not ported).\r\nHopefully it doesn't have the perf issues appearing in #7530."},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/444975355","html_url":"https://github.com/coq/coq/pull/8811#issuecomment-444975355","issue_url":"https://api.github.com/repos/coq/coq/issues/8811","id":444975355,"node_id":"MDEyOklzc3VlQ29tbWVudDQ0NDk3NTM1NQ==","user":{"login":"SkySkimmer","id":2461932,"node_id":"MDQ6VXNlcjI0NjE5MzI=","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},"created_at":"2018-12-06T18:19:32Z","updated_at":"2018-12-06T18:19:32Z","author_association":"CONTRIBUTOR","body":"https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/597/console\r\n~~~\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-bignums │  101.96  102.62 -0.64 % │      282338079138      284235517951 -0.67 % │      409989399395      410303113966 -0.08 % │     537580     537384  +0.04 % │      60       0     +nan % │\r\n├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼────────────────────────────────┼────────────────────────────┤\r\n│             coq-sf-vfa │   50.50   50.80 -0.59 % │      140100824283      140648237288 -0.39 % │      226036291326      226320125671 -0.13 % │     532700     532680  +0.00 % │      30       5  +500.00 % │\r\n├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼────────────────────────────────┼────────────────────────────┤\r\n│ coq-mathcomp-odd-order │ 1413.34 1421.32 -0.56 % │     3937316012185     3957083927842 -0.50 % │     6598412044817     6598458596578 -0.00 % │    1379484    1380172  -0.05 % │       2       0     +nan % │\r\n├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼────────────────────────────────┼────────────────────────────┤\r\n│               coq-hott │  333.38  334.64 -0.38 % │      922210050092      926736817122 -0.49 % │     1406713801041     1407088727152 -0.03 % │     473432     473624  -0.04 % │     363       0     +nan % │\r\n├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼────────────────────────────────┼────────────────────────────┤\r\n│          coq-fiat-core │  139.06  139.51 -0.32 % │      387031658110      388281698533 -0.32 % │      519940923885      520076605207 -0.03 % │     503100     503132  -0.01 % │     234      91  +157.14 % │\r\n├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼────────────────────────────────┼────────────────────────────┤\r\n│        coq-fiat-crypto │ 6436.88 6457.70 -0.32 % │    17906723771214    17960245377613 -0.30 % │    29163028682477    29192328464029 -0.10 % │    2451456    2457760  -0.26 % │    1596    1586    +0.63 % │\r\n├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼────────────────────────────────┼────────────────────────────┤\r\n│              coq-flocq │  596.85  598.61 -0.29 % │     1660565880246     1665403444120 -0.29 % │     2432043041158     2432361244629 -0.01 % │    1772860    1773160  -0.02 % │     484     256   +89.06 % │\r\n├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼────────────────────────────────┼────────────────────────────┤\r\n│       coq-fiat-parsers │  725.82  727.96 -0.29 % │     2010698290018     2020417706533 -0.48 % │     3064409264935     3064789304018 -0.01 % │    2908692    2908516  +0.01 % │      19     501   -96.21 % │\r\n├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼────────────────────────────────┼────────────────────────────┤\r\n│           coq-compcert │  904.26  906.92 -0.29 % │     2509520186688     2515262698477 -0.23 % │     3618209870666     3618289198247 -0.00 % │    1304944    1304856  +0.01 % │     167     241   -30.71 % │\r\n├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼────────────────────────────────┼────────────────────────────┤\r\n│                coq-vst │ 3158.03 3166.87 -0.28 % │     8787346885969     8810528617717 -0.26 % │    12258283132013    12256170503731 +0.02 % │    2223852    2224824  -0.04 % │      99      98    +1.02 % │\r\n├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼────────────────────────────────┼────────────────────────────┤\r\n│  coq-mathcomp-fingroup │   87.42   87.66 -0.27 % │      241700097700      242230886344 -0.22 % │      356520918650      357018056141 -0.14 % │     583580     583736  -0.03 % │     156       2 +7700.00 % │\r\n├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼────────────────────────────────┼────────────────────────────┤\r\n│             coq-sf-plf │   78.18   78.33 -0.19 % │      216412378007      216497387221 -0.04 % │      317902975426      318113832728 -0.07 % │     519364     519924  -0.11 % │      15       0     +nan % │\r\n├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼────────────────────────────────┼────────────────────────────┤\r\n│        coq-lambda-rust │ 2376.81 2380.57 -0.16 % │     6619903903574     6632347515790 -0.19 % │     8958908365669     8957892088986 +0.01 % │    1427156    1427524  -0.03 % │      20      37   -45.95 % │\r\n├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼────────────────────────────────┼────────────────────────────┤\r\n│              coq-color │  746.77  747.74 -0.13 % │     2071498271694     2073481296812 -0.10 % │     2506998303078     2506925158949 +0.00 % │    1436012    1435912  +0.01 % │     216     288   -25.00 % │\r\n├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼────────────────────────────────┼────────────────────────────┤\r\n│            coq-unimath │ 1653.72 1654.97 -0.08 % │     4594027693787     4598210694749 -0.09 % │     7828905326342     7827165326759 +0.02 % │    1233708    1116168 +10.53 % │     352      22 +1500.00 % │\r\n├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼────────────────────────────────┼────────────────────────────┤\r\n│ coq-mathcomp-character │  289.73  289.90 -0.06 % │      805745559898      805326476422 +0.05 % │     1149761071288     1149945509475 -0.02 % │    1107344    1107372  -0.00 % │      13       0     +nan % │\r\n├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼────────────────────────────────┼────────────────────────────┤\r\n│  coq-mathcomp-solvable │  224.62  224.75 -0.06 % │      623486471824      623977808326 -0.08 % │      875168425187      875406672346 -0.03 % │     824060     865204  -4.76 % │      20     251   -92.03 % │\r\n├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼────────────────────────────────┼────────────────────────────┤\r\n│     coq-mathcomp-field │  266.00  266.14 -0.05 % │      739259499966      740246382128 -0.13 % │     1111085910069     1111344663737 -0.02 % │     756176     756212  -0.00 % │       0      22  -100.00 % │\r\n├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼────────────────────────────────┼────────────────────────────┤\r\n│              coq-sf-lf │   47.92   47.93 -0.02 % │      131204099977      131576075041 -0.28 % │      215186904363      215408072152 -0.10 % │     430936     430824  +0.03 % │     117       0     +nan % │\r\n├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼────────────────────────────────┼────────────────────────────┤\r\n│    coq-formal-topology │   61.20   61.18 +0.03 % │      167687517342      167448275119 +0.14 % │      254975546503      255161564876 -0.07 % │     480480     480272  +0.04 % │      53       0     +nan % │\r\n├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼────────────────────────────────┼────────────────────────────┤\r\n│       coq-math-classes │  256.65  256.56 +0.04 % │      706626738466      707506051095 -0.12 % │      930632466915      930885628001 -0.03 % │     529080     529108  -0.01 % │      84      84    +0.00 % │\r\n├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼────────────────────────────────┼────────────────────────────┤\r\n│   coq-mathcomp-algebra │  191.14  191.06 +0.04 % │      530522736698      530219151417 +0.06 % │      718445972063      718684074473 -0.03 % │     641512     641392  +0.02 % │      34      10  +240.00 % │\r\n├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼────────────────────────────────┼────────────────────────────┤\r\n│               coq-corn │ 1550.35 1549.46 +0.06 % │     4303399369861     4303792699841 -0.01 % │     6321445655354     6321538764642 -0.00 % │     873848     874232  -0.04 % │      99      49  +102.04 % │\r\n├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼────────────────────────────────┼────────────────────────────┤\r\n│             coq-geocoq │ 2057.12 2055.57 +0.08 % │     5713447977265     5708315670261 +0.09 % │     8274224266887     8274950029271 -0.01 % │    1242892    1223236  +1.61 % │     175     120   +45.83 % │\r\n├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼────────────────────────────────┼────────────────────────────┤\r\n│ coq-mathcomp-ssreflect │   69.86   69.70 +0.23 % │      191933788098      191675717389 +0.13 % │      274701214289      274891078812 -0.07 % │     533268     533284  -0.00 % │       2       0     +nan % │\r\n├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼────────────────────────────────┼────────────────────────────┤\r\n│         coq-coquelicot │  108.84  108.51 +0.30 % │      300530963260      300932444258 -0.13 % │      407795743847      407756005263 +0.01 % │     708896     708916  -0.00 % │     282      14 +1914.29 % │\r\n└────────────────────────┴─────────────────────────┴─────────────────────────────────────────────┴─────────────────────────────────────────────┴────────────────────────────────┴────────────────────────────┘\r\n~~~\r\nFinally no impact"}}
{"actor":{"display_login":"SkySkimmer"}}