{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/8708","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/8708/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/8708/comments","events_url":"https://api.github.com/repos/coq/coq/issues/8708/events","html_url":"https://github.com/coq/coq/pull/8708","id":369025076,"node_id":"MDExOlB1bGxSZXF1ZXN0MjIyMDYxNjk2","number":8708,"title":"Stupid but critical unfolding heuristic.","user":{"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},"labels":[{"id":651324615,"node_id":"MDU6TGFiZWw2NTEzMjQ2MTU=","url":"https://api.github.com/repos/coq/coq/labels/kind:%20performance","name":"kind: performance","color":"9900cc","default":false}],"state":"open","locked":false,"assignee":{"login":"maximedenes","id":647105,"node_id":"MDQ6VXNlcjY0NzEwNQ==","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,"node_id":"MDQ6VXNlcjY0NzEwNQ==","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}],"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":54,"closed_issues":143,"state":"open","created_at":"2018-07-20T18:48:13Z","updated_at":"2018-10-11T19:56:20Z","due_on":null,"closed_at":null},"comments":6,"created_at":"2018-10-11T09:13:17Z","updated_at":"2018-10-11T20:03:14Z","closed_at":null,"author_association":"MEMBER","pull_request":{"url":"https://api.github.com/repos/coq/coq/pulls/8708","html_url":"https://github.com/coq/coq/pull/8708","diff_url":"https://github.com/coq/coq/pull/8708.diff","patch_url":"https://github.com/coq/coq/pull/8708.patch"},"body":"We favour unfolding of variables over constants because it is more frequent for the former to depend on the latter. This has huge consequences on a few extremely slow lines in mathcomp, up to dividing by 3 single-line invocations that were taking about 30s on my laptop before the patch.\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-mathcomp-field │  451.52  470.17 -3.97 % │  1256043920785  1307499881942 -3.94 % │  2039642380866  2125985727874 -4.06 % │  799080  805436 -0.79 % │    0   23 -100.00 % │\r\n├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼───────────────────┤\r\n│ coq-mathcomp-real-closed │  181.46  188.46 -3.71 % │   504892234076   524215868132 -3.69 % │   757711653396   790457635832 -4.14 % │  834296  828084 +0.75 % │    8    0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼───────────────────┤\r\n│              coq-unimath │ 1325.43 1336.12 -0.80 % │  3681679259332  3708538536896 -0.72 % │  6179317614400  6222320894210 -0.69 % │  986772  985524 +0.13 % │  356   21 +1595.24 % │\r\n├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼───────────────────┤\r\n│    coq-mathcomp-solvable │  219.08  220.25 -0.53 % │   608797537680   611189014049 -0.39 % │   867625487689   873007484061 -0.62 % │  819324  857276 -4.43 % │    0  253 -100.00 % │\r\n├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼───────────────────┤\r\n│         coq-fiat-parsers │  720.67  722.96 -0.32 % │  2000208918420  2004623043606 -0.22 % │  3058299308839  3058326911836 -0.00 % │ 2902324 2900992 +0.05 % │  144  488 -70.49 % │\r\n├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼───────────────────┤\r\n│              coq-bignums │   98.71   99.02 -0.31 % │   273072599990   273677176889 -0.22 % │   392925460275   393691214873 -0.19 % │  536264  536424 -0.03 % │   14    0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼───────────────────┤\r\n│               coq-sf-plf │   74.56   74.79 -0.31 % │   206312768406   206681404110 -0.18 % │   300628456391   300793941880 -0.06 % │  517772  518080 -0.06 % │   15    0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼───────────────────┤\r\n│            coq-fiat-core │  135.30  135.71 -0.30 % │   376717172228   377099349882 -0.10 % │   503947956067   503947945028 +0.00 % │  497972  497584 +0.08 % │  301  169 +78.11 % │\r\n├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼───────────────────┤\r\n│          coq-fiat-crypto │ 6309.56 6325.22 -0.25 % │ 17541473517561 17591620619420 -0.29 % │ 28886741757670 28949118285129 -0.22 % │ 2527464 2442976 +3.46 % │ 1429 1604 -10.91 % │\r\n├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼───────────────────┤\r\n│     coq-mathcomp-algebra │  205.52  205.79 -0.13 % │   570756493375   570824541479 -0.01 % │   797968129879   798592485059 -0.08 % │  641780  640908 +0.14 % │   13    6 +116.67 % │\r\n├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼───────────────────┤\r\n│                 coq-corn │ 1549.43 1550.91 -0.10 % │  4299177955994  4304767005454 -0.13 % │  6351031458314  6345679761648 +0.08 % │  818156  818080 +0.01 % │   44   44 +0.00 % │\r\n├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼───────────────────┤\r\n│               coq-geocoq │ 2835.56 2837.44 -0.07 % │  7883254537381  7887266939714 -0.05 % │ 12581310463650 12580378357181 +0.01 % │ 1289188 1285740 +0.27 % │  321  178 +80.34 % │\r\n├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼───────────────────┤\r\n│   coq-mathcomp-odd-order │ 1431.87 1432.56 -0.05 % │  3988503267711  3989436346228 -0.02 % │  6650430717672  6654458068276 -0.06 % │ 1364656 1360124 +0.33 % │    0    2 -100.00 % │\r\n├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼───────────────────┤\r\n│                 coq-hott │  342.14  342.28 -0.04 % │   948452221439   947717140665 +0.08 % │  1439699491374  1439423119663 +0.02 % │  666944  666992 -0.01 % │  382    0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼───────────────────┤\r\n│                  coq-vst │ 1714.00 1714.29 -0.02 % │  4764986261802  4765835678370 -0.02 % │  6523473751238  6526214668298 -0.04 % │ 2227400 2226844 +0.02 % │  282  286 -1.40 % │\r\n├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼───────────────────┤\r\n│                coq-gpfsl │ 1202.25 1202.20 +0.00 % │  3348424834354  3350145488560 -0.05 % │  4403586425502  4406497294245 -0.07 % │ 1620244 1587020 +2.09 % │   64    0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼───────────────────┤\r\n│   coq-mathcomp-ssreflect │   65.58   65.55 +0.05 % │   180634941007   180188270946 +0.25 % │   256343795744   256383543912 -0.02 % │  532196  532240 -0.01 % │    2    0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼───────────────────┤\r\n│         coq-math-classes │  249.97  249.78 +0.08 % │   687772203013   687852583176 -0.01 % │   898725881448   898785908738 -0.01 % │  521896  521744 +0.03 % │   84   84 +0.00 % │\r\n├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼───────────────────┤\r\n│    coq-mathcomp-fingroup │   85.04   84.97 +0.08 % │   234731017390   234785733709 -0.02 % │   348232320594   348351868361 -0.03 % │  588272  587564 +0.12 % │  156    0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼───────────────────┤\r\n│                coq-color │  736.73  735.84 +0.12 % │  2041003298859  2040706082908 +0.01 % │  2469055547704  2468533084188 +0.02 % │ 1370684 1429024 -4.08 % │   29  125 -76.80 % │\r\n├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼───────────────────┤\r\n│               coq-sf-vfa │   47.51   47.42 +0.19 % │   131258414117   131337549759 -0.06 % │   209539052188   209723174423 -0.09 % │  535660  535548 +0.02 % │   28    5 +460.00 % │\r\n├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼───────────────────┤\r\n│                coq-flocq │  594.14  592.81 +0.22 % │  1653379570180  1650326873739 +0.18 % │  2412867943085  2414747976836 -0.08 % │ 1764196 1764464 -0.02 % │  304   72 +322.22 % │\r\n├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼───────────────────┤\r\n│             coq-compcert │  892.66  890.48 +0.24 % │  2474398884437  2469212143007 +0.21 % │  3563190637748  3563333486762 -0.00 % │ 1355244 1355808 -0.04 % │  173  200 -13.50 % │\r\n├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼───────────────────┤\r\n│      coq-formal-topology │   57.97   57.82 +0.26 % │   158704356032   158734343611 -0.02 % │   239295939520   239343068057 -0.02 % │  477660  477608 +0.01 % │    0    0  +nan % │\r\n├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼───────────────────┤\r\n│   coq-mathcomp-character │  294.20  293.39 +0.28 % │   817703227889   815703662517 +0.25 % │  1188165014136  1185265372027 +0.24 % │ 1110704 1060032 +4.78 % │    5    2 +150.00 % │\r\n├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼───────────────────┤\r\n│           coq-coquelicot │  103.74  103.42 +0.31 % │   286843510132   286677435187 +0.06 % │   386118985227   386218345638 -0.03 % │  712688  714148 -0.20 % │  279   13 +2046.15 % │\r\n├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼───────────────────┤\r\n│                coq-sf-lf │   44.62   44.39 +0.52 % │   122205285805   122358099952 -0.12 % │   198837633045   198990048150 -0.08 % │  423104  423264 -0.04 % │  128    0  +nan % │\r\n└──────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┴───────────────────┘\r\n```"},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/429098870","html_url":"https://github.com/coq/coq/pull/8708#issuecomment-429098870","issue_url":"https://api.github.com/repos/coq/coq/issues/8708","id":429098870,"node_id":"MDEyOklzc3VlQ29tbWVudDQyOTA5ODg3MA==","user":{"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},"created_at":"2018-10-11T20:03:14Z","updated_at":"2018-10-11T20:03:14Z","author_association":"MEMBER","body":"> Yes, this is very nice! It would be interesting to hear about how came the idea of this improvement (and if similar ones are still possible).\r\n\r\nI was profiling the slowest diffs of @SkySkimmer's [Sprop branch](https://github.com/coq/ceps/pull/37), and came upon what looked like extremely slow conversions that were made worse by this branch. Had a deeper look and realized that the conversion was stupid.\r\n\r\n(The unofficial reason is that I badly want Sprop to land, and negating the slowdowns that it introduces by unrelated optimizations makes it easier for people to accept this. You know the drill.)\r\n\r\nAlso, I am currently trying to devise some even better heuristic based on the dependency between constants, but I don't know yet how to do it efficiently. The idea is that if a constant transitively contains another one, it is more likely that unfolding the former before the latter is going to lead to a shorter conversion route.\r\n"}}
{"actor":{"display_login":"ppedrot"}}