{"action":"created","issue":{"url":"https://api.github.com/repos/ProofGeneral/PG/issues/235","repository_url":"https://api.github.com/repos/ProofGeneral/PG","labels_url":"https://api.github.com/repos/ProofGeneral/PG/issues/235/labels{/name}","comments_url":"https://api.github.com/repos/ProofGeneral/PG/issues/235/comments","events_url":"https://api.github.com/repos/ProofGeneral/PG/issues/235/events","html_url":"https://github.com/ProofGeneral/PG/issues/235","id":301358035,"number":235,"title":"ProofGeneral stops printing Goal state on Coq error","user":{"login":"HeikoBecker","id":3237993,"avatar_url":"https://avatars0.githubusercontent.com/u/3237993?v=4","gravatar_id":"","url":"https://api.github.com/users/HeikoBecker","html_url":"https://github.com/HeikoBecker","followers_url":"https://api.github.com/users/HeikoBecker/followers","following_url":"https://api.github.com/users/HeikoBecker/following{/other_user}","gists_url":"https://api.github.com/users/HeikoBecker/gists{/gist_id}","starred_url":"https://api.github.com/users/HeikoBecker/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/HeikoBecker/subscriptions","organizations_url":"https://api.github.com/users/HeikoBecker/orgs","repos_url":"https://api.github.com/users/HeikoBecker/repos","events_url":"https://api.github.com/users/HeikoBecker/events{/privacy}","received_events_url":"https://api.github.com/users/HeikoBecker/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":1,"created_at":"2018-03-01T10:47:08Z","updated_at":"2018-03-01T13:38:14Z","closed_at":null,"author_association":"NONE","body":"I am runnning Coq 8.7.2 and the latest ProofGeneral master. \r\nThe issue occurs on large files that contain a proof that cannot be finished when running C-c C-b and needs to be fixed manually.\r\nI also have to step back to the beginning of the buffer and then consume manually until the point where the proof breaks using C-c C-n.\r\n\r\nHere is a minimal emacs config that can be used to showcase the problem:\r\n\r\n     ;;Proof General\r\n     ;; Open .v files with Proof General's Coq mode\r\n     (load \"~/.emacs.d/lisp/PG/generic/proof-site\")\r\n\r\nand a test file (test.v):\r\n\r\n    Definition test (a:nat) (b:nat) := a.\r\n    \r\n    Lemma test_is_a :\r\n      forall a b, test a b = a.\r\n    Proof.\r\n      intros.\r\n      unfold test2.\r\n      auto.\r\n\r\nWhen pressing C-c C-b to evaluate the buffer, Coq will complain that `test2` cannot be unfolded.\r\nWhen stepping back until the beginning of the Lemma the `*goals*` buffer is not refreshed and stays empty. I can however print the state with C-c C-p. Stepping one step further in the proof will not continue displaying the goal.\r\n\r\nTo get `*goals*` to display goals again, I have to step back before the definition of `test` and then run over the file stepwise with C-c C-n. \r\n"},"comment":{"url":"https://api.github.com/repos/ProofGeneral/PG/issues/comments/369593639","html_url":"https://github.com/ProofGeneral/PG/issues/235#issuecomment-369593639","issue_url":"https://api.github.com/repos/ProofGeneral/PG/issues/235","id":369593639,"user":{"login":"HeikoBecker","id":3237993,"avatar_url":"https://avatars0.githubusercontent.com/u/3237993?v=4","gravatar_id":"","url":"https://api.github.com/users/HeikoBecker","html_url":"https://github.com/HeikoBecker","followers_url":"https://api.github.com/users/HeikoBecker/followers","following_url":"https://api.github.com/users/HeikoBecker/following{/other_user}","gists_url":"https://api.github.com/users/HeikoBecker/gists{/gist_id}","starred_url":"https://api.github.com/users/HeikoBecker/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/HeikoBecker/subscriptions","organizations_url":"https://api.github.com/users/HeikoBecker/orgs","repos_url":"https://api.github.com/users/HeikoBecker/repos","events_url":"https://api.github.com/users/HeikoBecker/events{/privacy}","received_events_url":"https://api.github.com/users/HeikoBecker/received_events","type":"User","site_admin":false},"created_at":"2018-03-01T13:38:13Z","updated_at":"2018-03-01T13:38:13Z","author_association":"NONE","body":"I get the error when using \r\n    \r\n    commit 5e7566e54842fb198a6f68abb7c624b53a488038\r\n    Author: Erik Martin-Dorel <erik@martin-dorel.org>\r\n    Date:   Tue Feb 20 10:30:00 2018 +0100\r\n\r\n    Bind C-c C-m (= C-c RET) to proof-goto-point [tty] (#228)\r\n\r\n    Close ProofGeneral/PG#31\r\n"}}
{"actor":{"display_login":"HeikoBecker"}}