{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":10340342,"defaultBranch":"master","name":"coq","ownerLogin":"ppedrot","currentUserCanPush":false,"isFork":true,"isEmpty":false,"createdAt":"2013-05-28T16:46:07.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/1202327?v=4","public":true,"private":false,"isOrgOwned":false},"refInfo":{"name":"","listCacheKey":"v0:1719260572.0","currentOid":""},"activityList":{"items":[{"before":null,"after":"bcea77b3570a90a54b839e3941358f1ea5123e3b","ref":"refs/heads/cbv-stack-list","pushedAt":"2024-06-24T20:22:52.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"ppedrot","name":"Pierre-Marie Pédrot","path":"/ppedrot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1202327?s=80&v=4"},"commit":{"message":"Small inlining of array-manipulating functions in Cbv.","shortMessageHtmlLink":"Small inlining of array-manipulating functions in Cbv."}},{"before":"fb624bc915dc4b66369322e2878c035a12e5e36f","after":"62f487344be062fd897a22a13f87530db136b92a","ref":"refs/heads/template-no-sup-constraint-kernel","pushedAt":"2024-06-24T19:41:40.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"ppedrot","name":"Pierre-Marie Pédrot","path":"/ppedrot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1202327?s=80&v=4"},"commit":{"message":"Laxer kernel typing rule for template inductive types.\n\nUnder the view that template types are an optimization of sort-polymorphic\ninductive types, the requirement that the sort of an argument lives below\nthe global template universe of the corresponding parameter is spurious.","shortMessageHtmlLink":"Laxer kernel typing rule for template inductive types."}},{"before":"228048e6b95b5dd7a6ce543e17eafe11e2c261f5","after":"ed15f2c6cb7a714a088d0c31c42c3e41a22cb069","ref":"refs/heads/template-linear-levels","pushedAt":"2024-06-24T12:37:50.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"ppedrot","name":"Pierre-Marie Pédrot","path":"/ppedrot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1202327?s=80&v=4"},"commit":{"message":"Forbid non-linear template polymorphic universe levels.\n\nThis can break subject reduction in the future poly-like model. In practice,\nit is not possible to trigger this code path without explicit fidgetting\nwith universe levels in the inductive declaration.","shortMessageHtmlLink":"Forbid non-linear template polymorphic universe levels."}},{"before":"48bea8e47058e8322e5020ff36bceaea95248077","after":null,"ref":"refs/heads/clenv-missing-centralize-api","pushedAt":"2024-06-24T11:50:19.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"ppedrot","name":"Pierre-Marie Pédrot","path":"/ppedrot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1202327?s=80&v=4"}},{"before":null,"after":"228048e6b95b5dd7a6ce543e17eafe11e2c261f5","ref":"refs/heads/template-linear-levels","pushedAt":"2024-06-22T13:44:32.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"ppedrot","name":"Pierre-Marie Pédrot","path":"/ppedrot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1202327?s=80&v=4"},"commit":{"message":"Forbid non-linear template polymorphic universe levels.\n\nThis can break subject reduction in the future poly-like model. In practice,\nit is not possible to trigger this code path without explicit fidgetting\nwith universe levels in the inductive declaration.","shortMessageHtmlLink":"Forbid non-linear template polymorphic universe levels."}},{"before":null,"after":"fb624bc915dc4b66369322e2878c035a12e5e36f","ref":"refs/heads/template-no-sup-constraint-kernel","pushedAt":"2024-06-22T12:53:19.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"ppedrot","name":"Pierre-Marie Pédrot","path":"/ppedrot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1202327?s=80&v=4"},"commit":{"message":"Laxer kernel typing rule for template inductive types.\n\nUnder the view that template types are an optimization of sort-polymorphic\ninductive types, the requirement that the sort of an argument lives below\nthe global template universe of the corresponding parameter is spurious.","shortMessageHtmlLink":"Laxer kernel typing rule for template inductive types."}},{"before":"ce840d04090831403b246850e632abae2ca59e88","after":null,"ref":"refs/heads/template-strict-level-constraint","pushedAt":"2024-06-22T12:52:38.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"ppedrot","name":"Pierre-Marie Pédrot","path":"/ppedrot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1202327?s=80&v=4"}},{"before":"403c62d5bd8c5d97d2582f499eecc1cb233a6368","after":"bb86b07c01edd644dd774625b13b414fefc75f21","ref":"refs/heads/template-no-sup-constraint","pushedAt":"2024-06-21T13:16:39.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"ppedrot","name":"Pierre-Marie Pédrot","path":"/ppedrot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1202327?s=80&v=4"},"commit":{"message":"Fix Scheme Equality with template poly","shortMessageHtmlLink":"Fix Scheme Equality with template poly"}},{"before":"8e8165f8327e5130898fc91386f3db0fac12bc54","after":"ce840d04090831403b246850e632abae2ca59e88","ref":"refs/heads/template-strict-level-constraint","pushedAt":"2024-06-21T13:10:28.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"ppedrot","name":"Pierre-Marie Pédrot","path":"/ppedrot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1202327?s=80&v=4"},"commit":{"message":"Forbid inflationary universes to be template polymorphic.\n\nTemplate inductive types with a signature Type@{u} -> Type@{u+1} allowed\nto make the algebraic increment to increase arbitrarily. Despite being\na very weak invariant, most parts of the code expect at most a +1 increment\nin algebraic universes. We prevent a source of generation of such ill-formed\nalgebraic types by forbidding template polymorphic arities to return a +n\non a template universe.\n\nFixes #19230: Anomaly with explicit universe +1 and template polymorphism.","shortMessageHtmlLink":"Forbid inflationary universes to be template polymorphic."}},{"before":"9f79877c53ba512f84cfb6ca0b90f2eb601ed77b","after":null,"ref":"refs/heads/template-strict-level-position","pushedAt":"2024-06-21T13:09:34.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"ppedrot","name":"Pierre-Marie Pédrot","path":"/ppedrot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1202327?s=80&v=4"}},{"before":null,"after":"8e8165f8327e5130898fc91386f3db0fac12bc54","ref":"refs/heads/template-strict-level-constraint","pushedAt":"2024-06-20T20:33:40.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"ppedrot","name":"Pierre-Marie Pédrot","path":"/ppedrot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1202327?s=80&v=4"},"commit":{"message":"Forbid inflationary universes to be template polymorphic.\n\nTemplate inductive types with a signature Type@{u} -> Type@{u+1} allowed\nto make the algebraic increment to increase arbitrarily. Despite being\na very weak invariant, most parts of the code expect at most a +1 increment\nin algebraic universes. We prevent a source of generation of such ill-formed\nalgebraic types by forbidding template polymorphic arities to return a +n\non a template universe.\n\nFixes #19230: Anomaly with explicit universe +1 and template polymorphism.","shortMessageHtmlLink":"Forbid inflationary universes to be template polymorphic."}},{"before":"a7e11654b7b75dd65cdef5599c398e6a0250cbe4","after":"9f79877c53ba512f84cfb6ca0b90f2eb601ed77b","ref":"refs/heads/template-strict-level-position","pushedAt":"2024-06-20T19:57:56.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"ppedrot","name":"Pierre-Marie Pédrot","path":"/ppedrot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1202327?s=80&v=4"},"commit":{"message":"Stricter criterion for template universe levels.\n\nWe restrict template levels so that we can substitute them with arbitrary\nalgebraic levels. The criterion is an overapproximation, and should be\nremoved when algebraic universes are made first-class in the kernel.\n\nThe upper layers are actually already implementing this check, so that the\nkernel could not have received ill-formed template inductive types from\nuser input alone.","shortMessageHtmlLink":"Stricter criterion for template universe levels."}},{"before":"688343b05074ba6e2eb9a43081b0e6f313173b20","after":"403c62d5bd8c5d97d2582f499eecc1cb233a6368","ref":"refs/heads/template-no-sup-constraint","pushedAt":"2024-06-20T12:21:08.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"SkySkimmer","name":"Gaëtan Gilbert","path":"/SkySkimmer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2461932?s=80&v=4"},"commit":{"message":"Fix Scheme Equality with template poly","shortMessageHtmlLink":"Fix Scheme Equality with template poly"}},{"before":null,"after":"a7e11654b7b75dd65cdef5599c398e6a0250cbe4","ref":"refs/heads/template-strict-level-position","pushedAt":"2024-06-20T12:18:49.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"ppedrot","name":"Pierre-Marie Pédrot","path":"/ppedrot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1202327?s=80&v=4"},"commit":{"message":"Stricter criterion for template universe levels.\n\nWe restrict template levels so that we can substitute them with arbitrary\nalgebraic levels. The criterion is an overapproximation, and should be\nremoved when algebraic universes are made first-class in the kernel.\n\nThe upper layers are actually already implementing this check, so that the\nkernel could not have received ill-formed template inductive types from\nuser input alone.","shortMessageHtmlLink":"Stricter criterion for template universe levels."}},{"before":"39d2b20e4f6ee51d5f353d57f01ce8441e468867","after":"688343b05074ba6e2eb9a43081b0e6f313173b20","ref":"refs/heads/template-no-sup-constraint","pushedAt":"2024-06-19T13:33:35.000Z","pushType":"push","commitsCount":4,"pusher":{"login":"SkySkimmer","name":"Gaëtan Gilbert","path":"/SkySkimmer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2461932?s=80&v=4"},"commit":{"message":"Fix Scheme Equality with template poly","shortMessageHtmlLink":"Fix Scheme Equality with template poly"}},{"before":"c9e52cc2edc64b2aa9bedd0f0642aa73cffe422a","after":"39d2b20e4f6ee51d5f353d57f01ce8441e468867","ref":"refs/heads/template-no-sup-constraint","pushedAt":"2024-06-19T12:45:09.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"ppedrot","name":"Pierre-Marie Pédrot","path":"/ppedrot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1202327?s=80&v=4"},"commit":{"message":"Fix Typing.checked_appvect vs template poly","shortMessageHtmlLink":"Fix Typing.checked_appvect vs template poly"}},{"before":"8b02a7d61e9398f45c9446a17bf7e3b66d88165d","after":null,"ref":"refs/heads/rm-gintuition","pushedAt":"2024-06-19T09:39:51.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"ppedrot","name":"Pierre-Marie Pédrot","path":"/ppedrot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1202327?s=80&v=4"}},{"before":"0bf495b581512b0c5b3a5420c5941bcb634c85bc","after":null,"ref":"refs/heads/bench-metacoq-equations-608","pushedAt":"2024-06-19T09:37:51.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"ppedrot","name":"Pierre-Marie Pédrot","path":"/ppedrot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1202327?s=80&v=4"}},{"before":"2a74f51a35be66fbd5922154fb46894138b86459","after":"48bea8e47058e8322e5020ff36bceaea95248077","ref":"refs/heads/clenv-missing-centralize-api","pushedAt":"2024-06-18T15:10:12.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"ppedrot","name":"Pierre-Marie Pédrot","path":"/ppedrot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1202327?s=80&v=4"},"commit":{"message":"Adding overlays.","shortMessageHtmlLink":"Adding overlays."}},{"before":"b5e590541b19887fc07abfe496253c785a388f6e","after":"c9e52cc2edc64b2aa9bedd0f0642aa73cffe422a","ref":"refs/heads/template-no-sup-constraint","pushedAt":"2024-06-18T15:00:49.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"ppedrot","name":"Pierre-Marie Pédrot","path":"/ppedrot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1202327?s=80&v=4"},"commit":{"message":"Fix Typing.checked_appvect vs template poly","shortMessageHtmlLink":"Fix Typing.checked_appvect vs template poly"}},{"before":"8824dd298366d1fae42257e797a8a0549a9f67aa","after":"b5e590541b19887fc07abfe496253c785a388f6e","ref":"refs/heads/template-no-sup-constraint","pushedAt":"2024-06-18T14:31:01.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"SkySkimmer","name":"Gaëtan Gilbert","path":"/SkySkimmer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2461932?s=80&v=4"},"commit":{"message":"pretyping doesn't generate extra template poly constraints","shortMessageHtmlLink":"pretyping doesn't generate extra template poly constraints"}},{"before":"ec90e8a595a3691a26f81971483d80cfb72013c9","after":"8824dd298366d1fae42257e797a8a0549a9f67aa","ref":"refs/heads/template-no-sup-constraint","pushedAt":"2024-06-18T13:48:51.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"SkySkimmer","name":"Gaëtan Gilbert","path":"/SkySkimmer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2461932?s=80&v=4"},"commit":{"message":"pretyping doesn't generate extra template poly constraints","shortMessageHtmlLink":"pretyping doesn't generate extra template poly constraints"}},{"before":"6a192d804f3efc43b73ab2f38ae013bacd2ee0f2","after":"ec90e8a595a3691a26f81971483d80cfb72013c9","ref":"refs/heads/template-no-sup-constraint","pushedAt":"2024-06-18T13:20:00.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"ppedrot","name":"Pierre-Marie Pédrot","path":"/ppedrot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1202327?s=80&v=4"},"commit":{"message":"Reduce further the code generating useless template constraints.","shortMessageHtmlLink":"Reduce further the code generating useless template constraints."}},{"before":"e4b984d0d92eb52252c196c63e0a436c132fd581","after":"6a192d804f3efc43b73ab2f38ae013bacd2ee0f2","ref":"refs/heads/template-no-sup-constraint","pushedAt":"2024-06-18T12:49:40.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"ppedrot","name":"Pierre-Marie Pédrot","path":"/ppedrot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1202327?s=80&v=4"},"commit":{"message":"Less useless template constraints in Typing.","shortMessageHtmlLink":"Less useless template constraints in Typing."}},{"before":"657d656f79428f0a4b28c2807bf1681ffcefe7b3","after":"e4b984d0d92eb52252c196c63e0a436c132fd581","ref":"refs/heads/template-no-sup-constraint","pushedAt":"2024-06-18T08:21:49.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"ppedrot","name":"Pierre-Marie Pédrot","path":"/ppedrot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1202327?s=80&v=4"},"commit":{"message":"Laxer kernel typing rule for template inductive types.\n\nUnder the view that template types are an optimization of sort-polymorphic\ninductive types, the requirement that the sort of an argument lives below\nthe global template universe of the corresponding parameter is spurious.","shortMessageHtmlLink":"Laxer kernel typing rule for template inductive types."}},{"before":"3e2b6acbf05cfdd83fa6399706177d2151bb373c","after":"657d656f79428f0a4b28c2807bf1681ffcefe7b3","ref":"refs/heads/template-no-sup-constraint","pushedAt":"2024-06-18T08:17:03.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"ppedrot","name":"Pierre-Marie Pédrot","path":"/ppedrot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1202327?s=80&v=4"},"commit":{"message":"Laxer kernel typing rule for template inductive types.\n\nUnder the view that template types are an optimization of sort-polymorphic\ninductive types, the requirement that the sort of an argument lives below\nthe global template universe of the corresponding parameter is spurious.","shortMessageHtmlLink":"Laxer kernel typing rule for template inductive types."}},{"before":"f05943d54e04afd92ed847d97fc72e88dfa79c71","after":"3e2b6acbf05cfdd83fa6399706177d2151bb373c","ref":"refs/heads/template-no-sup-constraint","pushedAt":"2024-06-18T07:40:07.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"ppedrot","name":"Pierre-Marie Pédrot","path":"/ppedrot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1202327?s=80&v=4"},"commit":{"message":"Laxer kernel typing rule for template inductive types.\n\nUnder the view that template types are an optimization of sort-polymorphic\ninductive types, the requirement that the sort of an argument lives below\nthe global template universe of the corresponding parameter is spurious.","shortMessageHtmlLink":"Laxer kernel typing rule for template inductive types."}},{"before":"c01c3340f26348ea72bcbe05903f23153ff089f7","after":"f05943d54e04afd92ed847d97fc72e88dfa79c71","ref":"refs/heads/template-no-sup-constraint","pushedAt":"2024-06-17T20:42:05.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"ppedrot","name":"Pierre-Marie Pédrot","path":"/ppedrot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1202327?s=80&v=4"},"commit":{"message":"Laxer kernel typing rule for template inductive types.\n\nUnder the view that template types are an optimization of sort-polymorphic\ninductive types, the requirement that the sort of an argument lives below\nthe global template universe of the corresponding parameter is spurious.","shortMessageHtmlLink":"Laxer kernel typing rule for template inductive types."}},{"before":null,"after":"2a74f51a35be66fbd5922154fb46894138b86459","ref":"refs/heads/clenv-missing-centralize-api","pushedAt":"2024-06-17T16:07:04.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"ppedrot","name":"Pierre-Marie Pédrot","path":"/ppedrot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1202327?s=80&v=4"},"commit":{"message":"Finer API for Clenv.clenv_missing.","shortMessageHtmlLink":"Finer API for Clenv.clenv_missing."}},{"before":"3e4e56818f12eef4767b61e001f40d3f3382b40a","after":null,"ref":"refs/heads/infer-conv-generic-delay","pushedAt":"2024-06-17T08:27:46.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"ppedrot","name":"Pierre-Marie Pédrot","path":"/ppedrot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1202327?s=80&v=4"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEbeo5mAA","startCursor":null,"endCursor":null}},"title":"Activity · ppedrot/coq"}