{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":120383901,"defaultBranch":"master","name":"pumpkin-pi","ownerLogin":"uwplse","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2018-02-06T01:19:18.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/5273459?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1678925357.0","currentOid":""},"activityList":{"items":[{"before":"d181fb2f668ddd0006e339aeb22a0b5da58ceb9a","after":"a066716a1a99061b4d2f69aac210c62bf48de7a3","ref":"refs/heads/two-list-queue","pushedAt":"2024-04-24T22:39:31.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"cosmoviola","name":"Cosmo Viola","path":"/cosmoviola","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4514500?s=80&v=4"},"commit":{"message":"Add repair for lists to vectors with trivial eta.","shortMessageHtmlLink":"Add repair for lists to vectors with trivial eta."}},{"before":"f905844fee03417b54808f3bcc7de53ed4dcad49","after":"d181fb2f668ddd0006e339aeb22a0b5da58ceb9a","ref":"refs/heads/two-list-queue","pushedAt":"2024-02-29T10:46:59.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"cosmoviola","name":"Cosmo Viola","path":"/cosmoviola","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4514500?s=80&v=4"},"commit":{"message":"Add source of repair of add+Z0R.","shortMessageHtmlLink":"Add source of repair of add+Z0R."}},{"before":"7b633a6fa869c08feaf8627ae12a61f5d6961dbf","after":"f905844fee03417b54808f3bcc7de53ed4dcad49","ref":"refs/heads/two-list-queue","pushedAt":"2024-02-29T05:57:06.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"InnovativeInventor","name":"Max Fan","path":"/InnovativeInventor","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/20117409?s=80&v=4"},"commit":{"message":"Take TLQ out of modules","shortMessageHtmlLink":"Take TLQ out of modules"}},{"before":"79f210af2d78cfdc7b7a39eee18fb9edc9df0fa8","after":"7b633a6fa869c08feaf8627ae12a61f5d6961dbf","ref":"refs/heads/two-list-queue","pushedAt":"2024-02-29T05:53:20.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"InnovativeInventor","name":"Max Fan","path":"/InnovativeInventor","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/20117409?s=80&v=4"},"commit":{"message":"Get OLQ out of module","shortMessageHtmlLink":"Get OLQ out of module"}},{"before":"f711d7abe9a8551330f9286005de064fe27ca1cc","after":"79f210af2d78cfdc7b7a39eee18fb9edc9df0fa8","ref":"refs/heads/two-list-queue","pushedAt":"2024-02-29T05:26:12.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"cosmoviola","name":"Cosmo Viola","path":"/cosmoviola","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4514500?s=80&v=4"},"commit":{"message":"Fix ZZ in function names instead of Z.","shortMessageHtmlLink":"Fix ZZ in function names instead of Z."}},{"before":"3f45a67b6f92fe0edef90a244d4d6b5e8d3f1481","after":"f711d7abe9a8551330f9286005de064fe27ca1cc","ref":"refs/heads/two-list-queue","pushedAt":"2024-02-29T03:44:59.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"cosmoviola","name":"Cosmo Viola","path":"/cosmoviola","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4514500?s=80&v=4"},"commit":{"message":"Add iotas for queue example in Agda.","shortMessageHtmlLink":"Add iotas for queue example in Agda."}},{"before":"b70e67b01dfe6127f3b2425f0acb3268ae27cc24","after":"3f45a67b6f92fe0edef90a244d4d6b5e8d3f1481","ref":"refs/heads/two-list-queue","pushedAt":"2024-02-29T03:28:18.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"cosmoviola","name":"Cosmo Viola","path":"/cosmoviola","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4514500?s=80&v=4"},"commit":{"message":"Add reverse iota rules to agda int example.","shortMessageHtmlLink":"Add reverse iota rules to agda int example."}},{"before":"f2d93ec72d9ab28053bfcf723d37fcf1fd715833","after":"b70e67b01dfe6127f3b2425f0acb3268ae27cc24","ref":"refs/heads/two-list-queue","pushedAt":"2024-02-29T02:31:16.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"InnovativeInventor","name":"Max Fan","path":"/InnovativeInventor","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/20117409?s=80&v=4"},"commit":{"message":"Make naming scheme line up with Agda example","shortMessageHtmlLink":"Make naming scheme line up with Agda example"}},{"before":"a531f3c138fc2ebb4dddfdded5fe3062bd58e2fc","after":"f2d93ec72d9ab28053bfcf723d37fcf1fd715833","ref":"refs/heads/two-list-queue","pushedAt":"2024-02-29T02:24:55.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"InnovativeInventor","name":"Max Fan","path":"/InnovativeInventor","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/20117409?s=80&v=4"},"commit":{"message":"Merge branch 'two-list-queue' of github.com:uwplse/pumpkin-pi into two-list-queue","shortMessageHtmlLink":"Merge branch 'two-list-queue' of github.com:uwplse/pumpkin-pi into tw…"}},{"before":"f4fcc21a8c65c63a147ebb955b171d9e7d14fe05","after":"a531f3c138fc2ebb4dddfdded5fe3062bd58e2fc","ref":"refs/heads/two-list-queue","pushedAt":"2024-02-29T00:10:37.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"cosmoviola","name":"Cosmo Viola","path":"/cosmoviola","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4514500?s=80&v=4"},"commit":{"message":"Merge branch 'two-list-queue' of github.com:uwplse/pumpkin-pi into two-list-queue","shortMessageHtmlLink":"Merge branch 'two-list-queue' of github.com:uwplse/pumpkin-pi into tw…"}},{"before":"aa0d98d75a42d651456646c6d02678413d209752","after":"f4fcc21a8c65c63a147ebb955b171d9e7d14fe05","ref":"refs/heads/two-list-queue","pushedAt":"2024-02-28T21:05:00.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"InnovativeInventor","name":"Max Fan","path":"/InnovativeInventor","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/20117409?s=80&v=4"},"commit":{"message":"Fix broken links in README","shortMessageHtmlLink":"Fix broken links in README"}},{"before":"97779a71e573c7484b95470673a33dbd4360600f","after":"aa0d98d75a42d651456646c6d02678413d209752","ref":"refs/heads/two-list-queue","pushedAt":"2024-02-28T21:03:37.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"InnovativeInventor","name":"Max Fan","path":"/InnovativeInventor","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/20117409?s=80&v=4"},"commit":{"message":"Fix broken link in README","shortMessageHtmlLink":"Fix broken link in README"}},{"before":"4d139a3c9688c9e7f0b1180f821c9273411ed9ca","after":"97779a71e573c7484b95470673a33dbd4360600f","ref":"refs/heads/two-list-queue","pushedAt":"2024-02-28T21:02:02.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"InnovativeInventor","name":"Max Fan","path":"/InnovativeInventor","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/20117409?s=80&v=4"},"commit":{"message":"Add setoid repair tests","shortMessageHtmlLink":"Add setoid repair tests"}},{"before":"74987ade0def290b2099a3906ed36f5c91a683d9","after":"4d139a3c9688c9e7f0b1180f821c9273411ed9ca","ref":"refs/heads/two-list-queue","pushedAt":"2024-02-28T20:52:52.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"InnovativeInventor","name":"Max Fan","path":"/InnovativeInventor","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/20117409?s=80&v=4"},"commit":{"message":"Add links to cubical agda files","shortMessageHtmlLink":"Add links to cubical agda files"}},{"before":"366eda33d5e4343eb3df925cdccef873648a812a","after":"74987ade0def290b2099a3906ed36f5c91a683d9","ref":"refs/heads/two-list-queue","pushedAt":"2024-02-28T20:45:35.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"InnovativeInventor","name":"Max Fan","path":"/InnovativeInventor","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/20117409?s=80&v=4"},"commit":{"message":"Add links to cubical agda files","shortMessageHtmlLink":"Add links to cubical agda files"}},{"before":"5ef9eb3d8f38619788d8bcb7ca2008ced6c9b385","after":"366eda33d5e4343eb3df925cdccef873648a812a","ref":"refs/heads/two-list-queue","pushedAt":"2024-02-28T20:38:00.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"InnovativeInventor","name":"Max Fan","path":"/InnovativeInventor","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/20117409?s=80&v=4"},"commit":{"message":"Add first pass for build script and quotients README","shortMessageHtmlLink":"Add first pass for build script and quotients README"}},{"before":"d6ac371cdf5903945da4939742f48b69fdbd93e5","after":"5ef9eb3d8f38619788d8bcb7ca2008ced6c9b385","ref":"refs/heads/two-list-queue","pushedAt":"2024-02-28T09:15:40.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"cosmoviola","name":"Cosmo Viola","path":"/cosmoviola","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4514500?s=80&v=4"},"commit":{"message":"Fix wrong type in a comment.","shortMessageHtmlLink":"Fix wrong type in a comment."}},{"before":"726e871b05e11f4bad701903e4c6db0120648389","after":"d6ac371cdf5903945da4939742f48b69fdbd93e5","ref":"refs/heads/two-list-queue","pushedAt":"2024-02-28T09:12:48.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"cosmoviola","name":"Cosmo Viola","path":"/cosmoviola","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4514500?s=80&v=4"},"commit":{"message":"Explicitly declare instances of Setoid even though we don't use them.\n\nAdd comment explaining use of PERs.","shortMessageHtmlLink":"Explicitly declare instances of Setoid even though we don't use them."}},{"before":"7aa08c26011d2b26689457b6e0b4f24e65381e3a","after":"726e871b05e11f4bad701903e4c6db0120648389","ref":"refs/heads/two-list-queue","pushedAt":"2024-02-27T23:22:37.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"cosmoviola","name":"Cosmo Viola","path":"/cosmoviola","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4514500?s=80&v=4"},"commit":{"message":"Demonstrate that repaired proofs have types convertible to the types we want.","shortMessageHtmlLink":"Demonstrate that repaired proofs have types convertible to the types …"}},{"before":"aafbd2c133d7ec1da7b0dbd861839a17a205cc5d","after":"7aa08c26011d2b26689457b6e0b4f24e65381e3a","ref":"refs/heads/two-list-queue","pushedAt":"2024-02-27T11:39:57.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"cosmoviola","name":"Cosmo Viola","path":"/cosmoviola","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4514500?s=80&v=4"},"commit":{"message":"Pretend this commit was bundled with the previous one.","shortMessageHtmlLink":"Pretend this commit was bundled with the previous one."}},{"before":"fd9b2db63262ca6421cb374d55eb77e2e9e3e391","after":"aafbd2c133d7ec1da7b0dbd861839a17a205cc5d","ref":"refs/heads/two-list-queue","pushedAt":"2024-02-27T11:38:52.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"cosmoviola","name":"Cosmo Viola","path":"/cosmoviola","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4514500?s=80&v=4"},"commit":{"message":"Add proof of fastAdd0LGZ. Add comment that manually annotating functions and theorems is consistent with prior work.","shortMessageHtmlLink":"Add proof of fastAdd0LGZ. Add comment that manually annotating functi…"}},{"before":"1afe6993b840188c87955629eab7a50183b1d2b3","after":"fd9b2db63262ca6421cb374d55eb77e2e9e3e391","ref":"refs/heads/two-list-queue","pushedAt":"2024-02-27T07:33:17.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"cosmoviola","name":"Cosmo Viola","path":"/cosmoviola","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4514500?s=80&v=4"},"commit":{"message":"Remove unused imports. Move imports to top of file.","shortMessageHtmlLink":"Remove unused imports. Move imports to top of file."}},{"before":"9a35ae0e429f88efabca6da85f80c96bd19ab84f","after":"1afe6993b840188c87955629eab7a50183b1d2b3","ref":"refs/heads/two-list-queue","pushedAt":"2024-02-26T22:54:34.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"tlringer","name":"Talia Ringer","path":"/tlringer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9851391?s=80&v=4"},"commit":{"message":"remove extra preprocess not needed","shortMessageHtmlLink":"remove extra preprocess not needed"}},{"before":"9d89f4707313f9ab17b1092a5859167e9450203a","after":"9a35ae0e429f88efabca6da85f80c96bd19ab84f","ref":"refs/heads/two-list-queue","pushedAt":"2024-02-26T22:50:44.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"tlringer","name":"Talia Ringer","path":"/tlringer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9851391?s=80&v=4"},"commit":{"message":"unset irrelevant options","shortMessageHtmlLink":"unset irrelevant options"}},{"before":"57488d7ef4244113664c510ef883498fff78dd73","after":"9d89f4707313f9ab17b1092a5859167e9450203a","ref":"refs/heads/two-list-queue","pushedAt":"2024-02-26T22:47:17.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"tlringer","name":"Talia Ringer","path":"/tlringer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9851391?s=80&v=4"},"commit":{"message":"Remove unused code","shortMessageHtmlLink":"Remove unused code"}},{"before":"686d9aa6576ed72c771f8b827463199af762b15a","after":"57488d7ef4244113664c510ef883498fff78dd73","ref":"refs/heads/two-list-queue","pushedAt":"2024-02-26T13:13:38.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"cosmoviola","name":"Cosmo Viola","path":"/cosmoviola","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4514500?s=80&v=4"},"commit":{"message":"Implement lifting two list queue functions. Add comments to the file.","shortMessageHtmlLink":"Implement lifting two list queue functions. Add comments to the file."}},{"before":"bcd358e458e2a462a6507a31592aaa9dbf2a351b","after":"686d9aa6576ed72c771f8b827463199af762b15a","ref":"refs/heads/two-list-queue","pushedAt":"2024-02-26T07:16:05.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"cosmoviola","name":"Cosmo Viola","path":"/cosmoviola","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4514500?s=80&v=4"},"commit":{"message":"Add fast-slow study to integer example. Add documentation to integer example.","shortMessageHtmlLink":"Add fast-slow study to integer example. Add documentation to integer …"}},{"before":"a3176cb78ec2887628279b7523a6e311388d3018","after":"bcd358e458e2a462a6507a31592aaa9dbf2a351b","ref":"refs/heads/two-list-queue","pushedAt":"2024-02-25T20:15:29.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"tlringer","name":"Talia Ringer","path":"/tlringer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9851391?s=80&v=4"},"commit":{"message":"remove excess print debugging","shortMessageHtmlLink":"remove excess print debugging"}},{"before":"e6a014219ce03e13a68892488b5f0a631b53f15c","after":"a3176cb78ec2887628279b7523a6e311388d3018","ref":"refs/heads/two-list-queue","pushedAt":"2024-02-25T20:11:45.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"tlringer","name":"Talia Ringer","path":"/tlringer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9851391?s=80&v=4"},"commit":{"message":"Fix one more debruijn bug, get proper_test working","shortMessageHtmlLink":"Fix one more debruijn bug, get proper_test working"}},{"before":"425a07edf63965f598ea744d0fd7ce607c4d3ce9","after":"e6a014219ce03e13a68892488b5f0a631b53f15c","ref":"refs/heads/two-list-queue","pushedAt":"2024-02-25T20:05:34.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"tlringer","name":"Talia Ringer","path":"/tlringer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9851391?s=80&v=4"},"commit":{"message":"lmao Rel 2 works","shortMessageHtmlLink":"lmao Rel 2 works"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEOZxBjwA","startCursor":null,"endCursor":null}},"title":"Activity · uwplse/pumpkin-pi"}