{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/8237","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/8237/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/8237/comments","events_url":"https://api.github.com/repos/coq/coq/issues/8237/events","html_url":"https://github.com/coq/coq/issues/8237","id":349674586,"node_id":"MDU6SXNzdWUzNDk2NzQ1ODY=","number":8237,"title":"do n (pose proof I) takes O(n^2) time","user":{"login":"andres-erbsen","id":918403,"node_id":"MDQ6VXNlcjkxODQwMw==","avatar_url":"https://avatars0.githubusercontent.com/u/918403?v=4","gravatar_id":"","url":"https://api.github.com/users/andres-erbsen","html_url":"https://github.com/andres-erbsen","followers_url":"https://api.github.com/users/andres-erbsen/followers","following_url":"https://api.github.com/users/andres-erbsen/following{/other_user}","gists_url":"https://api.github.com/users/andres-erbsen/gists{/gist_id}","starred_url":"https://api.github.com/users/andres-erbsen/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/andres-erbsen/subscriptions","organizations_url":"https://api.github.com/users/andres-erbsen/orgs","repos_url":"https://api.github.com/users/andres-erbsen/repos","events_url":"https://api.github.com/users/andres-erbsen/events{/privacy}","received_events_url":"https://api.github.com/users/andres-erbsen/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":null,"assignees":[],"milestone":null,"comments":9,"created_at":"2018-08-10T22:26:02Z","updated_at":"2018-08-11T12:49:15Z","closed_at":null,"author_association":"NONE","body":"<!-- Thank you for your contribution.\r\n     Please complete the following information when reporting a bug. -->\r\n\r\n#### Version\r\n\r\n~~~~~\r\nThe Coq Proof Assistant, version 8.8.1 (July 2018)\r\ncompiled on Jul 5 2018 7:25:50 with OCaml 4.06.0\r\n~~~~~\r\n\r\n#### Operating system\r\n\r\nArch Linux, up to date as of yesterday. `Linux ashryn 4.17.13-arch1-1-ARCH #1 SMP PREEMPT Mon Aug 6 23:06:31 UTC 2018 x86_64 GNU/Linux`\r\n\r\n#### Description of the problem\r\n\r\n~~~~~\r\nGoal True. Time (do 125 pose proof I). exact I. Qed.\r\n(* Finished transaction in 0.009 secs (0.009u,0.s) (successful) *)\r\nGoal True. Time (do 250 pose proof I). exact I. Qed.\r\n(* Finished transaction in 0.027 secs (0.024u,0.003s) (successful) *)\r\nGoal True. Time (do 500 pose proof I). exact I. Qed.\r\n(* Finished transaction in 0.117 secs (0.106u,0.01s) (successful) *)\r\nGoal True. Time (do 1000 pose proof I). exact I. Qed.\r\n(* Finished transaction in 0.43 secs (0.409u,0.02s) (successful) *)\r\nGoal True. Time (do 2000 pose proof I). exact I. Qed.\r\n(* Finished transaction in 1.771 secs (1.714u,0.049s) (successful) *)\r\nGoal True. Time (do 4000 pose proof I). exact I. Qed.\r\n(* Finished transaction in 8.554 secs (8.31u,0.195s) (successful) *)\r\n\r\n(* TOTAL: coqc many_hyps.v  176.96s user 0.66s system 99% cpu 2:58.12 total *)\r\n~~~~~\r\n\r\n![quadratic](https://user-images.githubusercontent.com/918403/43983804-bf91756a-9cca-11e8-89e4-d49736f7ec9c.png)\r\n"},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/412273028","html_url":"https://github.com/coq/coq/issues/8237#issuecomment-412273028","issue_url":"https://api.github.com/repos/coq/coq/issues/8237","id":412273028,"node_id":"MDEyOklzc3VlQ29tbWVudDQxMjI3MzAyOA==","user":{"login":"andres-erbsen","id":918403,"node_id":"MDQ6VXNlcjkxODQwMw==","avatar_url":"https://avatars0.githubusercontent.com/u/918403?v=4","gravatar_id":"","url":"https://api.github.com/users/andres-erbsen","html_url":"https://github.com/andres-erbsen","followers_url":"https://api.github.com/users/andres-erbsen/followers","following_url":"https://api.github.com/users/andres-erbsen/following{/other_user}","gists_url":"https://api.github.com/users/andres-erbsen/gists{/gist_id}","starred_url":"https://api.github.com/users/andres-erbsen/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/andres-erbsen/subscriptions","organizations_url":"https://api.github.com/users/andres-erbsen/orgs","repos_url":"https://api.github.com/users/andres-erbsen/repos","events_url":"https://api.github.com/users/andres-erbsen/events{/privacy}","received_events_url":"https://api.github.com/users/andres-erbsen/received_events","type":"User","site_admin":false},"created_at":"2018-08-11T12:49:15Z","updated_at":"2018-08-11T12:49:15Z","author_association":"NONE","body":"@gares but is it actually necessary to copy the entire context in the refiner, even though it appears only once in the proof object?"}}
{"actor":{"display_login":"andres-erbsen"}}