{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/236","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/236/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/236/comments","events_url":"https://api.github.com/repos/coq/coq/issues/236/events","html_url":"https://github.com/coq/coq/pull/236","id":163580316,"number":236,"title":"Fix -profile-ltac flag","user":{"login":"JasonGross","id":396076,"avatar_url":"https://avatars.githubusercontent.com/u/396076?v=3","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},"labels":[{"url":"https://api.github.com/repos/coq/coq/labels/8.6","name":"8.6","color":"0e8a16"}],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":4,"created_at":"2016-07-03T21:18:20Z","updated_at":"2016-08-18T16:11:45Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/coq/coq/pulls/236","html_url":"https://github.com/coq/coq/pull/236","diff_url":"https://github.com/coq/coq/pull/236.diff","patch_url":"https://github.com/coq/coq/pull/236.patch"},"body":"This is probably not the Right way to fix it, but I don't know how to tell Coq that it shouldn't ignore side effects of tactics on the document state when in profiling mode.  (@gares? @ppedrot?)\r\n\r\nEven if the fix for the flag itself doesn't get merged, the comment-only changes in the debug-printing should probably get merged, and the testing file should also probably be merged.  (This is on top of #217 because I need the support I added there to testing infrastructure.)\r\n\r\nThis probably doesn't need any kind of copyright change, since I'm doing this on my own time on my own machine."},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/240774066","html_url":"https://github.com/coq/coq/pull/236#issuecomment-240774066","issue_url":"https://api.github.com/repos/coq/coq/issues/236","id":240774066,"user":{"login":"JasonGross","id":396076,"avatar_url":"https://avatars.githubusercontent.com/u/396076?v=3","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":"2016-08-18T16:11:45Z","updated_at":"2016-08-18T16:11:45Z","body":"The code works, and it's better than nothing, given that the current state of things is \"`-profile-ltac` claims that no tactics were run and that the total time spent in tactics is 0\".   Is that enough to get it merged?  (Once this is merged, I'll probably be making use of `-profile-ltac` on every build, so hopefully I'll catch any remaining wrinkles in the results.)\r\n\r\n\r\n\r\nThe issue is that `Defined` and `Qed` reset the document state to the way it was before the proof started, add the proof to the global env, and then replay any vernaculars declared as side-effectful (or something similar; I'm sure @gares has a better way of describing this).  Since tactics are not side-effectful, this means that every `Defined` and `Qed` wipe the profiling data that was gathered during execution of the tactic script.\r\n\r\nTo get around this, I make a copy of the profiling data stack which is not synchronized with the document, and update this one in parallel with the synchronized one.  (The unsynchronized one is used only for the `-profile-ltac` flag, currently, while the synchronized one is used to display things during document execution.  This is not great, but it's better than what's there now, and I'm waiting on feedback from @gares (or anyone else), on how to synchronize the profiling data with backtracking, but not wipe it when proofs are closed.)\r\n\r\nSince @tebbi makes use of imperative update of structures with multiple pointers to them, I took some care to make sure that the root node of the profiling data is shared between the synchronized and unsynchronized versions in `reset_profile` (but perhaps this is not necessary, since the code works, and I think sharing is lost when the state is restored), and I also take some care to guard against double-counting when references are shared, by checks of physical equality.\r\n\r\nThe rest of the changes at the bottom are just factoring the printing methods over which profile data to display."}}
{"actor":{"display_login":"JasonGross"}}