{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/7536","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/7536/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/7536/comments","events_url":"https://api.github.com/repos/coq/coq/issues/7536/events","html_url":"https://github.com/coq/coq/pull/7536","id":323689761,"node_id":"MDExOlB1bGxSZXF1ZXN0MTg4NDg1Njky","number":7536,"title":"Deprecate positive coinductive types","user":{"login":"ppedrot","id":1202327,"node_id":"MDQ6VXNlcjEyMDIzMjc=","avatar_url":"https://avatars1.githubusercontent.com/u/1202327?v=4","gravatar_id":"","url":"https://api.github.com/users/ppedrot","html_url":"https://github.com/ppedrot","followers_url":"https://api.github.com/users/ppedrot/followers","following_url":"https://api.github.com/users/ppedrot/following{/other_user}","gists_url":"https://api.github.com/users/ppedrot/gists{/gist_id}","starred_url":"https://api.github.com/users/ppedrot/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ppedrot/subscriptions","organizations_url":"https://api.github.com/users/ppedrot/orgs","repos_url":"https://api.github.com/users/ppedrot/repos","events_url":"https://api.github.com/users/ppedrot/events{/privacy}","received_events_url":"https://api.github.com/users/ppedrot/received_events","type":"User","site_admin":false},"labels":[{"id":485986179,"node_id":"MDU6TGFiZWw0ODU5ODYxNzk=","url":"https://api.github.com/repos/coq/coq/labels/kind:%20feature","name":"kind: feature","color":"0e8a16","default":false},{"id":572296906,"node_id":"MDU6TGFiZWw1NzIyOTY5MDY=","url":"https://api.github.com/repos/coq/coq/labels/needs:%20discussion","name":"needs: discussion","color":"bfd4f2","default":false}],"state":"open","locked":false,"assignee":{"login":"maximedenes","id":647105,"node_id":"MDQ6VXNlcjY0NzEwNQ==","avatar_url":"https://avatars1.githubusercontent.com/u/647105?v=4","gravatar_id":"","url":"https://api.github.com/users/maximedenes","html_url":"https://github.com/maximedenes","followers_url":"https://api.github.com/users/maximedenes/followers","following_url":"https://api.github.com/users/maximedenes/following{/other_user}","gists_url":"https://api.github.com/users/maximedenes/gists{/gist_id}","starred_url":"https://api.github.com/users/maximedenes/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/maximedenes/subscriptions","organizations_url":"https://api.github.com/users/maximedenes/orgs","repos_url":"https://api.github.com/users/maximedenes/repos","events_url":"https://api.github.com/users/maximedenes/events{/privacy}","received_events_url":"https://api.github.com/users/maximedenes/received_events","type":"User","site_admin":false},"assignees":[{"login":"maximedenes","id":647105,"node_id":"MDQ6VXNlcjY0NzEwNQ==","avatar_url":"https://avatars1.githubusercontent.com/u/647105?v=4","gravatar_id":"","url":"https://api.github.com/users/maximedenes","html_url":"https://github.com/maximedenes","followers_url":"https://api.github.com/users/maximedenes/followers","following_url":"https://api.github.com/users/maximedenes/following{/other_user}","gists_url":"https://api.github.com/users/maximedenes/gists{/gist_id}","starred_url":"https://api.github.com/users/maximedenes/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/maximedenes/subscriptions","organizations_url":"https://api.github.com/users/maximedenes/orgs","repos_url":"https://api.github.com/users/maximedenes/repos","events_url":"https://api.github.com/users/maximedenes/events{/privacy}","received_events_url":"https://api.github.com/users/maximedenes/received_events","type":"User","site_admin":false}],"milestone":{"url":"https://api.github.com/repos/coq/coq/milestones/7","html_url":"https://github.com/coq/coq/milestone/7","labels_url":"https://api.github.com/repos/coq/coq/milestones/7/labels","id":2647743,"node_id":"MDk6TWlsZXN0b25lMjY0Nzc0Mw==","number":7,"title":"8.9+beta1","description":"The date of the feature freeze has not been announced yet.","creator":{"login":"Zimmi48","id":1108325,"node_id":"MDQ6VXNlcjExMDgzMjU=","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},"open_issues":140,"closed_issues":342,"state":"open","created_at":"2017-07-18T15:03:25Z","updated_at":"2018-07-24T12:15:02Z","due_on":null,"closed_at":null},"comments":77,"created_at":"2018-05-16T16:11:14Z","updated_at":"2018-07-24T13:43:44Z","closed_at":null,"author_association":"MEMBER","pull_request":{"url":"https://api.github.com/repos/coq/coq/pulls/7536","html_url":"https://github.com/coq/coq/pull/7536","diff_url":"https://github.com/coq/coq/pull/7536.diff","patch_url":"https://github.com/coq/coq/pull/7536.patch"},"body":"Adding a warning when declaring positive coinductive types.\r\n\r\nSuch types a fundamentally wrong and are known to break subject reduction of CIC. We advertise for the use of negative coinductive types instead, i.e. defined by means of primitive records.\r\n\r\nDue to the fact that the kernel is currently unable to handle mutually corecursive negative records, we currently only produce the warning on coinductive types which only made of one block, which is the vast majority of the uses. When this is solved, the warning needs to be adapted accordingly.\r\n\r\nWe adapted the standard library and tests to use primitive corecursive records.\r\n\r\nMost of the changes are actually due to the Coq \"design pattern\" that CoInductive types do not generate induction schemes.\r\n\r\nThe only part of the stdlib that was really using them is the Stream library, which is probably not much used in the wild.\r\n\r\nDepending on the case, tests were either adapted, or removed if they were made moot by the transition, e.g. if they relied on properties not holding with negative coinductive types.\r\n\r\nThis was documented both in the Coq reference manual and in the CHANGES.\r\n"},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/407411378","html_url":"https://github.com/coq/coq/pull/7536#issuecomment-407411378","issue_url":"https://api.github.com/repos/coq/coq/issues/7536","id":407411378,"node_id":"MDEyOklzc3VlQ29tbWVudDQwNzQxMTM3OA==","user":{"login":"ppedrot","id":1202327,"node_id":"MDQ6VXNlcjEyMDIzMjc=","avatar_url":"https://avatars1.githubusercontent.com/u/1202327?v=4","gravatar_id":"","url":"https://api.github.com/users/ppedrot","html_url":"https://github.com/ppedrot","followers_url":"https://api.github.com/users/ppedrot/followers","following_url":"https://api.github.com/users/ppedrot/following{/other_user}","gists_url":"https://api.github.com/users/ppedrot/gists{/gist_id}","starred_url":"https://api.github.com/users/ppedrot/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ppedrot/subscriptions","organizations_url":"https://api.github.com/users/ppedrot/orgs","repos_url":"https://api.github.com/users/ppedrot/repos","events_url":"https://api.github.com/users/ppedrot/events{/privacy}","received_events_url":"https://api.github.com/users/ppedrot/received_events","type":"User","site_admin":false},"created_at":"2018-07-24T13:43:44Z","updated_at":"2018-07-24T13:43:44Z","author_association":"MEMBER","body":"@mattam82 Just as `Case` but the return clause is not a function `λ(x : indices)(p : I p x). R`, rather an array of functions corresponding to each η-expanded type."}}
{"actor":{"display_login":"ppedrot"}}