{"action":"closed","issue":{"url":"https://api.github.com/repos/Zimmi48/bugzilla-test/issues/4060","repository_url":"https://api.github.com/repos/Zimmi48/bugzilla-test","labels_url":"https://api.github.com/repos/Zimmi48/bugzilla-test/issues/4060/labels{/name}","comments_url":"https://api.github.com/repos/Zimmi48/bugzilla-test/issues/4060/comments","events_url":"https://api.github.com/repos/Zimmi48/bugzilla-test/issues/4060/events","html_url":"https://github.com/Zimmi48/bugzilla-test/issues/4060","id":253120579,"number":4060,"title":"Anomaly: File \"library/heads.ml\", line 71, characters 25-31: Assertion failed","user":{"login":"Zimmi48","id":1108325,"avatar_url":"https://avatars2.githubusercontent.com/u/1108325?v=4","gravatar_id":"","url":"https://api.github.com/users/Zimmi48","html_url":"https://github.com/Zimmi48","followers_url":"https://api.github.com/users/Zimmi48/followers","following_url":"https://api.github.com/users/Zimmi48/following{/other_user}","gists_url":"https://api.github.com/users/Zimmi48/gists{/gist_id}","starred_url":"https://api.github.com/users/Zimmi48/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/Zimmi48/subscriptions","organizations_url":"https://api.github.com/users/Zimmi48/orgs","repos_url":"https://api.github.com/users/Zimmi48/repos","events_url":"https://api.github.com/users/Zimmi48/events{/privacy}","received_events_url":"https://api.github.com/users/Zimmi48/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2017-08-26T20:22:20Z","updated_at":"2017-08-26T20:22:24Z","closed_at":"2017-08-26T20:22:24Z","body":"Note: the issue was created automatically with bugzilla2github tool\n\n# Bugzilla Bug ID: 4060\nDate: 2015-02-18 19:25:43 +0100\nFrom: @_Lionel-Rieg\nTo:   \nCC:   coq-bugs-redist@lists.gforge.inria.fr, @_herbelin, @_ppedrot\n\nSee also:     https://coq.inria.fr/bugs/show_bug.cgi?id=3767\nLast updated: 2017-05-20 13:19:54 +0200\n\n\n## Bugzilla Comment ID: 9479\nDate: 2015-02-18 19:25:43 +0100\nFrom: @_Lionel-Rieg\n\nCreated attachment 552\nBacktrace of the error\n\nI have seen this error at an [Hypotheses] statement juste after a opening a section.  I think I have seen it a few times before but it is not reproducible.\nRestarting the Coq process on the file solves the problem but not rolling back to a point before the section.\n\nIn attachelmnt is a backtrace of the anomaly.\n\n> Attached file: bug.txt (text/plain, 2561 bytes)\n> Description:   Backtrace of the error\n\n\n## Bugzilla Comment ID: 9714\nDate: 2015-03-01 15:38:50 +0100\nFrom: @_ppedrot\n\nIf you encounter it again, can you give us the file you're working on?\n\n\n## Bugzilla Comment ID: 10256\nDate: 2015-04-23 16:02:40 +0200\nFrom: @_Lionel-Rieg\n\n(In reply to comment #1)\n> If you encounter it again, can you give us the file you're working on?\n\nHere is a tarball containing an excerpt of the project on which I got this error again and the backtrace.\nThe bug does not seem to be not reproducible but it happened the right after the instance [spectrum_of_compat] when trying to validate the definition of [idle].\n\nTo solve the issue it is necessary to restart the coq process, just reverting it (even up to the top of the buffer) is not enough.\n\nI am using the git version 2a5fd12d597d4337810ae367ea3a49720ee3d80c.\n\n\n## Bugzilla Comment ID: 10257\nDate: 2015-04-23 16:03:48 +0200\nFrom: @_Lionel-Rieg\n\nCreated attachment 580\nThe aforementioned tarball.\n\n> Attached file: bug4060.tgz (application/x-compressed-tar, 92160 bytes)\n> Description:   The aforementioned tarball.\n\n\n## Bugzilla Comment ID: 16350\nDate: 2017-05-20 13:16:00 +0200\nFrom: @_herbelin\n\nHi Lionel, I just checked with 8.6 and trunk and no anomaly shows up. However, I had to make some changes to pass to 8.6 from the pre-8.5 development version that you apparently used. You probably already made an upgrade, but I found:\n- refine shelving a goal which was not unshelved\n- the activation of \"Bracketing Last Introduction Pattern\"\n- kFair now in Prop (singleton recursive coinductive type), resulting in H being named X.\n\nI can't tell what fixed it exactly though.\n\n"}}
{"actor":{"display_login":"Zimmi48"}}