{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/7409","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/7409/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/7409/comments","events_url":"https://api.github.com/repos/coq/coq/issues/7409/events","html_url":"https://github.com/coq/coq/issues/7409","id":319699341,"number":7409,"title":"What is the appropriate level of abstraction on which a sentence location should be attached?","user":{"login":"herbelin","id":460771,"avatar_url":"https://avatars1.githubusercontent.com/u/460771?v=4","gravatar_id":"","url":"https://api.github.com/users/herbelin","html_url":"https://github.com/herbelin","followers_url":"https://api.github.com/users/herbelin/followers","following_url":"https://api.github.com/users/herbelin/following{/other_user}","gists_url":"https://api.github.com/users/herbelin/gists{/gist_id}","starred_url":"https://api.github.com/users/herbelin/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/herbelin/subscriptions","organizations_url":"https://api.github.com/users/herbelin/orgs","repos_url":"https://api.github.com/users/herbelin/repos","events_url":"https://api.github.com/users/herbelin/events{/privacy}","received_events_url":"https://api.github.com/users/herbelin/received_events","type":"User","site_admin":false},"labels":[{"id":735167060,"url":"https://api.github.com/repos/coq/coq/labels/kind:%20question","name":"kind: question","color":"4a9ae0","default":false}],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2018-05-02T20:25:12Z","updated_at":"2018-05-02T20:33:58Z","closed_at":null,"author_association":"OWNER","body":"Currently, there is a `locate_if_not_already` which adds a location to errors of `Vernacentries.interp` in case there is not already a finer location.\r\n\r\nIn the `stm`, there is `process_transaction`, `query`, `reach` and `perform` which call `Vernacentries.interp`. The method `process_transaction` comes with a location but not `query`, `reach` and `perform`. There are parts of `process_transaction` which are a priori liable to raise errors but which do not call `interp` and which may then not necessarily be encapsulated with a location. Shouldn't they be encapsulated?\r\n\r\nAt the current time, I did not investigate the purpose of each part of `process_transaction`, the purpose of `query` and the one of `perform`, and the one of `reach`, assuming that more experts than me could explain.\r\n\r\nSo, the question remains open at this time (for at least @ejgallego and me, see discussion at #7134): what are the exact entry points where a sentence location is relevant."},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/386111798","html_url":"https://github.com/coq/coq/issues/7409#issuecomment-386111798","issue_url":"https://api.github.com/repos/coq/coq/issues/7409","id":386111798,"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-05-02T20:33:58Z","updated_at":"2018-05-02T20:33:58Z","author_association":"MEMBER","body":"@herbelin , the location of a sentence is stored in the `aast` type in the STM. This is the canonical one; and all the methods above have access to it except `process_transaction` which is the one creating the node itself.\r\n\r\nAs for `locate_if_not_already`, let me remark that this is used in error handling. Usually, exception contain location information as to refine the part of the sub-sentence that should be displayed. If no such location information is present, then the method tries to attach the location of the sentence.\r\n\r\nNow we need to distinguish two scenarios as the current situation is derived from them and a bit tricky:\r\n- The STM was supposed to provide asynchronous error handling. In this scenario, every error comes with a location, which is added by the document traversal. Due to the way document traversal works this is hard to do and it doesn't always work. Also, if there is not location info the span id can be used to retrieve the location, modulo bugs such as #6884 .\r\n\r\n- As for exceptions, again it seem the place to add this information would be the document traversal code, however this is a bit tricky to hook today. In my opinion the best place may be `stm_vernac_interp`.\r\n"}}
{"actor":{"display_login":"ejgallego"}}