{"action":"created","issue":{"url":"https://api.github.com/repos/leanprover/mathlib/issues/151","repository_url":"https://api.github.com/repos/leanprover/mathlib","labels_url":"https://api.github.com/repos/leanprover/mathlib/issues/151/labels{/name}","comments_url":"https://api.github.com/repos/leanprover/mathlib/issues/151/comments","events_url":"https://api.github.com/repos/leanprover/mathlib/issues/151/events","html_url":"https://github.com/leanprover/mathlib/pull/151","id":328896323,"node_id":"MDExOlB1bGxSZXF1ZXN0MTkyMjg5MjEw","number":151,"title":"feat(ext): ext fails if it can't make progress","user":{"login":"semorrison","id":477956,"node_id":"MDQ6VXNlcjQ3Nzk1Ng==","avatar_url":"https://avatars1.githubusercontent.com/u/477956?v=4","gravatar_id":"","url":"https://api.github.com/users/semorrison","html_url":"https://github.com/semorrison","followers_url":"https://api.github.com/users/semorrison/followers","following_url":"https://api.github.com/users/semorrison/following{/other_user}","gists_url":"https://api.github.com/users/semorrison/gists{/gist_id}","starred_url":"https://api.github.com/users/semorrison/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/semorrison/subscriptions","organizations_url":"https://api.github.com/users/semorrison/orgs","repos_url":"https://api.github.com/users/semorrison/repos","events_url":"https://api.github.com/users/semorrison/events{/privacy}","received_events_url":"https://api.github.com/users/semorrison/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2018-06-04T03:23:43Z","updated_at":"2018-06-04T12:28:26Z","closed_at":null,"author_association":"CONTRIBUTOR","pull_request":{"url":"https://api.github.com/repos/leanprover/mathlib/pulls/151","html_url":"https://github.com/leanprover/mathlib/pull/151","diff_url":"https://github.com/leanprover/mathlib/pull/151.diff","patch_url":"https://github.com/leanprover/mathlib/pull/151.patch"},"body":"Per discussion with @cipher1024 on zulip."},"comment":{"url":"https://api.github.com/repos/leanprover/mathlib/issues/comments/394337194","html_url":"https://github.com/leanprover/mathlib/pull/151#issuecomment-394337194","issue_url":"https://api.github.com/repos/leanprover/mathlib/issues/151","id":394337194,"node_id":"MDEyOklzc3VlQ29tbWVudDM5NDMzNzE5NA==","user":{"login":"cipher1024","id":71008,"node_id":"MDQ6VXNlcjcxMDA4","avatar_url":"https://avatars0.githubusercontent.com/u/71008?v=4","gravatar_id":"","url":"https://api.github.com/users/cipher1024","html_url":"https://github.com/cipher1024","followers_url":"https://api.github.com/users/cipher1024/followers","following_url":"https://api.github.com/users/cipher1024/following{/other_user}","gists_url":"https://api.github.com/users/cipher1024/gists{/gist_id}","starred_url":"https://api.github.com/users/cipher1024/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/cipher1024/subscriptions","organizations_url":"https://api.github.com/users/cipher1024/orgs","repos_url":"https://api.github.com/users/cipher1024/repos","events_url":"https://api.github.com/users/cipher1024/events{/privacy}","received_events_url":"https://api.github.com/users/cipher1024/received_events","type":"User","site_admin":false},"created_at":"2018-06-04T12:28:26Z","updated_at":"2018-06-04T12:28:26Z","author_association":"CONTRIBUTOR","body":"Is there any test case for under `test/` for `ext`? It's not a rule of mathlib but I find it a useful thing to keep. In change sets, that already gives you a diff on how the use of the tactic will change or at least just an example use of the tactic."}}
{"actor":{"display_login":"cipher1024"}}