{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":18411972,"defaultBranch":"master","name":"FStar","ownerLogin":"FStarLang","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2014-04-03T17:32:49.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/7689927?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1714534230.0","currentOid":""},"activityList":{"items":[{"before":"66e947dad3587d35c3cbb7a24de98ce1008ba444","after":"bb9e55a2bf04feef4a26b7f8bdc69fc5e595dc57","ref":"refs/heads/master","pushedAt":"2024-05-04T01:37:13.000Z","pushType":"push","commitsCount":4,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"snap","shortMessageHtmlLink":"snap"}},{"before":"c990b3cae32f6ed6f10a7d6062c77f9af29150da","after":"bb9e55a2bf04feef4a26b7f8bdc69fc5e595dc57","ref":"refs/heads/guido_misc","pushedAt":"2024-05-04T01:17:52.000Z","pushType":"push","commitsCount":235,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"snap","shortMessageHtmlLink":"snap"}},{"before":"b410b9fa57af079327deb2adc4cd78c344b2ab75","after":"66e947dad3587d35c3cbb7a24de98ce1008ba444","ref":"refs/heads/master","pushedAt":"2024-05-03T15:44:49.000Z","pushType":"pr_merge","commitsCount":5,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"Merge pull request #3284 from mtzguido/fix\n\nFix #3266","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2277929098\" data-permission-text=\"Title is private\" data-url=\"https://github.com/FStarLang/FStar/issues/3284\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/FStarLang/FStar/pull/3284/hovercard\" href=\"https://github.com/FStarLang/FStar/pull/3284\">#3284</a> from mtzguido/fix"}},{"before":"b332ac1e7a608ace65ae9f16064e5303509f5324","after":"b410b9fa57af079327deb2adc4cd78c344b2ab75","ref":"refs/heads/master","pushedAt":"2024-05-03T07:25:07.000Z","pushType":"pr_merge","commitsCount":9,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"Merge pull request #3283 from mtzguido/misc\n\nMisc","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2277044336\" data-permission-text=\"Title is private\" data-url=\"https://github.com/FStarLang/FStar/issues/3283\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/FStarLang/FStar/pull/3283/hovercard\" href=\"https://github.com/FStarLang/FStar/pull/3283\">#3283</a> from mtzguido/misc"}},{"before":"3849844bc62687983bce7c4775bd69f7fa212938","after":null,"ref":"refs/heads/nik_restrict_injectivity","pushedAt":"2024-05-01T03:30:30.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"nikswamy","name":null,"path":"/nikswamy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6163359?s=80&v=4"}},{"before":"0996e782012571113969e19bfd7a1674e993ee39","after":"b332ac1e7a608ace65ae9f16064e5303509f5324","ref":"refs/heads/master","pushedAt":"2024-05-01T03:30:29.000Z","pushType":"pr_merge","commitsCount":61,"pusher":{"login":"nikswamy","name":null,"path":"/nikswamy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6163359?s=80&v=4"},"commit":{"message":"Merge pull request #3253 from FStarLang/nik_restrict_injectivity\n\nInjectivity of inductive types revisited","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2249134836\" data-permission-text=\"Title is private\" data-url=\"https://github.com/FStarLang/FStar/issues/3253\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/FStarLang/FStar/pull/3253/hovercard\" href=\"https://github.com/FStarLang/FStar/pull/3253\">#3253</a> from FStarLang/nik_restrict_injectivity"}},{"before":"3b730a9382129727a1ad42d7e05d5239d8c88c31","after":"3849844bc62687983bce7c4775bd69f7fa212938","ref":"refs/heads/nik_restrict_injectivity","pushedAt":"2024-05-01T03:04:10.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"Fix test\n\nFirst few were failing due to `is_inj` not being found. Use codes\nfor all of them.","shortMessageHtmlLink":"Fix test"}},{"before":"0d8be16a1e7e26be902992f6bbcbc5f84564e489","after":"3b730a9382129727a1ad42d7e05d5239d8c88c31","ref":"refs/heads/nik_restrict_injectivity","pushedAt":"2024-05-01T03:00:24.000Z","pushType":"push","commitsCount":7,"pusher":{"login":"nikswamy","name":null,"path":"/nikswamy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6163359?s=80&v=4"},"commit":{"message":"merge master","shortMessageHtmlLink":"merge master"}},{"before":"d75bfa695306a3708e9990b8907989e16532107e","after":"0996e782012571113969e19bfd7a1674e993ee39","ref":"refs/heads/master","pushedAt":"2024-05-01T02:04:22.000Z","pushType":"pr_merge","commitsCount":5,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"Merge pull request #3281 from mtzguido/repr_tac\n\nTactics.TypeRepr: add a tactic to translate inductives to a sums of products","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2272782746\" data-permission-text=\"Title is private\" data-url=\"https://github.com/FStarLang/FStar/issues/3281\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/FStarLang/FStar/pull/3281/hovercard\" href=\"https://github.com/FStarLang/FStar/pull/3281\">#3281</a> from mtzguido/repr_tac"}},{"before":"0d8be16a1e7e26be902992f6bbcbc5f84564e489","after":"b85bee9c3184653eef8397a465cba21d686e182b","ref":"refs/heads/nik_restrict_injectivity_wip","pushedAt":"2024-04-30T16:47:33.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"nikswamy","name":null,"path":"/nikswamy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6163359?s=80&v=4"},"commit":{"message":"eq_tm and eq_t disregard non-injective type parameters in equality tests of data constructors","shortMessageHtmlLink":"eq_tm and eq_t disregard non-injective type parameters in equality te…"}},{"before":"46b685506250f5a7c6f47e1f42dc452e968e3ec8","after":"0d8be16a1e7e26be902992f6bbcbc5f84564e489","ref":"refs/heads/nik_restrict_injectivity","pushedAt":"2024-04-30T05:18:04.000Z","pushType":"push","commitsCount":110,"pusher":{"login":"nikswamy","name":null,"path":"/nikswamy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6163359?s=80&v=4"},"commit":{"message":"Merge remote-tracking branch 'origin/master' into nik_restrict_injectivity_wip","shortMessageHtmlLink":"Merge remote-tracking branch 'origin/master' into nik_restrict_inject…"}},{"before":"596cc5c35c8eb458e32f74c630c006e4c78b218f","after":"0d8be16a1e7e26be902992f6bbcbc5f84564e489","ref":"refs/heads/nik_restrict_injectivity_wip","pushedAt":"2024-04-30T05:16:49.000Z","pushType":"push","commitsCount":8,"pusher":{"login":"nikswamy","name":null,"path":"/nikswamy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6163359?s=80&v=4"},"commit":{"message":"Merge remote-tracking branch 'origin/master' into nik_restrict_injectivity_wip","shortMessageHtmlLink":"Merge remote-tracking branch 'origin/master' into nik_restrict_inject…"}},{"before":"a94456863e3f971a7c63a64aca1a07d2cd9eb9a1","after":"d75bfa695306a3708e9990b8907989e16532107e","ref":"refs/heads/master","pushedAt":"2024-04-29T22:40:22.000Z","pushType":"pr_merge","commitsCount":7,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"Merge pull request #3278 from mtzguido/tcmisc\n\nSmall optimization in tcresolve, error message tweaks","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2270098560\" data-permission-text=\"Title is private\" data-url=\"https://github.com/FStarLang/FStar/issues/3278\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/FStarLang/FStar/pull/3278/hovercard\" href=\"https://github.com/FStarLang/FStar/pull/3278\">#3278</a> from mtzguido/tcmisc"}},{"before":"18b55b2a52b20e3cea968e8ce79e3f7b4609be8a","after":"596cc5c35c8eb458e32f74c630c006e4c78b218f","ref":"refs/heads/nik_restrict_injectivity_wip","pushedAt":"2024-04-29T18:07:56.000Z","pushType":"push","commitsCount":38,"pusher":{"login":"nikswamy","name":null,"path":"/nikswamy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6163359?s=80&v=4"},"commit":{"message":"another test","shortMessageHtmlLink":"another test"}},{"before":"ac9f6932a9c1ecb9942567b40adea9deaf42c05b","after":"a94456863e3f971a7c63a64aca1a07d2cd9eb9a1","ref":"refs/heads/master","pushedAt":"2024-04-29T15:54:48.000Z","pushType":"pr_merge","commitsCount":7,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"Merge pull request #3274 from mtzguido/debug\n\nMaking debug toggles more efficient","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2267129677\" data-permission-text=\"Title is private\" data-url=\"https://github.com/FStarLang/FStar/issues/3274\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/FStarLang/FStar/pull/3274/hovercard\" href=\"https://github.com/FStarLang/FStar/pull/3274\">#3274</a> from mtzguido/debug"}},{"before":"85a5dbcfbb9bf3d8d36d0074724a4b199a3194fc","after":null,"ref":"refs/heads/_aseem_pulse_interfaces","pushedAt":"2024-04-29T08:18:52.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"aseemr","name":"Aseem Rastogi","path":"/aseemr","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3921573?s=80&v=4"}},{"before":"df5b3dd12d0c2dfdb492971bd225e4232e6f708b","after":"ac9f6932a9c1ecb9942567b40adea9deaf42c05b","ref":"refs/heads/master","pushedAt":"2024-04-29T08:18:51.000Z","pushType":"pr_merge","commitsCount":17,"pusher":{"login":"aseemr","name":"Aseem Rastogi","path":"/aseemr","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3921573?s=80&v=4"},"commit":{"message":"Merge pull request #3270 from FStarLang/_aseem_pulse_interfaces\n\nSome enhancements in support of interfaces in Pulse","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2265444672\" data-permission-text=\"Title is private\" data-url=\"https://github.com/FStarLang/FStar/issues/3270\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/FStarLang/FStar/pull/3270/hovercard\" href=\"https://github.com/FStarLang/FStar/pull/3270\">#3270</a> from FStarLang/_aseem_pulse_interfaces"}},{"before":"67c99f4b526910ad9da0bae50ac1d126296a61fc","after":"85a5dbcfbb9bf3d8d36d0074724a4b199a3194fc","ref":"refs/heads/_aseem_pulse_interfaces","pushedAt":"2024-04-29T06:20:34.000Z","pushType":"push","commitsCount":17,"pusher":{"login":"aseemr","name":"Aseem Rastogi","path":"/aseemr","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3921573?s=80&v=4"},"commit":{"message":"some cleanup","shortMessageHtmlLink":"some cleanup"}},{"before":"85a6957f871f5b8c06e5dab3a30ed1eab8e4a18c","after":"df5b3dd12d0c2dfdb492971bd225e4232e6f708b","ref":"refs/heads/master","pushedAt":"2024-04-29T04:10:47.000Z","pushType":"pr_merge","commitsCount":8,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"Merge pull request #3277 from mtzguido/label_doc\n\nSyntax/SMT: Structure SMT errors (and Meta_labeled)","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2268073017\" data-permission-text=\"Title is private\" data-url=\"https://github.com/FStarLang/FStar/issues/3277\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/FStarLang/FStar/pull/3277/hovercard\" href=\"https://github.com/FStarLang/FStar/pull/3277\">#3277</a> from mtzguido/label_doc"}},{"before":"96f90842af8c0137bdee87ccb7bd3ea92485efb6","after":"85a6957f871f5b8c06e5dab3a30ed1eab8e4a18c","ref":"refs/heads/master","pushedAt":"2024-04-29T03:04:52.000Z","pushType":"pr_merge","commitsCount":4,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"Merge pull request #3276 from mtzguido/misc\n\nMisc","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2268022014\" data-permission-text=\"Title is private\" data-url=\"https://github.com/FStarLang/FStar/issues/3276\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/FStarLang/FStar/pull/3276/hovercard\" href=\"https://github.com/FStarLang/FStar/pull/3276\">#3276</a> from mtzguido/misc"}},{"before":"35f89bf0d24cec45b1b8df01681ab850e35d5869","after":"18b55b2a52b20e3cea968e8ce79e3f7b4609be8a","ref":"refs/heads/nik_restrict_injectivity_wip","pushedAt":"2024-04-28T20:09:30.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"nikswamy","name":null,"path":"/nikswamy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6163359?s=80&v=4"},"commit":{"message":"rlimit bump & retry on Lib.Vec.Lemmas","shortMessageHtmlLink":"rlimit bump &amp; retry on Lib.Vec.Lemmas"}},{"before":"d950b26a32da33add7f9788e53cd3a8219cd6b2d","after":"35f89bf0d24cec45b1b8df01681ab850e35d5869","ref":"refs/heads/nik_restrict_injectivity_wip","pushedAt":"2024-04-28T03:53:23.000Z","pushType":"push","commitsCount":4,"pusher":{"login":"nikswamy","name":null,"path":"/nikswamy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6163359?s=80&v=4"},"commit":{"message":"Merge remote-tracking branch 'origin/master' into nik_restrict_injectivity_wip","shortMessageHtmlLink":"Merge remote-tracking branch 'origin/master' into nik_restrict_inject…"}},{"before":"c9e98c764c952eaaba49a91282c8e32b09483768","after":"96f90842af8c0137bdee87ccb7bd3ea92485efb6","ref":"refs/heads/master","pushedAt":"2024-04-27T19:00:30.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"Merge pull request #3273 from mtzguido/ci\n\nbase.Dockerfile: remove libicu from install invocation","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2266850346\" data-permission-text=\"Title is private\" data-url=\"https://github.com/FStarLang/FStar/issues/3273\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/FStarLang/FStar/pull/3273/hovercard\" href=\"https://github.com/FStarLang/FStar/pull/3273\">#3273</a> from mtzguido/ci"}},{"before":null,"after":"fbc5e846030bd3576d8cfe275a840c741d681754","ref":"refs/heads/aseem_ci","pushedAt":"2024-04-27T11:48:36.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"aseemr","name":"Aseem Rastogi","path":"/aseemr","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3921573?s=80&v=4"},"commit":{"message":"CI is erroring out on package python3-distutils not installed, trying","shortMessageHtmlLink":"CI is erroring out on package python3-distutils not installed, trying"}},{"before":"a3bb2c03f05e23ed8369bb55279745eb78981fe6","after":"67c99f4b526910ad9da0bae50ac1d126296a61fc","ref":"refs/heads/_aseem_pulse_interfaces","pushedAt":"2024-04-27T11:26:48.000Z","pushType":"push","commitsCount":11,"pusher":{"login":"aseemr","name":"Aseem Rastogi","path":"/aseemr","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3921573?s=80&v=4"},"commit":{"message":"snap","shortMessageHtmlLink":"snap"}},{"before":"bcbff7cdffae2030d64279d25ff895052a4ab1fb","after":"d950b26a32da33add7f9788e53cd3a8219cd6b2d","ref":"refs/heads/nik_restrict_injectivity_wip","pushedAt":"2024-04-27T06:41:44.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"nikswamy","name":null,"path":"/nikswamy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6163359?s=80&v=4"},"commit":{"message":"tweak a test; we seemt to run out of stack a bit sooner on unembedding large lists; try to optimize eq_tm a bit","shortMessageHtmlLink":"tweak a test; we seemt to run out of stack a bit sooner on unembeddin…"}},{"before":"42bba1e4e2d0037ec53d7d48543eda4740465502","after":"bcbff7cdffae2030d64279d25ff895052a4ab1fb","ref":"refs/heads/nik_restrict_injectivity_wip","pushedAt":"2024-04-27T01:20:51.000Z","pushType":"push","commitsCount":26,"pusher":{"login":"nikswamy","name":null,"path":"/nikswamy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6163359?s=80&v=4"},"commit":{"message":"snap","shortMessageHtmlLink":"snap"}},{"before":"03d1b17e6720d2bc54315f93f7e7cd0865a2c614","after":"42bba1e4e2d0037ec53d7d48543eda4740465502","ref":"refs/heads/nik_restrict_injectivity_wip","pushedAt":"2024-04-27T01:05:55.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"nikswamy","name":null,"path":"/nikswamy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6163359?s=80&v=4"},"commit":{"message":"compute injective_type_params flag in phase2 only","shortMessageHtmlLink":"compute injective_type_params flag in phase2 only"}},{"before":"22319cb43f925b3f620c9d8590b1e2f7cfc067ea","after":"c9e98c764c952eaaba49a91282c8e32b09483768","ref":"refs/heads/master","pushedAt":"2024-04-27T00:53:32.000Z","pushType":"pr_merge","commitsCount":9,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"Merge pull request #3272 from mtzguido/no_fv_delta\n\nRemoving the fv_delta field","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2266607754\" data-permission-text=\"Title is private\" data-url=\"https://github.com/FStarLang/FStar/issues/3272\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/FStarLang/FStar/pull/3272/hovercard\" href=\"https://github.com/FStarLang/FStar/pull/3272\">#3272</a> from mtzguido/no_fv_delta"}},{"before":"a3ca82c2c3fd0f4ec31841e166b428e5469f4551","after":"03d1b17e6720d2bc54315f93f7e7cd0865a2c614","ref":"refs/heads/nik_restrict_injectivity_wip","pushedAt":"2024-04-27T00:20:35.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"nikswamy","name":null,"path":"/nikswamy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6163359?s=80&v=4"},"commit":{"message":"adding an injective_type_params field to Sig_inductive and Sig_datacon","shortMessageHtmlLink":"adding an injective_type_params field to Sig_inductive and Sig_datacon"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEQThe_AA","startCursor":null,"endCursor":null}},"title":"Activity · FStarLang/FStar"}