{"action":"created","issue":{"url":"https://api.github.com/repos/ejgallego/coq-serapi/issues/11","repository_url":"https://api.github.com/repos/ejgallego/coq-serapi","labels_url":"https://api.github.com/repos/ejgallego/coq-serapi/issues/11/labels{/name}","comments_url":"https://api.github.com/repos/ejgallego/coq-serapi/issues/11/comments","events_url":"https://api.github.com/repos/ejgallego/coq-serapi/issues/11/events","html_url":"https://github.com/ejgallego/coq-serapi/issues/11","id":160195034,"number":11,"title":"How does EditAt work? / EditAt limitations","user":{"login":"cpitclaudel","id":8181630,"avatar_url":"https://avatars.githubusercontent.com/u/8181630?v=3","gravatar_id":"","url":"https://api.github.com/users/cpitclaudel","html_url":"https://github.com/cpitclaudel","followers_url":"https://api.github.com/users/cpitclaudel/followers","following_url":"https://api.github.com/users/cpitclaudel/following{/other_user}","gists_url":"https://api.github.com/users/cpitclaudel/gists{/gist_id}","starred_url":"https://api.github.com/users/cpitclaudel/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/cpitclaudel/subscriptions","organizations_url":"https://api.github.com/users/cpitclaudel/orgs","repos_url":"https://api.github.com/users/cpitclaudel/repos","events_url":"https://api.github.com/users/cpitclaudel/events{/privacy}","received_events_url":"https://api.github.com/users/cpitclaudel/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/ejgallego/coq-serapi/labels/in-progress","name":"in-progress","color":"5319e7"},{"url":"https://api.github.com/repos/ejgallego/coq-serapi/labels/question","name":"question","color":"cc317c"},{"url":"https://api.github.com/repos/ejgallego/coq-serapi/labels/upstream","name":"upstream","color":"fbca04"}],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":40,"created_at":"2016-06-14T14:25:32Z","updated_at":"2016-07-19T11:00:12Z","closed_at":null,"body":"Assume the following document:\r\n\r\n```\r\nLemma a : True.\r\n  idtac.\r\n  urgh.\r\n  idtac.\r\n```\r\n\r\nI run the following commands in sertop.el:\r\n\r\n```lisp\r\n(add-lemma (Control (StmAdd 1 2 \"Lemma a : True.\")))\r\n  (Answer add-lemma Ack)\r\n  (Answer add-lemma\r\n          (StmAdded 3\r\n                    ((fname \"\")\r\n                     (line_nb 1)\r\n                     (bol_pos 0)\r\n                     (line_nb_last 1)\r\n                     (bol_pos_last 0)\r\n                     (bp 0)\r\n                     (ep 15))\r\n                    NewTip))\r\n  (Answer add-lemma Completed)\r\n(add-idtac (Control (StmAdd 1 3 \"\\n  idtac.\")))\r\n  (Answer add-idtac Ack)\r\n  (Answer add-idtac\r\n          (StmAdded 4\r\n                    ((fname \"\")\r\n                     (line_nb 1)\r\n                     (bol_pos 0)\r\n                     (line_nb_last 1)\r\n                     (bol_pos_last 0)\r\n                     (bp 3)\r\n                     (ep 9))\r\n                    NewTip))\r\n  (Answer add-idtac Completed)\r\n(add-urgh (Control (StmAdd 1 4 \"\\n  urgh.\")))\r\n  (Answer add-urgh Ack)\r\n  (Answer add-urgh\r\n          (StmAdded 5\r\n                    ((fname \"\")\r\n                     (line_nb 1)\r\n                     (bol_pos 0)\r\n                     (line_nb_last 1)\r\n                     (bol_pos_last 0)\r\n                     (bp 3)\r\n                     (ep 8))\r\n                    NewTip))\r\n  (Answer add-urgh Completed)\r\n(add-idtac-2 (Control (StmAdd 1 5 \"\\n  idtac.\")))\r\n  (Answer add-idtac-2 Ack)\r\n  (Answer add-idtac-2\r\n          (StmAdded 6\r\n                    ((fname \"\")\r\n                     (line_nb 1)\r\n                     (bol_pos 0)\r\n                     (line_nb_last 1)\r\n                     (bol_pos_last 0)\r\n                     (bp 3)\r\n                     (ep 9))\r\n                    NewTip))\r\n  (Answer add-idtac-2 Completed)\r\n(observe (Control (StmObserve 6)))\r\n  (Answer observe Ack)\r\n  (Feedback\r\n   ((id\r\n     (State 6))\r\n    (contents\r\n     (ProcessingIn master))\r\n    (route 0)))\r\n  (Feedback\r\n   ((id\r\n     (State 5))\r\n    (contents\r\n     (ProcessingIn master))\r\n    (route 0)))\r\n  (Feedback\r\n   ((id\r\n     (State 4))\r\n    (contents\r\n     (ProcessingIn master))\r\n    (route 0)))\r\n  (Feedback\r\n   ((id\r\n     (State 3))\r\n    (contents\r\n     (ProcessingIn master))\r\n    (route 0)))\r\n  (Feedback\r\n   ((id\r\n     (State 2))\r\n    (contents Processed)\r\n    (route 0)))\r\n  (Feedback\r\n   ((id\r\n     (State 3))\r\n    (contents Processed)\r\n    (route 0)))\r\n  (Feedback\r\n   ((id\r\n     (State 4))\r\n    (contents Processed)\r\n    (route 0)))\r\n  (Feedback\r\n   ((id\r\n     (State 5))\r\n    (contents\r\n     (ErrorMsg\r\n      ((fname \"\")\r\n       (line_nb 1)\r\n       (bol_pos 0)\r\n       (line_nb_last 1)\r\n       (bol_pos_last 0)\r\n       (bp 3)\r\n       (ep 7))\r\n      \"Error: The reference urgh was not found in the current environment.\"))\r\n    (route 0)))\r\n  (Answer observe\r\n          (CoqExn\r\n           (\"Cerrors.EvaluatedError(_, 0)\")))\r\n```\r\n\r\nAt this point, how can I know which sentences are invalid? I tried EditAt:\r\n\r\n```\r\n(edit-at (Control (StmEditAt 4)))\r\n  (Answer edit-at Ack)\r\n  (Feedback\r\n   ((id\r\n     (State 4))\r\n    (contents Processed)\r\n    (route 0)))\r\n  (Answer edit-at\r\n          (StmEdited NewTip))\r\n  (Answer edit-at Completed)\r\n```\r\n\r\nBut I'm not sure how to interpret the result. Does this mean that everything after state 4 needs to be invalidated?\r\n\r\nThanks!"},"comment":{"url":"https://api.github.com/repos/ejgallego/coq-serapi/issues/comments/233599026","html_url":"https://github.com/ejgallego/coq-serapi/issues/11#issuecomment-233599026","issue_url":"https://api.github.com/repos/ejgallego/coq-serapi/issues/11","id":233599026,"user":{"login":"gares","id":1013846,"avatar_url":"https://avatars.githubusercontent.com/u/1013846?v=3","gravatar_id":"","url":"https://api.github.com/users/gares","html_url":"https://github.com/gares","followers_url":"https://api.github.com/users/gares/followers","following_url":"https://api.github.com/users/gares/following{/other_user}","gists_url":"https://api.github.com/users/gares/gists{/gist_id}","starred_url":"https://api.github.com/users/gares/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/gares/subscriptions","organizations_url":"https://api.github.com/users/gares/orgs","repos_url":"https://api.github.com/users/gares/repos","events_url":"https://api.github.com/users/gares/events{/privacy}","received_events_url":"https://api.github.com/users/gares/received_events","type":"User","site_admin":false},"created_at":"2016-07-19T11:00:12Z","updated_at":"2016-07-19T11:00:12Z","body":"It is like commenting out all the text between the last added sentence in the re-opened proof and the Qed, add the Qed, re-open another proof."}}
{"actor":{"display_login":"gares"}}