{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":206173953,"defaultBranch":"master","name":"libraries","ownerLogin":"RustanLeino","currentUserCanPush":false,"isFork":true,"isEmpty":false,"createdAt":"2019-09-03T21:17:02.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/11763367?v=4","public":true,"private":false,"isOrgOwned":false},"refInfo":{"name":"","listCacheKey":"v0:1708452176.0","currentOid":""},"activityList":{"items":[{"before":"492c08ad53c92fe08dab638c4e7bc873e912d199","after":null,"ref":"refs/heads/add-missing-type-characteristics","pushedAt":"2024-02-20T18:02:56.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"RustanLeino","name":"Rustan Leino","path":"/RustanLeino","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/11763367?s=80&v=4"}},{"before":"67e21af2810b6290d77b7b1e1acab92fe52c7a87","after":"492c08ad53c92fe08dab638c4e7bc873e912d199","ref":"refs/heads/add-missing-type-characteristics","pushedAt":"2024-01-20T16:37:06.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"RustanLeino","name":"Rustan Leino","path":"/RustanLeino","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/11763367?s=80&v=4"},"commit":{"message":"Merge branch 'master' into add-missing-type-characteristics","shortMessageHtmlLink":"Merge branch 'master' into add-missing-type-characteristics"}},{"before":"a2aac6d3c82529e23a9160af2516a6fac5f355b5","after":"67e21af2810b6290d77b7b1e1acab92fe52c7a87","ref":"refs/heads/add-missing-type-characteristics","pushedAt":"2024-01-20T16:27:33.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"RustanLeino","name":"Rustan Leino","path":"/RustanLeino","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/11763367?s=80&v=4"},"commit":{"message":"Remove {:opaque} attribute from lemmas","shortMessageHtmlLink":"Remove {:opaque} attribute from lemmas"}},{"before":"ce5c491d119a9b447d8681154f521aec9faad6bb","after":"a2aac6d3c82529e23a9160af2516a6fac5f355b5","ref":"refs/heads/add-missing-type-characteristics","pushedAt":"2024-01-03T21:10:56.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"RustanLeino","name":"Rustan Leino","path":"/RustanLeino","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/11763367?s=80&v=4"},"commit":{"message":"Revert \"Change deprecated “forall ensures” to “assert by”\"\n\nThis reverts commit ce5c491d119a9b447d8681154f521aec9faad6bb.","shortMessageHtmlLink":"Revert \"Change deprecated “forall ensures” to “assert by”\""}},{"before":null,"after":"ce5c491d119a9b447d8681154f521aec9faad6bb","ref":"refs/heads/add-missing-type-characteristics","pushedAt":"2024-01-03T20:00:57.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"RustanLeino","name":"Rustan Leino","path":"/RustanLeino","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/11763367?s=80&v=4"},"commit":{"message":"Change deprecated “forall ensures” to “assert by”","shortMessageHtmlLink":"Change deprecated “forall ensures” to “assert by”"}},{"before":"7c386fa0b4a267715f9bd49948d1af68e1631e6b","after":"ae8708c091d32383235d5d8c15c08cff05613bbc","ref":"refs/heads/master","pushedAt":"2024-01-03T18:05:53.000Z","pushType":"push","commitsCount":11,"pusher":{"login":"RustanLeino","name":"Rustan Leino","path":"/RustanLeino","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/11763367?s=80&v=4"},"commit":{"message":"Chore: Proofs not depending on leaks of opaque + brittleness reduction (#149)\n\n* Chore: Proofs not depending on leaks of opaque + brittleness reduction\r\nI added reveal statements where they were previously \"leaked\" because of fuel encoding that are soon going away.\r\nI also reduced the RU for ToLarge from 6.8M to 1.3M.\r\n\r\n* Forgot to save a file\r\n\r\n* Fixed brittleness issue for current Dafny\r\n\r\n* Fixed two brittle proofs\r\n\r\n* Fixed formatting\r\n\r\n* Comment about the proof\r\n\r\n* Update src/Collections/Sequences/LittleEndianNatConversions.dfy","shortMessageHtmlLink":"Chore: Proofs not depending on leaks of opaque + brittleness reduction ("}},{"before":"8cfeb0d52772429ad8d55b25aef6dfd88bc5c843","after":"7c386fa0b4a267715f9bd49948d1af68e1631e6b","ref":"refs/heads/master","pushedAt":"2023-05-05T17:44:02.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"RustanLeino","name":"Rustan Leino","path":"/RustanLeino","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/11763367?s=80&v=4"},"commit":{"message":"Miscellaneous edits to the new library, to support testing (#117)\n\n* Working on reusable tests\r\n\r\n* Debugging\r\n\r\n* Debugging #2\r\n\r\n* Debugging #3\r\n\r\n* Debugging #4\r\n\r\n* Debugging #4\r\n\r\n* Debugging #5\r\n\r\n* Debugging #6\r\n\r\n* Debugging #7\r\n\r\n* Debugging #8\r\n\r\n* Debugging #9\r\n\r\n* Debugging #10\r\n\r\n* Debugging #11\r\n\r\n* Debugging #12\r\n\r\n* Debugging #13\r\n\r\n* Debugging #14\r\n\r\n* Debugging #14\r\n\r\n* Debugging\r\n\r\n* Debugging\r\n\r\n* Debugging\r\n\r\n* Debugging\r\n\r\n* OK, except disabling 3.13.1 and nightly-latest until setup-dafny-action is fixed\r\n\r\n* OK, except disabling 3.13.1 and nightly-latest until setup-dafny-action is fixed\r\n\r\n* Fixing the concurrency check\r\n\r\n* Old edits\r\n\r\n* Edits to examples\r\n\r\n* Touchups to examples and library\r\n\r\n* Math relations and examples\r\n\r\n* Some docstring documentation\r\n\r\n* Some docstring documentation\r\n\r\n* typo\r\n\r\n* Formatting\r\n\r\n* Removing semicolon\r\n\r\n* Adjusting for Dafny 3\r\n\r\n* Attempt to fix proof in ld dafny versions\r\n\r\n* Fixing up docstrings\r\n\r\n* Fixed examples\r\n\r\n* Fixed formatting\r\n\r\n* Fixed formatting\r\n\r\n* Formatting\r\n\r\n* Formatting\r\n\r\n---------\r\n\r\nCo-authored-by: davidcok ","shortMessageHtmlLink":"Miscellaneous edits to the new library, to support testing (dafny-lan…"}},{"before":"20d90ec43db21d224bb5db0020cc68a2d441143c","after":"8cfeb0d52772429ad8d55b25aef6dfd88bc5c843","ref":"refs/heads/master","pushedAt":"2023-03-31T17:15:46.000Z","pushType":"push","commitsCount":11,"pusher":{"login":"RustanLeino","name":"Rustan Leino","path":"/RustanLeino","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/11763367?s=80&v=4"},"commit":{"message":"Documentation and examples for library modules (#116)\n\n* Edits to examples\r\n\r\n* Touchups to examples and library\r\n\r\n* Math relations and examples\r\n\r\n* Some docstring documentation\r\n\r\n* Some docstring documentation\r\n\r\n* typo\r\n\r\n* Formatting\r\n\r\n* Removing semicolon\r\n\r\n* Adjusting for Dafny 3\r\n\r\n* Attempt to fix proof in ld dafny versions\r\n\r\n---------\r\n\r\nCo-authored-by: davidcok ","shortMessageHtmlLink":"Documentation and examples for library modules (dafny-lang#116)"}}],"hasNextPage":false,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"Y3Vyc29yOnYyOpK7MjAyNC0wMi0yMFQxODowMjo1Ni4wMDAwMDBazwAAAAP__0Ky","startCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wMi0yMFQxODowMjo1Ni4wMDAwMDBazwAAAAP__0Ky","endCursor":"Y3Vyc29yOnYyOpK7MjAyMy0wMy0zMVQxNzoxNTo0Ni4wMDAwMDBazwAAAAMPrJHs"}},"title":"Activity · RustanLeino/libraries"}