{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/8245","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/8245/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/8245/comments","events_url":"https://api.github.com/repos/coq/coq/issues/8245/events","html_url":"https://github.com/coq/coq/issues/8245","id":349853840,"node_id":"MDU6SXNzdWUzNDk4NTM4NDA=","number":8245,"title":"creating n evars takes O(n^2.5) time; 4GB RAM for 8k","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":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2018-08-12T23:43:24Z","updated_at":"2018-08-13T01:29:36Z","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.14-arch1-1-ARCH #1 SMP PREEMPT Thu Aug 9 11:56:50 UTC 2018 x86_64 GNU/Linux`.\r\n\r\n#### Description of the problem\r\n\r\nHopefully this is just another manifestation of the issues underlying #8231 and #8237, but I am opening an issue anyway just to be sure.\r\n\r\nCreating evars is unexpectedly expensive. Creating 8000 evars takes a minute and a half and 4GB of RAM. The overall performance seems to scale worse than O(n^2) and better than O(n^3), so maybe O(n^2.5). I have not measured memory requirements for individual runs, but I suspect it is O(n^2).\r\n\r\n~~~~~~\r\nGoal True. Time do 250 (let H := fresh in evar (H : unit)). Abort. Optimize Heap.\r\n(* Finished transaction in 0.066 secs (0.042u,0.023s) (successful) *)\r\nGoal True. Time do 500 (let H := fresh in evar (H : unit)). Abort. Optimize Heap.\r\n(* Finished transaction in 0.192 secs (0.192u,0.s) (successful) *)\r\nGoal True. Time do 1000 (let H := fresh in evar (H : unit)). Abort. Optimize Heap.\r\n(* Finished transaction in 0.798 secs (0.779u,0.016s) (successful) *)\r\nGoal True. Time do 2000 (let H := fresh in evar (H : unit)). Abort. Optimize Heap.\r\n(* Finished transaction in 3.692 secs (3.599u,0.083s) (successful) *)\r\nGoal True. Time do 4000 (let H := fresh in evar (H : unit)). Abort. Optimize Heap.\r\n(* Finished transaction in 18.662 secs (18.329u,0.282s) (successful) *)\r\nGoal True. Time do 8000 (let H := fresh in evar (H : unit)). Abort.\r\n(* Finished transaction in 97.144 secs (95.799u,1.073s) (successful) *)\r\n\r\n(* 119.28user 1.68system 2:01.31elapsed 99%CPU (0avgtext+0avgdata 4050804maxresident)k\r\n0inputs+0outputs (0major+1272385minor)pagefaults 0swaps *)\r\n~~~~~~"},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/412387084","html_url":"https://github.com/coq/coq/issues/8245#issuecomment-412387084","issue_url":"https://api.github.com/repos/coq/coq/issues/8245","id":412387084,"node_id":"MDEyOklzc3VlQ29tbWVudDQxMjM4NzA4NA==","user":{"login":"JasonGross","id":396076,"node_id":"MDQ6VXNlcjM5NjA3Ng==","avatar_url":"https://avatars0.githubusercontent.com/u/396076?v=4","gravatar_id":"","url":"https://api.github.com/users/JasonGross","html_url":"https://github.com/JasonGross","followers_url":"https://api.github.com/users/JasonGross/followers","following_url":"https://api.github.com/users/JasonGross/following{/other_user}","gists_url":"https://api.github.com/users/JasonGross/gists{/gist_id}","starred_url":"https://api.github.com/users/JasonGross/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/JasonGross/subscriptions","organizations_url":"https://api.github.com/users/JasonGross/orgs","repos_url":"https://api.github.com/users/JasonGross/repos","events_url":"https://api.github.com/users/JasonGross/events{/privacy}","received_events_url":"https://api.github.com/users/JasonGross/received_events","type":"User","site_admin":false},"created_at":"2018-08-13T01:29:36Z","updated_at":"2018-08-13T01:29:36Z","author_association":"CONTRIBUTOR","body":"Maybe we should add an `epose` tactic and deprecate the `evar` tactic.  Note that you there are three things going on here: evar name creation, evar creation, and the fact that the context of each evar contains the previous ones.  If you want to pull apart evar creation separately, use `open_contr:(_: unit)` "}}
{"actor":{"display_login":"JasonGross"}}