{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/6374","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/6374/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/6374/comments","events_url":"https://api.github.com/repos/coq/coq/issues/6374/events","html_url":"https://github.com/coq/coq/pull/6374","id":280857765,"number":6374,"title":"[toplevel] Modify printing goal strategy.","user":{"login":"ejgallego","id":7192257,"avatar_url":"https://avatars2.githubusercontent.com/u/7192257?v=4","gravatar_id":"","url":"https://api.github.com/users/ejgallego","html_url":"https://github.com/ejgallego","followers_url":"https://api.github.com/users/ejgallego/followers","following_url":"https://api.github.com/users/ejgallego/following{/other_user}","gists_url":"https://api.github.com/users/ejgallego/gists{/gist_id}","starred_url":"https://api.github.com/users/ejgallego/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ejgallego/subscriptions","organizations_url":"https://api.github.com/users/ejgallego/orgs","repos_url":"https://api.github.com/users/ejgallego/repos","events_url":"https://api.github.com/users/ejgallego/events{/privacy}","received_events_url":"https://api.github.com/users/ejgallego/received_events","type":"User","site_admin":false},"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},{"id":396673733,"url":"https://api.github.com/repos/coq/coq/labels/kind:%20redesign","name":"kind: redesign","color":"0052cc","default":false},{"id":640626205,"url":"https://api.github.com/repos/coq/coq/labels/needs:%20independent%20fix","name":"needs: independent fix","color":"ffc8f2","default":false}],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":{"url":"https://api.github.com/repos/coq/coq/milestones/5","html_url":"https://github.com/coq/coq/milestone/5","labels_url":"https://api.github.com/repos/coq/coq/milestones/5/labels","id":2550427,"number":5,"title":"8.8","description":"","creator":{"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},"open_issues":141,"closed_issues":343,"state":"open","created_at":"2017-05-30T13:02:47Z","updated_at":"2018-02-13T17:30:15Z","due_on":null,"closed_at":null},"comments":6,"created_at":"2017-12-10T23:33:59Z","updated_at":"2018-02-13T17:42:56Z","closed_at":null,"author_association":"MEMBER","pull_request":{"url":"https://api.github.com/repos/coq/coq/pulls/6374","html_url":"https://github.com/coq/coq/pull/6374","diff_url":"https://github.com/coq/coq/pull/6374.diff","patch_url":"https://github.com/coq/coq/pull/6374.patch"},"body":"Instead of using a command-analysis heuristic, coqtop will now print\r\ngoals if the goal has changed. We use a fast goal comparison\r\nheuristic, but a more refined strategy would be possible.\r\n\r\nThis brings some [IMHO very welcome] change to PG and `-emacs`, which\r\nwill now disable the printing of goals. Now, instead of playing with\r\n`Set/Unset Silent` and a bunch of other hacks, PG can issue a `Show`\r\ncommand whenever it wishes to redisplay the goals.\r\n\r\nThis change will break PG, so we need to carefully coordinate this PR\r\nwith PG upstream (see ProofGeneral/PG#212).\r\n\r\nSome interesting further things to do:\r\n\r\n- Detect changes in nested proofs.\r\n- Uncouple the silent flag from \"print goals\"."},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/365345381","html_url":"https://github.com/coq/coq/pull/6374#issuecomment-365345381","issue_url":"https://api.github.com/repos/coq/coq/issues/6374","id":365345381,"user":{"login":"ejgallego","id":7192257,"avatar_url":"https://avatars2.githubusercontent.com/u/7192257?v=4","gravatar_id":"","url":"https://api.github.com/users/ejgallego","html_url":"https://github.com/ejgallego","followers_url":"https://api.github.com/users/ejgallego/followers","following_url":"https://api.github.com/users/ejgallego/following{/other_user}","gists_url":"https://api.github.com/users/ejgallego/gists{/gist_id}","starred_url":"https://api.github.com/users/ejgallego/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ejgallego/subscriptions","organizations_url":"https://api.github.com/users/ejgallego/orgs","repos_url":"https://api.github.com/users/ejgallego/repos","events_url":"https://api.github.com/users/ejgallego/events{/privacy}","received_events_url":"https://api.github.com/users/ejgallego/received_events","type":"User","site_admin":false},"created_at":"2018-02-13T17:42:56Z","updated_at":"2018-02-13T17:42:56Z","author_association":"MEMBER","body":"Ok so this is ready again. The main blocker for the merge is to know what the PG devs think. This basically switches Proof General from randomly reciving goals and having to recognize them to actually never receiving goals, so PG should request goal display when it wants."}}
{"actor":{"display_login":"ejgallego"}}