{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":24187206,"defaultBranch":"master","name":"CompCert","ownerLogin":"AbsInt","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2014-09-18T12:27:33.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/8820208?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1720194445.0","currentOid":""},"activityList":{"items":[{"before":"891f2bd29abc3ec5498191b17be600b77cb820f6","after":"f993018b98c99aa8e7e2410b72ed1b945a98a5a2","ref":"refs/heads/master","pushedAt":"2024-07-08T11:36:39.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Update test/ submodule","shortMessageHtmlLink":"Update test/ submodule"}},{"before":"71b249c0aba5f94cb26d7f72e4bcbd44554a679f","after":"891f2bd29abc3ec5498191b17be600b77cb820f6","ref":"refs/heads/master","pushedAt":"2024-07-05T15:57:57.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Improve compatibility with OCaml 5\n\nAdd `-I +str` when the Str library is used.","shortMessageHtmlLink":"Improve compatibility with OCaml 5"}},{"before":null,"after":"e42aaab8fb7df5ec91f31772123a43b63f186b81","ref":"refs/heads/xtype","pushedAt":"2024-07-05T15:47:25.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Update clightgen","shortMessageHtmlLink":"Update clightgen"}},{"before":"411f82b81c93b2736dbcd16ec2ed87d6c51bb72b","after":"71b249c0aba5f94cb26d7f72e4bcbd44554a679f","ref":"refs/heads/master","pushedAt":"2024-07-05T09:53:13.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"PrintCminor: don't quote all local variable names, only those that need quoting\n\nThis greatly improves legibility of the debug .cm files.","shortMessageHtmlLink":"PrintCminor: don't quote all local variable names, only those that ne…"}},{"before":"c6438cf1a22d7ab73301000a05ca0de342f9f164","after":"411f82b81c93b2736dbcd16ec2ed87d6c51bb72b","ref":"refs/heads/master","pushedAt":"2024-07-05T07:55:40.000Z","pushType":"push","commitsCount":4,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Replace `Ctypes.typelist` by `list Ctypes.type`\n\nIt makes the Coq and OCaml codes more legible, and avoids some typelist/list\nconversions.","shortMessageHtmlLink":"Replace <code>Ctypes.typelist</code> by <code>list Ctypes.type</code>"}},{"before":"e6e9f6d2c79f33f3641ed4c49b9bdd4c1ae82c1b","after":null,"ref":"refs/heads/Mbool","pushedAt":"2024-07-05T07:51:41.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"}},{"before":"50770a3ddbd37b5c9923cdfe27cdc92dcc805c1d","after":null,"ref":"refs/heads/gha2","pushedAt":"2024-07-05T07:51:32.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"}},{"before":"afb7fd2e9da90808b6e0fde9a63b9f900c7091c6","after":"c6438cf1a22d7ab73301000a05ca0de342f9f164","ref":"refs/heads/master","pushedAt":"2024-07-05T07:36:11.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Add CI testing using Github Actions (#514)\n\nThe \"build\" job tests all supported architectures under Linux,\r\nusing cross-compilation and QEMU to run the small test suite.\r\nIt also tests AArch64 under macOS, natively.\r\n\r\nThe \"oldest\" and \"latest\" jobs test compatibility with specific\r\nversions of Coq.  They just build the proof and the extracted OCaml\r\ncode, but they do not run any test.","shortMessageHtmlLink":"Add CI testing using Github Actions (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2392001597\" data-permission-text=\"Title is private\" data-url=\"https://github.com/AbsInt/CompCert/issues/514\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/AbsInt/CompCert/pull/514/hovercard\" href=\"https://github.com/AbsInt/CompCert/pull/514\">#514</a>)"}},{"before":null,"after":"50770a3ddbd37b5c9923cdfe27cdc92dcc805c1d","ref":"refs/heads/gha2","pushedAt":"2024-07-05T07:18:05.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Add CI testing using Github Actions","shortMessageHtmlLink":"Add CI testing using Github Actions"}},{"before":"8f5fd33fb4f9594dacbc11597335ec362344c08d","after":"afb7fd2e9da90808b6e0fde9a63b9f900c7091c6","ref":"refs/heads/master","pushedAt":"2024-07-03T09:15:00.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Build: Support TIMING and PROFILING like coq_makefile (#512)\n\nShould be useful to identify changes more precisely in the Coq benchmarking.","shortMessageHtmlLink":"Build: Support TIMING and PROFILING like coq_makefile (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2346291629\" data-permission-text=\"Title is private\" data-url=\"https://github.com/AbsInt/CompCert/issues/512\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/AbsInt/CompCert/pull/512/hovercard\" href=\"https://github.com/AbsInt/CompCert/pull/512\">#512</a>)"}},{"before":"2ca39a2801d333abcfa3d691620d03abde4e7e37","after":"8f5fd33fb4f9594dacbc11597335ec362344c08d","ref":"refs/heads/master","pushedAt":"2024-06-16T15:42:29.000Z","pushType":"pr_merge","commitsCount":8,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Merge pull request #513 from AbsInt/Mbool\n\nAdd `Mbool` memory chunk to improve compilation of computations at type `_Bool`","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2350619408\" data-permission-text=\"Title is private\" data-url=\"https://github.com/AbsInt/CompCert/issues/513\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/AbsInt/CompCert/pull/513/hovercard\" href=\"https://github.com/AbsInt/CompCert/pull/513\">#513</a> from AbsInt/Mbool"}},{"before":"9f7668658844d9400608b3c2ca28c87c73713ae7","after":"e6e9f6d2c79f33f3641ed4c49b9bdd4c1ae82c1b","ref":"refs/heads/Mbool","pushedAt":"2024-06-13T09:08:18.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Give \"bsel\" builtin the Tbool return type","shortMessageHtmlLink":"Give \"bsel\" builtin the Tbool return type"}},{"before":null,"after":"9f7668658844d9400608b3c2ca28c87c73713ae7","ref":"refs/heads/Mbool","pushedAt":"2024-05-24T11:41:50.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Strengthen the type preservation results in Ctyping.v w.r.t. type _Bool\n\nNow, a value of type _Bool is 0, 1, or Vundef.\nAlso: introduce and use Val.norm_bool_cases.","shortMessageHtmlLink":"Strengthen the type preservation results in Ctyping.v w.r.t. type _Bool"}},{"before":null,"after":"10f8d6c76e89f84eabd4ae1d1f4f62fd3591e578","ref":"refs/heads/boolcast","pushedAt":"2024-05-20T15:46:33.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Stricter semantics for bool -> bool casts and test on bool values\n\nIn both cases, require that input value is 0 or 1; otherwise the cast or the Boolean value is undefined.\n\nThis makes it possible to generate simpler code for loads and casts with _Bool types.","shortMessageHtmlLink":"Stricter semantics for bool -&gt; bool casts and test on bool values"}},{"before":"c20c38a0eaac9e987d3ae65eb79597e6ca99a8b0","after":"2ca39a2801d333abcfa3d691620d03abde4e7e37","ref":"refs/heads/master","pushedAt":"2024-05-06T14:20:53.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"make clean: don't recurse into \"test\" directory","shortMessageHtmlLink":"make clean: don't recurse into \"test\" directory"}},{"before":"6019bc41556473897155259e3d15c5d689185569","after":"c20c38a0eaac9e987d3ae65eb79597e6ca99a8b0","ref":"refs/heads/master","pushedAt":"2024-05-02T14:59:40.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Bump version number for next release","shortMessageHtmlLink":"Bump version number for next release"}},{"before":"3505be515559a8524c174a2068d944646a072df5","after":"6019bc41556473897155259e3d15c5d689185569","ref":"refs/heads/master","pushedAt":"2024-05-02T09:00:37.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Remove tools/xtime.ml, moved to the small test suite repo","shortMessageHtmlLink":"Remove tools/xtime.ml, moved to the small test suite repo"}},{"before":"330dd44c077e3995f0e8690b8f9cc5cdf9478ae4","after":"3505be515559a8524c174a2068d944646a072df5","ref":"refs/heads/master","pushedAt":"2024-05-02T08:49:59.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Updates for release 3.14","shortMessageHtmlLink":"Updates for release 3.14"}},{"before":"901425a8be68b0351715bf44edef78040fd00f12","after":"330dd44c077e3995f0e8690b8f9cc5cdf9478ae4","ref":"refs/heads/master","pushedAt":"2024-05-01T17:46:40.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Use absolute URL for test/ module\n\nShoudl work better with private clones of this repository.","shortMessageHtmlLink":"Use absolute URL for test/ module"}},{"before":"901425a8be68b0351715bf44edef78040fd00f12","after":null,"ref":"refs/heads/test-as-submodule","pushedAt":"2024-05-01T17:30:38.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"}},{"before":"11dc3df96273b3b25b9c59298e2d21a4591c2c82","after":"901425a8be68b0351715bf44edef78040fd00f12","ref":"refs/heads/master","pushedAt":"2024-05-01T17:23:22.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Setup test/ as a git submodule","shortMessageHtmlLink":"Setup test/ as a git submodule"}},{"before":null,"after":"901425a8be68b0351715bf44edef78040fd00f12","ref":"refs/heads/test-as-submodule","pushedAt":"2024-05-01T17:21:05.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Setup test/ as a git submodule","shortMessageHtmlLink":"Setup test/ as a git submodule"}},{"before":"9b74b3c63f57c35f7a271345f4d4fc0956ab83c4","after":"11dc3df96273b3b25b9c59298e2d21a4591c2c82","ref":"refs/heads/master","pushedAt":"2024-05-01T15:56:40.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Update Changes, continued","shortMessageHtmlLink":"Update Changes, continued"}},{"before":"a5f370678ee445e9e354621c7e1405096143a39d","after":"9b74b3c63f57c35f7a271345f4d4fc0956ab83c4","ref":"refs/heads/master","pushedAt":"2024-04-29T08:57:51.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Update Changes in preparation of next release","shortMessageHtmlLink":"Update Changes in preparation of next release"}},{"before":"b4ca7f2aef3903701ca1bb5a3e1f04e789b8d19e","after":"a5f370678ee445e9e354621c7e1405096143a39d","ref":"refs/heads/master","pushedAt":"2024-03-30T17:38:59.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Replace one `intuition` by `intuition auto`","shortMessageHtmlLink":"Replace one <code>intuition</code> by <code>intuition auto</code>"}},{"before":"3fa22695fc4bf7f5bef7ee80ee0156788021a97b","after":"b4ca7f2aef3903701ca1bb5a3e1f04e789b8d19e","ref":"refs/heads/master","pushedAt":"2024-03-30T16:05:56.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Improved constant expansion for ARM\n\nIn order to avoid some problems with code size we don't want to emit the\n`movt/movw` instruction when code size plays a role.\n\nFurthermore we can remove `literals_in_code` since it always `true` and\nif it would be `false` it would also use `movt/movw` and thus only work\nif the target supports Thumb2.","shortMessageHtmlLink":"Improved constant expansion for ARM"}},{"before":"95fb36ed699f23af2e8fa06d2714416cbca96833","after":"3fa22695fc4bf7f5bef7ee80ee0156788021a97b","ref":"refs/heads/master","pushedAt":"2024-03-30T15:50:55.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Replace one `intuition` with `intuition auto`","shortMessageHtmlLink":"Replace one <code>intuition</code> with <code>intuition auto</code>"}},{"before":"a2e4ed62fc558d565366845f9d135bd7db5e23c4","after":"95fb36ed699f23af2e8fa06d2714416cbca96833","ref":"refs/heads/master","pushedAt":"2024-03-20T08:18:21.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Use movt/movw in ARM mode too (#503)\n\nThese instructions are available in both modes as soon as the processor supports Thumb2.","shortMessageHtmlLink":"Use movt/movw in ARM mode too (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1892257624\" data-permission-text=\"Title is private\" data-url=\"https://github.com/AbsInt/CompCert/issues/503\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/AbsInt/CompCert/pull/503/hovercard\" href=\"https://github.com/AbsInt/CompCert/pull/503\">#503</a>)"}},{"before":"e1ea590dddd1ac2f7b1b25187c38d6e44cebcdd6","after":"a2e4ed62fc558d565366845f9d135bd7db5e23c4","ref":"refs/heads/master","pushedAt":"2024-03-19T18:00:55.000Z","pushType":"push","commitsCount":5,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Coq 8.19.1 is supported\n\nWith a few warnings.","shortMessageHtmlLink":"Coq 8.19.1 is supported"}},{"before":"2e37443c5b20d3e06ecc7f44dc1f765707bc255b","after":"e1ea590dddd1ac2f7b1b25187c38d6e44cebcdd6","ref":"refs/heads/master","pushedAt":"2024-03-18T15:29:18.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"xavierleroy","name":"Xavier Leroy","path":"/xavierleroy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3845810?s=80&v=4"},"commit":{"message":"Semantics of free(): remove requirement size > 0  (#509)\n\nZero-sized blocks work fine, with a slightly different proof of memory\ninjections in Events.v.\n\nCo-authored-by: xavier.leroy@college-de-france.fr","shortMessageHtmlLink":"Semantics of free(): remove requirement size &gt; 0 (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2105912096\" data-permission-text=\"Title is private\" data-url=\"https://github.com/AbsInt/CompCert/issues/509\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/AbsInt/CompCert/pull/509/hovercard\" href=\"https://github.com/AbsInt/CompCert/pull/509\">#509</a>)"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEeYW2TAA","startCursor":null,"endCursor":null}},"title":"Activity · AbsInt/CompCert"}