{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":831131113,"defaultBranch":"main","name":"rust-lean-models","ownerLogin":"model-checking","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2024-07-19T18:25:05.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/78765001?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1721413507.0","currentOid":""},"activityList":{"items":[{"before":"16fcb23e0d2580b1153f5260c8bef7706127b91f","after":"ce44f0266495ef4758b6528cb5d979b9b20ce23f","ref":"refs/heads/main","pushedAt":"2024-09-04T01:57:08.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"BrunoDutertre","name":"Bruno Dutertre","path":"/BrunoDutertre","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/8507586?s=80&v=4"},"commit":{"message":"Upgrade Lean to v4.11.0 (#11)\n\nWith v4.11.0, `batteries` is no longer needed.\r\n\r\nBy submitting this pull request, I confirm that my contribution is made\r\nunder the terms of the Apache 2.0 and MIT licenses.","shortMessageHtmlLink":"Upgrade Lean to v4.11.0 (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2503600831\" data-permission-text=\"Title is private\" data-url=\"https://github.com/model-checking/rust-lean-models/issues/11\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/model-checking/rust-lean-models/pull/11/hovercard\" href=\"https://github.com/model-checking/rust-lean-models/pull/11\">#11</a>)"}},{"before":"bc90fc7ecdb5ca5381f3271b265f80699ec94e24","after":"16fcb23e0d2580b1153f5260c8bef7706127b91f","ref":"refs/heads/main","pushedAt":"2024-08-27T23:29:46.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"zhassan-aws","name":"Zyad Hassan","path":"/zhassan-aws","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88045115?s=80&v=4"},"commit":{"message":"Add Lean action in CI (#10)\n\nAdd Lean action in CI to make sure the package doesn't break.\r\n\r\nBy submitting this pull request, I confirm that my contribution is made\r\nunder the terms of the Apache 2.0 and MIT licenses.","shortMessageHtmlLink":"Add Lean action in CI (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2490133587\" data-permission-text=\"Title is private\" data-url=\"https://github.com/model-checking/rust-lean-models/issues/10\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/model-checking/rust-lean-models/pull/10/hovercard\" href=\"https://github.com/model-checking/rust-lean-models/pull/10\">#10</a>)"}},{"before":"f869a4c6054234073ef56681c24aed95de128be0","after":"bc90fc7ecdb5ca5381f3271b265f80699ec94e24","ref":"refs/heads/main","pushedAt":"2024-08-13T23:32:27.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"BrunoDutertre","name":"Bruno Dutertre","path":"/BrunoDutertre","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/8507586?s=80&v=4"},"commit":{"message":"Remove mathlib dependency (#9)\n\nRemove mathlib from dependencies and fix all proofs.\r\n\r\nCall outs: I had to add `batteries` as a dependency, but all\r\ndefinitions/theorems needed from `batteries` (e.g. `List.IsPrefix`) have\r\nbeen upstreamed in\r\nhttps://github.com/leanprover/lean4/releases/tag/v4.11.0-rc1 (e.g.\r\nhttps://github.com/leanprover/lean4/pull/4836), so we should be able to\r\nget rid of the `batteries` dependency as well once v4.11.0 is released.\r\n\r\nBy submitting this pull request, I confirm that my contribution is made\r\nunder the terms of the Apache 2.0 and MIT licenses.","shortMessageHtmlLink":"Remove mathlib dependency (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2461805131\" data-permission-text=\"Title is private\" data-url=\"https://github.com/model-checking/rust-lean-models/issues/9\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/model-checking/rust-lean-models/pull/9/hovercard\" href=\"https://github.com/model-checking/rust-lean-models/pull/9\">#9</a>)"}},{"before":"d18550535a99fd0f20f5273f54608bfbecf1a7f4","after":"f869a4c6054234073ef56681c24aed95de128be0","ref":"refs/heads/main","pushedAt":"2024-08-02T21:00:07.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"zhassan-aws","name":"Zyad Hassan","path":"/zhassan-aws","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88045115?s=80&v=4"},"commit":{"message":"Edits to the README and other markdown files. (#7)\n\nThis fixes typos in the README and gives links to the RustString.md and\r\nIterators.md.\r\n\r\nBy submitting this pull request, I confirm that my contribution is made\r\nunder the terms of the Apache 2.0 and MIT licenses.","shortMessageHtmlLink":"Edits to the README and other markdown files. (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2443908587\" data-permission-text=\"Title is private\" data-url=\"https://github.com/model-checking/rust-lean-models/issues/7\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/model-checking/rust-lean-models/pull/7/hovercard\" href=\"https://github.com/model-checking/rust-lean-models/pull/7\">#7</a>)"}},{"before":"bfac0bfd0e4ba14199137f7d60bc0ed1094b5528","after":"d18550535a99fd0f20f5273f54608bfbecf1a7f4","ref":"refs/heads/main","pushedAt":"2024-08-01T23:28:02.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"BrunoDutertre","name":"Bruno Dutertre","path":"/BrunoDutertre","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/8507586?s=80&v=4"},"commit":{"message":"Upgrade Lean to v4.10.0 (#5)\n\nUpgrade Lean toolchain version to v4.10.0.\r\n\r\nThe change in `Basic.lean` is due to a warning I got from the linter:\r\n```bash\r\n$ lake build\r\n⚠ [4886/4888] Built RustLeanModels.Basic\r\nwarning: ././././RustLeanModels/Basic.lean:21:2: Please, use '·' (typed as `\\·`) instead of '.' as 'cdot'.\r\nnote: this linter can be disabled with `set_option linter.cdot false`\r\nwarning: ././././RustLeanModels/Basic.lean:24:2: Please, use '·' (typed as `\\·`) instead of '.' as 'cdot'.\r\nnote: this linter can be disabled with `set_option linter.cdot false`\r\nBuild completed successfully.\r\n```\r\n\r\nBy submitting this pull request, I confirm that my contribution is made\r\nunder the terms of the Apache 2.0 and MIT licenses.","shortMessageHtmlLink":"Upgrade Lean to v4.10.0 (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2443225477\" data-permission-text=\"Title is private\" data-url=\"https://github.com/model-checking/rust-lean-models/issues/5\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/model-checking/rust-lean-models/pull/5/hovercard\" href=\"https://github.com/model-checking/rust-lean-models/pull/5\">#5</a>)"}},{"before":"ec55589968733d583783cdd6fe03a5ae8cfd4f44","after":"bfac0bfd0e4ba14199137f7d60bc0ed1094b5528","ref":"refs/heads/main","pushedAt":"2024-08-01T23:27:43.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"BrunoDutertre","name":"Bruno Dutertre","path":"/BrunoDutertre","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/8507586?s=80&v=4"},"commit":{"message":"Update CODEOWNERS file (#6)\n\nAdd @BrunoDutertre to `CODEOWNERS` file so that he can approve PRs.\r\n\r\nBy submitting this pull request, I confirm that my contribution is made\r\nunder the terms of the Apache 2.0 and MIT licenses.","shortMessageHtmlLink":"Update CODEOWNERS file (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2443571705\" data-permission-text=\"Title is private\" data-url=\"https://github.com/model-checking/rust-lean-models/issues/6\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/model-checking/rust-lean-models/pull/6/hovercard\" href=\"https://github.com/model-checking/rust-lean-models/pull/6\">#6</a>)"}},{"before":"9ebeeda918cd02729b5d5e2bcdb275bfbb8c0524","after":"ec55589968733d583783cdd6fe03a5ae8cfd4f44","ref":"refs/heads/main","pushedAt":"2024-07-29T17:56:48.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"BrunoDutertre","name":"Bruno Dutertre","path":"/BrunoDutertre","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/8507586?s=80&v=4"},"commit":{"message":"Include a couple of definitions in the README.md (#4)\n\nInclude the definitions of `is_char_boundary` and `floor_char_boundary`\r\nin the README.md file since the equivalence theorems refers to them.\r\n\r\nAlso, update `is_char_boundary_def` to match the definition used in\r\n`RustString.lean`.\r\n\r\nBy submitting this pull request, I confirm that my contribution is made\r\nunder the terms of the Apache 2.0 and MIT licenses.","shortMessageHtmlLink":"Include a couple of definitions in the README.md (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2435892231\" data-permission-text=\"Title is private\" data-url=\"https://github.com/model-checking/rust-lean-models/issues/4\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/model-checking/rust-lean-models/pull/4/hovercard\" href=\"https://github.com/model-checking/rust-lean-models/pull/4\">#4</a>)"}},{"before":"e89e39a4d45cdceb87eca93e19017018fc2822e7","after":"9ebeeda918cd02729b5d5e2bcdb275bfbb8c0524","ref":"refs/heads/main","pushedAt":"2024-07-25T23:33:51.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"zhassan-aws","name":"Zyad Hassan","path":"/zhassan-aws","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88045115?s=80&v=4"},"commit":{"message":"Adding some lemmas for Str_toUTF8 in UTF8Str, cleaning up some proofs in RustString (#3)\n\n> Adding some lemmas for Str_toUTF8 in UTF8Str, cleaning up some proofs\r\nin RustString\r\n\r\nBy submitting this pull request, I confirm that my contribution is made\r\nunder the terms of the Apache 2.0 and MIT licenses.\r\n\r\nCo-authored-by: THANH NGUYEN <ntson@amazon.com>","shortMessageHtmlLink":"Adding some lemmas for Str_toUTF8 in UTF8Str, cleaning up some proofs…"}},{"before":"2a6f7873d3bf3f665f826a8bd5ac74cd0a87f267","after":"e89e39a4d45cdceb87eca93e19017018fc2822e7","ref":"refs/heads/main","pushedAt":"2024-07-25T17:41:47.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"zhassan-aws","name":"Zyad Hassan","path":"/zhassan-aws","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88045115?s=80&v=4"},"commit":{"message":"add README.md, RustString library, Iterator, general functions (#1)\n\nREADME.md: documentation (installation, description) of the library\r\nRustString.lean: the RustString library which includes all the\r\nequivalent Lean versions of Rust String functions in Rust standard\r\nlibrary, proof of correctness and supporting theorems/lemma\r\nBasic.lean: Generic lemmas for logic, Nat, List\r\nIterator: modeling Rust Iterator in Lean\r\n\r\n---------\r\n\r\nCo-authored-by: THANH NGUYEN <ntson@amazon.com>\r\nCo-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>","shortMessageHtmlLink":"add README.md, RustString library, Iterator, general functions (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2420412228\" data-permission-text=\"Title is private\" data-url=\"https://github.com/model-checking/rust-lean-models/issues/1\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/model-checking/rust-lean-models/pull/1/hovercard\" href=\"https://github.com/model-checking/rust-lean-models/pull/1\">#1</a>)"}},{"before":"391080df3f7ee59c0d7ec2816d2675d9307b789a","after":"2a6f7873d3bf3f665f826a8bd5ac74cd0a87f267","ref":"refs/heads/main","pushedAt":"2024-07-22T18:35:40.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"zhassan-aws","name":"Zyad Hassan","path":"/zhassan-aws","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88045115?s=80&v=4"},"commit":{"message":"Add MIT license, CODEOWNERS file, and PR template (#2)\n\nAdd MIT license, CODEOWNERS file, and PR template.\r\n\r\nBy submitting this pull request, I confirm that my contribution is made\r\nunder the terms of the Apache 2.0 and MIT licenses.","shortMessageHtmlLink":"Add MIT license, CODEOWNERS file, and PR template (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2420420220\" data-permission-text=\"Title is private\" data-url=\"https://github.com/model-checking/rust-lean-models/issues/2\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/model-checking/rust-lean-models/pull/2/hovercard\" href=\"https://github.com/model-checking/rust-lean-models/pull/2\">#2</a>)"}},{"before":"954e4cbb5ee05aaa65ef246c80c361e5e3c63b00","after":"391080df3f7ee59c0d7ec2816d2675d9307b789a","ref":"refs/heads/main","pushedAt":"2024-07-19T23:38:03.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"ntson-aws","name":null,"path":"/ntson-aws","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/176079618?s=80&v=4"},"commit":{"message":"add lake package","shortMessageHtmlLink":"add lake package"}},{"before":"39856985f6faff3a00053e94501ac0087ec58806","after":"954e4cbb5ee05aaa65ef246c80c361e5e3c63b00","ref":"refs/heads/main","pushedAt":"2024-07-19T23:35:45.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"ntson-aws","name":null,"path":"/ntson-aws","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/176079618?s=80&v=4"},"commit":{"message":"add lake packages","shortMessageHtmlLink":"add lake packages"}},{"before":"5499eb73f2d50b5391d1a709baa7913fb383dce6","after":"39856985f6faff3a00053e94501ac0087ec58806","ref":"refs/heads/main","pushedAt":"2024-07-19T19:34:48.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"zhassan-aws","name":"Zyad Hassan","path":"/zhassan-aws","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88045115?s=80&v=4"},"commit":{"message":"Update README","shortMessageHtmlLink":"Update README"}},{"before":null,"after":"5499eb73f2d50b5391d1a709baa7913fb383dce6","ref":"refs/heads/main","pushedAt":"2024-07-19T18:25:07.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"amazon-auto","name":"Amazon GitHub Automation","path":"/amazon-auto","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/54958958?s=80&v=4"},"commit":{"message":"Initial commit","shortMessageHtmlLink":"Initial commit"}}],"hasNextPage":false,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0wNFQwMTo1NzowOC4wMDAwMDBazwAAAASsLxNq","startCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0wNFQwMTo1NzowOC4wMDAwMDBazwAAAASsLxNq","endCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wNy0xOVQxODoyNTowNy4wMDAwMDBazwAAAASELutz"}},"title":"Activity · model-checking/rust-lean-models"}