{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":342393010,"defaultBranch":"master","name":"cerberus","ownerLogin":"rems-project","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2021-02-25T22:11:56.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/35805581?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1722376168.0","currentOid":""},"activityList":{"items":[{"before":"20d9d5ce2e982c4744ef6911a25a3be9307518f3","after":"6188c37ecc0a55903a16b9272b9f2b85f6546b3b","ref":"refs/heads/master","pushedAt":"2024-07-31T01:06:38.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"vzaliva","name":"Vadim Zaliva","path":"/vzaliva","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/86581?s=80&v=4"},"commit":{"message":"`sizeof_pos` wip","shortMessageHtmlLink":"sizeof_pos wip"}},{"before":"4ee33242ea00a0e5f6033abd254b2d826392c8e8","after":"1dbbf4bb41689c880319c754180432a10c2fd65a","ref":"refs/heads/issue_435","pushedAt":"2024-07-30T23:10:37.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yav","name":"Iavor S. Diatchki","path":"/yav","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12394?s=80&v=4"},"commit":{"message":"Fixes #395.\n\nThis commit has the same changes as in PR #397, but adapted\nto the new formatting and library location.","shortMessageHtmlLink":"Fixes #395."}},{"before":"556171a17fca94b6aaf76bccfa7db63833428113","after":"20d9d5ce2e982c4744ef6911a25a3be9307518f3","ref":"refs/heads/master","pushedAt":"2024-07-30T22:17:14.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"dc-mak","name":"Dhruv Makwana","path":"/dc-mak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7052028?s=80&v=4"},"commit":{"message":"CN: Fix lemmata tests (#454)\n\nThese tests are not enabled in the CI yet (they should be, but I couldn't figure it out and I'm away for the next 1.5 weeks).\r\n\r\n`as_auto_mutual_dt` was deleted because there's [a check in CN](https://github.com/rems-project/cerberus/blob/556171a17fca94b6aaf76bccfa7db63833428113/backend/cn/lib/wellTyped.ml#L2443-L2444) which prevents the indirect recursion used in [as_auto_mutual_dt/tree16.error.c](https://github.com/rems-project/cerberus/blob/master/tests/cn/tree16/as_auto_mutual_dt/tree16.error.c) from passing.\r\n\r\nTested with the following:\r\n```sh\r\n➜ coqc --version\r\nThe Coq Proof Assistant, version 8.19.2\r\ncompiled with OCaml 4.14.1\r\n```","shortMessageHtmlLink":"CN: Fix lemmata tests (#454)"}},{"before":"5e09152bf2ac99bfe5ee1fe3e334b2324f879a28","after":"4ee33242ea00a0e5f6033abd254b2d826392c8e8","ref":"refs/heads/issue_435","pushedAt":"2024-07-30T22:02:01.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yav","name":"Iavor S. Diatchki","path":"/yav","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12394?s=80&v=4"},"commit":{"message":"Format things appropriately.","shortMessageHtmlLink":"Format things appropriately."}},{"before":"752b1ef93dcff921a6a908b84decfc8a865ae0a7","after":"556171a17fca94b6aaf76bccfa7db63833428113","ref":"refs/heads/master","pushedAt":"2024-07-30T22:01:31.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"dc-mak","name":"Dhruv Makwana","path":"/dc-mak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7052028?s=80&v=4"},"commit":{"message":"CN-exec: Remove malloc/free runtime tests\n\nThese have been moved to the cn-tutorial repo as part of the CN runtime\ntesting CI https://github.com/rems-project/cn-tutorial/commit/b762b022f6d8bc8fb440464c01c73bacc37ebc78","shortMessageHtmlLink":"CN-exec: Remove malloc/free runtime tests"}},{"before":null,"after":"5e09152bf2ac99bfe5ee1fe3e334b2324f879a28","ref":"refs/heads/issue_435","pushedAt":"2024-07-30T21:49:28.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"yav","name":"Iavor S. Diatchki","path":"/yav","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12394?s=80&v=4"},"commit":{"message":"Fixes #435\n\nMaps may appear in the fields of a struct, if the field is of an array type.","shortMessageHtmlLink":"Fixes #435"}},{"before":"29e8f7c10cef676a4b2f927b25d8a0758c1e62f8","after":"752b1ef93dcff921a6a908b84decfc8a865ae0a7","ref":"refs/heads/master","pushedAt":"2024-07-30T21:00:48.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"dc-mak","name":"Dhruv Makwana","path":"/dc-mak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7052028?s=80&v=4"},"commit":{"message":"CN: Make run-cn.sh printing more consistent\n\nThe priniting is now in line with other CI test scripts, and run through\nshellcheck to check for mistakes. An oddity is that the failing tests\ncould reflect either exit code 1 or 2, and passing arrays in bash is a\nbit tricky, but this all seems to work.","shortMessageHtmlLink":"CN: Make run-cn.sh printing more consistent"}},{"before":"fa710e609b35e3e87f6b4a4596af744c34999c5d","after":"29e8f7c10cef676a4b2f927b25d8a0758c1e62f8","ref":"refs/heads/master","pushedAt":"2024-07-30T12:45:42.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"dc-mak","name":"Dhruv Makwana","path":"/dc-mak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7052028?s=80&v=4"},"commit":{"message":"CN: Fix and re-enable formatting\n\nhttps://github.com/rems-project/cerberus/commit/c77d64541983966a50cc00e349b6627756d18024\naccidentally deleted the formatting CI check and https://github.com/rems-project/cerberus/commit/d7b47b7417ab78af0d9e0dbbc590453b83bc5870\ncommitted badly formatted code.\n\nThis commit fixes both of the above.","shortMessageHtmlLink":"CN: Fix and re-enable formatting"}},{"before":"6ec601fd2f70e19762de3d0c28274fce9d76f25c","after":"fa710e609b35e3e87f6b4a4596af744c34999c5d","ref":"refs/heads/master","pushedAt":"2024-07-30T01:50:28.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"vzaliva","name":"Vadim Zaliva","path":"/vzaliva","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/86581?s=80&v=4"},"commit":{"message":"~offsetof_max_offset_pos~ wip","shortMessageHtmlLink":"~offsetof_max_offset_pos~ wip"}},{"before":"d7b47b7417ab78af0d9e0dbbc590453b83bc5870","after":"6ec601fd2f70e19762de3d0c28274fce9d76f25c","ref":"refs/heads/master","pushedAt":"2024-07-29T15:18:03.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"cp526","name":"Christopher Pulte","path":"/cp526","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6631650?s=80&v=4"},"commit":{"message":"Make Core elaboration of unary minus add C-type annotation to 0. (#446)\n\nFixes https://github.com/rems-project/cerberus/issues/236 and https://github.com/rems-project/cerberus/issues/257","shortMessageHtmlLink":"Make Core elaboration of unary minus add C-type annotation to 0. (#446)"}},{"before":"b3d7e04634ebb267152a7d8b34b30e25869e68cf","after":"d7b47b7417ab78af0d9e0dbbc590453b83bc5870","ref":"refs/heads/master","pushedAt":"2024-07-29T15:01:38.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"dc-mak","name":"Dhruv Makwana","path":"/dc-mak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7052028?s=80&v=4"},"commit":{"message":"[CN] Add Modulo Operator %\n\nAdd OpRem_t to check.ml and CN_mod as a cn_binop in cn.lem\n\nAdd CN_mod definiton to mk_translate_binop in compile.ml\n\nAdd CN_mod to pp_cn_binop in cn_ocaml.ml\n\nAdd PERCENT symbol as a mul_expr in c_parser.mly\n\nUpdate parser message to allow PERCENT as a mul_expr with CN\n\nAdd modulo test in tests/cn/","shortMessageHtmlLink":"[CN] Add Modulo Operator %"}},{"before":"931e0c1bc39b794825a5a896e19891cd0b4120c6","after":"b3d7e04634ebb267152a7d8b34b30e25869e68cf","ref":"refs/heads/master","pushedAt":"2024-07-27T00:41:59.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"vzaliva","name":"Vadim Zaliva","path":"/vzaliva","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/86581?s=80&v=4"},"commit":{"message":"work on `sizeof_pos` proof. automations. helper lemmas.","shortMessageHtmlLink":"work on sizeof_pos proof. automations. helper lemmas."}},{"before":"d5d8db5a52e3abe2990375f9f0f58cbed01c321b","after":"931e0c1bc39b794825a5a896e19891cd0b4120c6","ref":"refs/heads/master","pushedAt":"2024-07-26T23:36:07.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"ZippeyKeys12","name":"Zain K Aamer","path":"/ZippeyKeys12","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9499189?s=80&v=4"},"commit":{"message":" [CN-Test-Gen/CN-Exec] Make CI tests use executable spec","shortMessageHtmlLink":" [CN-Test-Gen/CN-Exec] Make CI tests use executable spec"}},{"before":"31ad5db6b658536cafd2ecb603d7f14d2706100c","after":"d5d8db5a52e3abe2990375f9f0f58cbed01c321b","ref":"refs/heads/master","pushedAt":"2024-07-26T17:54:13.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"vzaliva","name":"Vadim Zaliva","path":"/vzaliva","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/86581?s=80&v=4"},"commit":{"message":"`capmeta_ghost_tags_spec_outside_range_aligned` proven","shortMessageHtmlLink":"capmeta_ghost_tags_spec_outside_range_aligned proven"}},{"before":"74f5b374ca06c9272431218ebddf6f3d3b0c26cf","after":"31ad5db6b658536cafd2ecb603d7f14d2706100c","ref":"refs/heads/master","pushedAt":"2024-07-26T10:31:58.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"cp526","name":"Christopher Pulte","path":"/cp526","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6631650?s=80&v=4"},"commit":{"message":"[CN] improve CN performance (#436)\n\nCN derives constraints from resource ownership; this fixes (some of\r\nthe) duplication in what constraints are derived","shortMessageHtmlLink":"[CN] improve CN performance (#436)"}},{"before":"6edf463aa8de250d9a5b8e5da1ad4112f76f1239","after":"74f5b374ca06c9272431218ebddf6f3d3b0c26cf","ref":"refs/heads/master","pushedAt":"2024-07-25T20:16:44.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"cp526","name":"Christopher Pulte","path":"/cp526","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6631650?s=80&v=4"},"commit":{"message":"Minor tweaks to fix concurent job execution (#434)","shortMessageHtmlLink":"Minor tweaks to fix concurent job execution (#434)"}},{"before":"251beeed9d5ec34acd4d0e60b731c10611afbebe","after":"6edf463aa8de250d9a5b8e5da1ad4112f76f1239","ref":"refs/heads/master","pushedAt":"2024-07-25T19:58:47.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"cp526","name":"Christopher Pulte","path":"/cp526","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6631650?s=80&v=4"},"commit":{"message":"Build multiplatform docker images (#430)\n\n* Build multiplatform docker images\r\n\r\n* try to start from scratch\r\n\r\n* Try QEMU action\r\n\r\n* Restore missing jobs and clean up the whitespace\r\n\r\n* Split the CI jobs, and run the docker build only on merge to master","shortMessageHtmlLink":"Build multiplatform docker images (#430)"}},{"before":"f5efec8d45ae44f7bae12dd847b8e434e5d5cc16","after":"251beeed9d5ec34acd4d0e60b731c10611afbebe","ref":"refs/heads/master","pushedAt":"2024-07-25T19:09:56.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rbanerjee20","name":"Rini Banerjee","path":"/rbanerjee20","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/26858592?s=80&v=4"},"commit":{"message":"CN-exec: add printing for generated files tmp directory at end of output","shortMessageHtmlLink":"CN-exec: add printing for generated files tmp directory at end of output"}},{"before":"281cfc42fc5de0672b6ac6867cbc9b8346a2eb41","after":"f5efec8d45ae44f7bae12dd847b8e434e5d5cc16","ref":"refs/heads/master","pushedAt":"2024-07-25T18:49:05.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"cp526","name":"Christopher Pulte","path":"/cp526","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6631650?s=80&v=4"},"commit":{"message":"CN: make `make install_cn` work without `make install`\n(and update README)","shortMessageHtmlLink":"CN: make make install_cn work without make install"}},{"before":"96c4c83838d38d5908d2ee039b6ad2e6285eb94d","after":"281cfc42fc5de0672b6ac6867cbc9b8346a2eb41","ref":"refs/heads/master","pushedAt":"2024-07-25T18:22:49.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"cp526","name":"Christopher Pulte","path":"/cp526","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6631650?s=80&v=4"},"commit":{"message":"CN: split CN into a library and an executable (#429)\n\n* CN: split CN into library and executable components\r\n\r\n* CN: remove CLI dependency from library\r\n\r\n* CN: update filepath references in docs","shortMessageHtmlLink":"CN: split CN into a library and an executable (#429)"}},{"before":"e7a4d2b407f69dd9a757dfba5ede1a66a50e188a","after":"96c4c83838d38d5908d2ee039b6ad2e6285eb94d","ref":"refs/heads/master","pushedAt":"2024-07-25T16:39:37.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"dc-mak","name":"Dhruv Makwana","path":"/dc-mak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7052028?s=80&v=4"},"commit":{"message":"CN: Tidy up in core_to_mucore.ml and signature","shortMessageHtmlLink":"CN: Tidy up in core_to_mucore.ml and signature"}},{"before":"979016d39c1caf393cd33ae6b3964fc7d8038b01","after":"e7a4d2b407f69dd9a757dfba5ede1a66a50e188a","ref":"refs/heads/master","pushedAt":"2024-07-25T16:00:38.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"ZippeyKeys12","name":"Zain K Aamer","path":"/ZippeyKeys12","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9499189?s=80&v=4"},"commit":{"message":"[CN] Use `Filename.concat` instead of `^` where appropriate","shortMessageHtmlLink":"[CN] Use Filename.concat instead of ^ where appropriate"}},{"before":"6c6bdf979fd59dc6067df26bf646429da6c62fd7","after":"63ed5d042853844375aa557f9c23e829306e7dc8","ref":"refs/heads/bcp-mlifiles","pushedAt":"2024-07-25T14:12:28.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"bcpierce00","name":"Benjamin Pierce","path":"/bcpierce00","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7014411?s=80&v=4"},"commit":{"message":"Some new (draft / unfinished) .mli files from Apol","shortMessageHtmlLink":"Some new (draft / unfinished) .mli files from Apol"}},{"before":"6c6bdf979fd59dc6067df26bf646429da6c62fd7","after":"979016d39c1caf393cd33ae6b3964fc7d8038b01","ref":"refs/heads/master","pushedAt":"2024-07-24T23:50:07.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"vzaliva","name":"Vadim Zaliva","path":"/vzaliva","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/86581?s=80&v=4"},"commit":{"message":"`store_lock_preserves` proof completed","shortMessageHtmlLink":"store_lock_preserves proof completed"}},{"before":null,"after":"6c6bdf979fd59dc6067df26bf646429da6c62fd7","ref":"refs/heads/bcp-mlifiles","pushedAt":"2024-07-24T20:05:17.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"bcpierce00","name":"Benjamin Pierce","path":"/bcpierce00","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7014411?s=80&v=4"},"commit":{"message":"CN: Add support for bitwise and in spec\n\nAn initial version of this commit had an incorrect type annotation in\n`BW_And` in `compile.ml`; it was inconsequential because it is never\nread/immediately written over by `Welltyped.infer`.","shortMessageHtmlLink":"CN: Add support for bitwise and in spec"}},{"before":"a91db76c44cb0e87bedabec2fe5ab6471068c78b","after":"6c6bdf979fd59dc6067df26bf646429da6c62fd7","ref":"refs/heads/master","pushedAt":"2024-07-24T17:26:50.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"dc-mak","name":"Dhruv Makwana","path":"/dc-mak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7052028?s=80&v=4"},"commit":{"message":"CN: Add support for bitwise and in spec\n\nAn initial version of this commit had an incorrect type annotation in\n`BW_And` in `compile.ml`; it was inconsequential because it is never\nread/immediately written over by `Welltyped.infer`.","shortMessageHtmlLink":"CN: Add support for bitwise and in spec"}},{"before":"324aad0c2fc3d87dfb970cf5cad0d48f99bf8a56","after":"749b056a80dc281ca0ea6e83c29fca8c08e254e0","ref":"refs/heads/cn-bw-and-spec","pushedAt":"2024-07-24T16:56:03.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"dc-mak","name":"Dhruv Makwana","path":"/dc-mak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7052028?s=80&v=4"},"commit":{"message":"CN: Add support for bitwise and in spec\n\nAn initial version of this commit had an incorrect type annotation in\n`BW_And` in `compile.ml`; it was inconsequential because it is never\nread/immediately written over by `Welltyped.infer`.","shortMessageHtmlLink":"CN: Add support for bitwise and in spec"}},{"before":"b54b84bfc0a5a790ed0ae9214bf75f5ec29c10dd","after":"a91db76c44cb0e87bedabec2fe5ab6471068c78b","ref":"refs/heads/master","pushedAt":"2024-07-24T16:49:50.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"cp526","name":"Christopher Pulte","path":"/cp526","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6631650?s=80&v=4"},"commit":{"message":"git: fix formatting commit hash (#420)","shortMessageHtmlLink":"git: fix formatting commit hash (#420)"}},{"before":"a0c90f14fedc3b3cfee1ebc383f755fc92617351","after":"324aad0c2fc3d87dfb970cf5cad0d48f99bf8a56","ref":"refs/heads/cn-bw-and-spec","pushedAt":"2024-07-24T16:46:12.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"dc-mak","name":"Dhruv Makwana","path":"/dc-mak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/7052028?s=80&v=4"},"commit":{"message":"CN: Fix typo and add note\n\nThe type annoatation for `BW_And` in `compile.ml` was incorrect, but\nthis is inconsequential because it is never read/immediately written\nover by `Welltyped.infer`.","shortMessageHtmlLink":"CN: Fix typo and add note"}},{"before":"1c6f2c2cfaa115441a28fb91de972ac6281a2662","after":"b54b84bfc0a5a790ed0ae9214bf75f5ec29c10dd","ref":"refs/heads/master","pushedAt":"2024-07-24T16:40:58.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"cp526","name":"Christopher Pulte","path":"/cp526","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6631650?s=80&v=4"},"commit":{"message":"CN: remove unused modules and script (#428)","shortMessageHtmlLink":"CN: remove unused modules and script (#428)"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEjYrTjgA","startCursor":null,"endCursor":null}},"title":"Activity · rems-project/cerberus"}