{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":173480464,"defaultBranch":"master","name":"perennial","ownerLogin":"mit-pdos","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2019-03-02T17:54:02.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/12404246?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1726106335.0","currentOid":""},"activityList":{"items":[{"before":"d4f705d8625545b06c53d6f97e1c1daae1850b5a","after":"4cf5afdd3a13a90be80962f1ce4120286cc10fd9","ref":"refs/heads/coq/tested","pushedAt":"2024-09-20T07:04:30.000Z","pushType":"push","commitsCount":7,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Checkpoint paxos resources/invariants","shortMessageHtmlLink":"Checkpoint paxos resources/invariants"}},{"before":"dc070af59c19d84a745688bafc12c4678d8b379a","after":"4cf5afdd3a13a90be80962f1ce4120286cc10fd9","ref":"refs/heads/master","pushedAt":"2024-09-19T16:36:57.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"yunshengtw","name":"Yun-Sheng Chang","path":"/yunshengtw","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/29350735?s=80&v=4"},"commit":{"message":"Checkpoint paxos resources/invariants","shortMessageHtmlLink":"Checkpoint paxos resources/invariants"}},{"before":"2dc24e591400750c12b5cbc42ac70cc41067101e","after":"dc070af59c19d84a745688bafc12c4678d8b379a","ref":"refs/heads/master","pushedAt":"2024-09-19T15:52:44.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"upamanyus","name":"Upamanyu Sharma","path":"/upamanyus","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10575923?s=80&v=4"},"commit":{"message":"store_ty takes 2 separate arguments instead of a pair","shortMessageHtmlLink":"store_ty takes 2 separate arguments instead of a pair"}},{"before":"5cbed0bcfb110a89e74f22de4bffb3c7dd42bc70","after":"2dc24e591400750c12b5cbc42ac70cc41067101e","ref":"refs/heads/master","pushedAt":"2024-09-19T14:15:55.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"tchajed","name":"Tej Chajed","path":"/tchajed","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1255037?s=80&v=4"},"commit":{"message":"[ci]: test Coq 8.20 instead of 8.19","shortMessageHtmlLink":"[ci]: test Coq 8.20 instead of 8.19"}},{"before":"d4f705d8625545b06c53d6f97e1c1daae1850b5a","after":"5cbed0bcfb110a89e74f22de4bffb3c7dd42bc70","ref":"refs/heads/master","pushedAt":"2024-09-19T04:40:24.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"upamanyus","name":"Upamanyu Sharma","path":"/upamanyus","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10575923?s=80&v=4"},"commit":{"message":"Make wp_store/wp_load much faster by first doing a `wp_bind`;\n\ne.g. cases that used to take 2 seconds now take ~40ms. Previously, the\ntactics were slow because they would keep trying to eapply\ntac_wp_whatever wihle walking down the possible evaluation contexts.\nWith a longer ectx list at the end, there would be more failed attempts,\nand the top-level tactic was slow.","shortMessageHtmlLink":"Make wp_store/wp_load much faster by first doing a wp_bind;"}},{"before":"9ae5f9cebda20a415dc266cc5288c7c47f4c9f51","after":"d4f705d8625545b06c53d6f97e1c1daae1850b5a","ref":"refs/heads/coq/tested","pushedAt":"2024-09-18T07:04:25.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Merge pull request #117 from proux01/stdlib_repo\n\nAdapt to https://github.com/coq/coq/pull/19530","shortMessageHtmlLink":"Merge pull request #117 from proux01/stdlib_repo"}},{"before":"9ae5f9cebda20a415dc266cc5288c7c47f4c9f51","after":"d4f705d8625545b06c53d6f97e1c1daae1850b5a","ref":"refs/heads/master","pushedAt":"2024-09-17T12:40:15.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"tchajed","name":"Tej Chajed","path":"/tchajed","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1255037?s=80&v=4"},"commit":{"message":"Merge pull request #117 from proux01/stdlib_repo\n\nAdapt to https://github.com/coq/coq/pull/19530","shortMessageHtmlLink":"Merge pull request #117 from proux01/stdlib_repo"}},{"before":"ab6c5093026bc18cfc4689be4cda9e5fb2614a97","after":"9ae5f9cebda20a415dc266cc5288c7c47f4c9f51","ref":"refs/heads/coq/tested","pushedAt":"2024-09-12T07:04:38.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Bump std++ and Iris\n\nNeed some fixes for std++ moving string functions into a module","shortMessageHtmlLink":"Bump std++ and Iris"}},{"before":"753ba18dc59b3f45edf3821e23388fd7df64e508","after":null,"ref":"refs/heads/dependabot/submodules/external/iris-6f24ed4","pushedAt":"2024-09-12T01:58:55.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"dependabot[bot]","name":null,"path":"/apps/dependabot","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/29110?s=80&v=4"}},{"before":"ff50067d468b4d3703da4aa4dcb39e628665bde7","after":null,"ref":"refs/heads/dependabot/submodules/external/stdpp-a1a12e0","pushedAt":"2024-09-12T01:58:50.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"dependabot[bot]","name":null,"path":"/apps/dependabot","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/29110?s=80&v=4"}},{"before":"ab6c5093026bc18cfc4689be4cda9e5fb2614a97","after":"9ae5f9cebda20a415dc266cc5288c7c47f4c9f51","ref":"refs/heads/master","pushedAt":"2024-09-12T01:58:31.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"tchajed","name":"Tej Chajed","path":"/tchajed","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1255037?s=80&v=4"},"commit":{"message":"Bump std++ and Iris\n\nNeed some fixes for std++ moving string functions into a module","shortMessageHtmlLink":"Bump std++ and Iris"}},{"before":null,"after":"753ba18dc59b3f45edf3821e23388fd7df64e508","ref":"refs/heads/dependabot/submodules/external/iris-6f24ed4","pushedAt":"2024-09-11T08:16:25.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"dependabot[bot]","name":null,"path":"/apps/dependabot","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/29110?s=80&v=4"},"commit":{"message":"Bump external/iris from `f6ed092` to `6f24ed4`\n\nBumps external/iris from `f6ed092` to `6f24ed4`.\n\n---\nupdated-dependencies:\n- dependency-name: external/iris\n dependency-type: direct:production\n...\n\nSigned-off-by: dependabot[bot] ","shortMessageHtmlLink":"Bump external/iris from f6ed092 to 6f24ed4"}},{"before":null,"after":"ff50067d468b4d3703da4aa4dcb39e628665bde7","ref":"refs/heads/dependabot/submodules/external/stdpp-a1a12e0","pushedAt":"2024-09-11T08:16:23.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"dependabot[bot]","name":null,"path":"/apps/dependabot","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/29110?s=80&v=4"},"commit":{"message":"Bump external/stdpp from `d37b5e7` to `a1a12e0`\n\nBumps external/stdpp from `d37b5e7` to `a1a12e0`.\n\n---\nupdated-dependencies:\n- dependency-name: external/stdpp\n dependency-type: direct:production\n...\n\nSigned-off-by: dependabot[bot] ","shortMessageHtmlLink":"Bump external/stdpp from d37b5e7 to a1a12e0"}},{"before":"32f8c1ee3de8a1b7e5bac68a0bb1658633bb79ac","after":"ab6c5093026bc18cfc4689be4cda9e5fb2614a97","ref":"refs/heads/coq/tested","pushedAt":"2024-09-11T07:04:20.000Z","pushType":"push","commitsCount":5,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Suppress warnings about Stdlib renaming\n\nThe new names will be available in Coq 8.21, in the meantime the warning\nshould be disabled.","shortMessageHtmlLink":"Suppress warnings about Stdlib renaming"}},{"before":"ba9c27a9b22237d7ae40899188b0a6d373bec7d5","after":"ab6c5093026bc18cfc4689be4cda9e5fb2614a97","ref":"refs/heads/master","pushedAt":"2024-09-10T17:34:43.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"tchajed","name":"Tej Chajed","path":"/tchajed","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1255037?s=80&v=4"},"commit":{"message":"Suppress warnings about Stdlib renaming\n\nThe new names will be available in Coq 8.21, in the meantime the warning\nshould be disabled.","shortMessageHtmlLink":"Suppress warnings about Stdlib renaming"}},{"before":"4535a5d192b329af94b152b010e0e8672d006eb3","after":"ba9c27a9b22237d7ae40899188b0a6d373bec7d5","ref":"refs/heads/master","pushedAt":"2024-09-10T17:24:07.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"zeldovich","name":"Nickolai Zeldovich","path":"/zeldovich","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/828308?s=80&v=4"},"commit":{"message":"partial fixes tutorial/kvservice/full_proof.v\n\nSeems to be in a more substantially broken state, though.","shortMessageHtmlLink":"partial fixes tutorial/kvservice/full_proof.v"}},{"before":"32f8c1ee3de8a1b7e5bac68a0bb1658633bb79ac","after":"4535a5d192b329af94b152b010e0e8672d006eb3","ref":"refs/heads/master","pushedAt":"2024-09-10T16:54:41.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"tchajed","name":"Tej Chajed","path":"/tchajed","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1255037?s=80&v=4"},"commit":{"message":"Merge pull request #114 from proux01/coq_19519\n\nAdapt to https://github.com/coq/coq/pull/19519","shortMessageHtmlLink":"Merge pull request #114 from proux01/coq_19519"}},{"before":"a990c2255c86cc215a1afb587afd2709fcdd6d8f","after":"32f8c1ee3de8a1b7e5bac68a0bb1658633bb79ac","ref":"refs/heads/coq/tested","pushedAt":"2024-09-10T07:05:32.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Merge pull request #113 from mit-pdos/dependabot/submodules/external/stdpp-d37b5e7\n\nBump external/stdpp from `9d0f527` to `d37b5e7`","shortMessageHtmlLink":"Merge pull request #113 from mit-pdos/dependabot/submodules/external/…"}},{"before":"f30e8569da4187ebb0295feb116dfef70d0d7ead","after":null,"ref":"refs/heads/dependabot/submodules/external/stdpp-d37b5e7","pushedAt":"2024-09-09T10:04:56.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"dependabot[bot]","name":null,"path":"/apps/dependabot","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/29110?s=80&v=4"}},{"before":"a990c2255c86cc215a1afb587afd2709fcdd6d8f","after":"32f8c1ee3de8a1b7e5bac68a0bb1658633bb79ac","ref":"refs/heads/master","pushedAt":"2024-09-09T10:04:49.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Merge pull request #113 from mit-pdos/dependabot/submodules/external/stdpp-d37b5e7\n\nBump external/stdpp from `9d0f527` to `d37b5e7`","shortMessageHtmlLink":"Merge pull request #113 from mit-pdos/dependabot/submodules/external/…"}},{"before":null,"after":"f30e8569da4187ebb0295feb116dfef70d0d7ead","ref":"refs/heads/dependabot/submodules/external/stdpp-d37b5e7","pushedAt":"2024-09-09T09:06:56.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"dependabot[bot]","name":null,"path":"/apps/dependabot","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/29110?s=80&v=4"},"commit":{"message":"Bump external/stdpp from `9d0f527` to `d37b5e7`\n\nBumps external/stdpp from `9d0f527` to `d37b5e7`.\n\n---\nupdated-dependencies:\n- dependency-name: external/stdpp\n dependency-type: direct:production\n...\n\nSigned-off-by: dependabot[bot] ","shortMessageHtmlLink":"Bump external/stdpp from 9d0f527 to d37b5e7"}},{"before":"2cac086f346fb1e94e0c24bac8efb7a71f49254f","after":"a990c2255c86cc215a1afb587afd2709fcdd6d8f","ref":"refs/heads/coq/tested","pushedAt":"2024-09-08T07:04:07.000Z","pushType":"push","commitsCount":7,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Merge pull request #112 from mit-pdos/tchajed/slice-specs\n\nAdd various specs for slice skip/take","shortMessageHtmlLink":"Merge pull request #112 from mit-pdos/tchajed/slice-specs"}},{"before":"308a0b5c8e0db92b6fbf60001cc5474dc394c4f5","after":null,"ref":"refs/heads/tchajed/slice-specs","pushedAt":"2024-09-07T20:46:53.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"tchajed","name":"Tej Chajed","path":"/tchajed","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1255037?s=80&v=4"}},{"before":"531014b24a31bf3cdce455b096762728f196d6b7","after":"a990c2255c86cc215a1afb587afd2709fcdd6d8f","ref":"refs/heads/master","pushedAt":"2024-09-07T20:45:09.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"tchajed","name":"Tej Chajed","path":"/tchajed","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1255037?s=80&v=4"},"commit":{"message":"Merge pull request #112 from mit-pdos/tchajed/slice-specs\n\nAdd various specs for slice skip/take","shortMessageHtmlLink":"Merge pull request #112 from mit-pdos/tchajed/slice-specs"}},{"before":"87300f6095e4281c872fcc05c5e364a3b604653f","after":"308a0b5c8e0db92b6fbf60001cc5474dc394c4f5","ref":"refs/heads/tchajed/slice-specs","pushedAt":"2024-09-07T19:46:23.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"tchajed","name":"Tej Chajed","path":"/tchajed","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1255037?s=80&v=4"},"commit":{"message":"Add various specs for slice skip/take\n\nWe had several low-level specs, especially in the untyped library, but\nthe typed library was missing many things that seem obvious in\nretrospect.\n\nThere are six variants based on how ownership is divided, and it makes\nsense to provide all of these specs since they are not obvious\nconsequences of more general specs:\n\n1. SliceTake with `own_slice_small`. Straightforward.\n2. SliceSkip with `own_slice_small`. Straightforward.\n3. SliceTake with `own_slice`. Consumes the remainder of the slice to\n become the capacity of the prefix. This is the most distant from the\n code; it is not obvious that the original slice should no longer be\n used, even for reads.\n4. SliceSkip with `own_slice`. The capacity is retained as-is.\n5. std.SliceSplit with `own_slice_small`. This is a function in the\n Goose standard library that makes it easy to specify that doing\n `s[:n]` and `s[n:]` at the same time splits ownership, in a\n straightforward way. It is possible but more awkward to do this by\n directly writing `s[:n]` and `s[n:]` in the code.\n6. std.SliceSplit with `own_slice`. Similar to the `own_slice_small`\n spec, because the capacity of the original slice is identical to the\n capacity of the skipped part. Splitting in this case allows using the\n original capacity as the capacity of the `s[n:]` end, while not\n allowing appending to the `s[:n]` end since this capacity aliases the\n `s[n:]`.","shortMessageHtmlLink":"Add various specs for slice skip/take"}},{"before":null,"after":"87300f6095e4281c872fcc05c5e364a3b604653f","ref":"refs/heads/tchajed/slice-specs","pushedAt":"2024-09-07T19:45:45.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"tchajed","name":"Tej Chajed","path":"/tchajed","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1255037?s=80&v=4"},"commit":{"message":"Add various specs for slice skip/take\n\nWe had several low-level specs, especially in the untyped library, but\nthe typed library was missing many things that seem obvious in\nretrospect.\n\nThere are six variants based on how ownership is divided, and it makes\nsense to provide all of these specs since they are not obvious\nconsequences of more general specs:\n\n- 1, 2. SliceTake and SliceSkip with `own_slice_small`. Straightforward.\n- 3. SliceTake with `own_slice`. Consumes the remainder of the slice to\n become the capacity of the prefix. This is the most distant from the\n code; it is not obvious that the original slice should no longer be\n used, even for reads.\n- 4. SliceSkip with `own_slice`. The capacity is retained as-is.\n- 5. std.SliceSplit with `own_slice_small`. This is a function in the\n Goose standard library that makes it easy to specify that doing\n `s[:n]` and `s[n:]` at the same time splits ownership, in a\n straightforward way. It is possible but more awkward to do this by\n directly writing `s[:n]` and `s[n:]` in the code.\n- 6. std.SliceSplit with `own_slice`. Similar to the `own_slice_small`\n spec, because the capacity of the original slice is identical to the\n capacity of the skipped part. Splitting in this case allows using the\n original capacity as the capacity of the `s[n:]` end, while not\n allowing appending to the `s[:n]` end since this capacity aliases the\n `s[n:]`.","shortMessageHtmlLink":"Add various specs for slice skip/take"}},{"before":"e9ed8ceaf54c9a476b6d98e03f673a8dc11fae72","after":null,"ref":"refs/heads/tchajed/rename-mutex-methods","pushedAt":"2024-09-07T18:25:35.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"tchajed","name":"Tej Chajed","path":"/tchajed","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1255037?s=80&v=4"}},{"before":"90480d0a8c76deb34a2d4161c64c42b5090d9d5e","after":"531014b24a31bf3cdce455b096762728f196d6b7","ref":"refs/heads/master","pushedAt":"2024-09-07T16:08:22.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"tchajed","name":"Tej Chajed","path":"/tchajed","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1255037?s=80&v=4"},"commit":{"message":"Re-goose with mutex/cond renames","shortMessageHtmlLink":"Re-goose with mutex/cond renames"}},{"before":"73bc2ed38c89dbbe7663109c543f756844bfab57","after":"90480d0a8c76deb34a2d4161c64c42b5090d9d5e","ref":"refs/heads/master","pushedAt":"2024-09-07T15:58:05.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"tchajed","name":"Tej Chajed","path":"/tchajed","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1255037?s=80&v=4"},"commit":{"message":"Merge pull request #111 from mit-pdos/tchajed/rename-mutex-methods\n\nRename Mutex and Cond methods for consistency","shortMessageHtmlLink":"Merge pull request #111 from mit-pdos/tchajed/rename-mutex-methods"}},{"before":"2cac086f346fb1e94e0c24bac8efb7a71f49254f","after":"73bc2ed38c89dbbe7663109c543f756844bfab57","ref":"refs/heads/master","pushedAt":"2024-09-07T15:00:16.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"tchajed","name":"Tej Chajed","path":"/tchajed","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1255037?s=80&v=4"},"commit":{"message":"Fix a warning from Coq 8.20","shortMessageHtmlLink":"Fix a warning from Coq 8.20"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0yMFQwNzowNDozMC4wMDAwMDBazwAAAAS7pbzC","startCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0yMFQwNzowNDozMC4wMDAwMDBazwAAAAS7pbzC","endCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0wN1QxNTowMDoxNi4wMDAwMDBazwAAAASvsCXa"}},"title":"Activity · mit-pdos/perennial"}