{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":47426662,"defaultBranch":"master","name":"vcfloat","ownerLogin":"VeriNum","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2015-12-04T20:15:36.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/100858532?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1710948477.0","currentOid":""},"activityList":{"items":[{"before":"f59040c5395e04d64d027f88c1501a2df4dfe410","after":"65a9bcabfa17825d0b03e7d9856a00350aeafacc","ref":"refs/heads/master","pushedAt":"2024-07-28T18:34:58.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"andrew-appel","name":"Andrew Appel","path":"/andrew-appel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9196811?s=80&v=4"},"commit":{"message":"Merge pull request #28 from VeriNum/coq8.19\n\nAdapt to Coq 8.19 and the flocq/interval packages that go with it","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2200149502\" data-permission-text=\"Title is private\" data-url=\"https://github.com/VeriNum/vcfloat/issues/28\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/VeriNum/vcfloat/pull/28/hovercard\" href=\"https://github.com/VeriNum/vcfloat/pull/28\">#28</a> from VeriNum/coq8.19"}},{"before":"cf131d6d9b28a692f82f64b92355fd2d10db5872","after":"f59040c5395e04d64d027f88c1501a2df4dfe410","ref":"refs/heads/master","pushedAt":"2024-05-24T19:25:30.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"ak-2485","name":"Ariel Kellison","path":"/ak-2485","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/25615362?s=80&v=4"},"commit":{"message":"Fix suppress","shortMessageHtmlLink":"Fix suppress"}},{"before":"a43370de1e21e69a16aa592b4910ea2b8eaa6fe3","after":"cf131d6d9b28a692f82f64b92355fd2d10db5872","ref":"refs/heads/master","pushedAt":"2024-05-24T19:11:39.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"ak-2485","name":"Ariel Kellison","path":"/ak-2485","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/25615362?s=80&v=4"},"commit":{"message":"Suppress warnings on make","shortMessageHtmlLink":"Suppress warnings on make"}},{"before":null,"after":"10caf1cda152590dd1f32d87e902ecac57d7d527","ref":"refs/heads/coq8.19","pushedAt":"2024-03-20T14:59:52.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"andrew-appel","name":"Andrew Appel","path":"/andrew-appel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9196811?s=80&v=4"},"commit":{"message":"Adapt to Coq 8.19 and the flocq/interval packages that go with it","shortMessageHtmlLink":"Adapt to Coq 8.19 and the flocq/interval packages that go with it"}},{"before":"4b9a6d2d355a7f45d2b351bbfdf5f4d962a36938","after":null,"ref":"refs/heads/test","pushedAt":"2023-12-21T18:34:41.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"andrew-appel","name":"Andrew Appel","path":"/andrew-appel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9196811?s=80&v=4"}},{"before":"6f5e172e6a4cde1eb3f0e7f9b9124e1cf9854296","after":null,"ref":"refs/heads/revert-7-elpi-restricted-compute","pushedAt":"2023-12-21T18:34:17.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"andrew-appel","name":"Andrew Appel","path":"/andrew-appel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9196811?s=80&v=4"}},{"before":"f04070e8241bb21791b85f7a89e6437b5ea4de70","after":null,"ref":"refs/heads/fplib","pushedAt":"2023-12-21T18:34:13.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"andrew-appel","name":"Andrew Appel","path":"/andrew-appel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9196811?s=80&v=4"}},{"before":"c738147de22f65e80826367433ae67a2628bf883","after":null,"ref":"refs/heads/dependent","pushedAt":"2023-12-21T18:34:10.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"andrew-appel","name":"Andrew Appel","path":"/andrew-appel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9196811?s=80&v=4"}},{"before":"6aa6e0cc342d191cb3216ff71ad3144cc674e4af","after":null,"ref":"refs/heads/gentype","pushedAt":"2023-12-21T18:33:46.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"andrew-appel","name":"Andrew Appel","path":"/andrew-appel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9196811?s=80&v=4"}},{"before":"0c6fcc847b536d78c0b5ce7e5277650bf27a31ae","after":"a43370de1e21e69a16aa592b4910ea2b8eaa6fe3","ref":"refs/heads/master","pushedAt":"2023-12-21T18:33:37.000Z","pushType":"pr_merge","commitsCount":25,"pusher":{"login":"andrew-appel","name":"Andrew Appel","path":"/andrew-appel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9196811?s=80&v=4"},"commit":{"message":"Merge pull request #16 from VeriNum/gentype\n\nGeneralized types (not limited to IEEE Binary)","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1689111511\" data-permission-text=\"Title is private\" data-url=\"https://github.com/VeriNum/vcfloat/issues/16\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/VeriNum/vcfloat/pull/16/hovercard\" href=\"https://github.com/VeriNum/vcfloat/pull/16\">#16</a> from VeriNum/gentype"}},{"before":"3205b5525500a67b71fc09de64e510dd58d37a03","after":"0c6fcc847b536d78c0b5ce7e5277650bf27a31ae","ref":"refs/heads/master","pushedAt":"2023-12-21T18:33:10.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"andrew-appel","name":"Andrew Appel","path":"/andrew-appel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9196811?s=80&v=4"},"commit":{"message":"Merge pull request #23 from JasonGross/relax-opam-bound\n\nRelax Coq version bounds in informational opam file","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1908064447\" data-permission-text=\"Title is private\" data-url=\"https://github.com/VeriNum/vcfloat/issues/23\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/VeriNum/vcfloat/pull/23/hovercard\" href=\"https://github.com/VeriNum/vcfloat/pull/23\">#23</a> from JasonGross/relax-opam-bound"}},{"before":"b427da8cbda5755825d3011b0ff41ad5f3aabf0b","after":"3205b5525500a67b71fc09de64e510dd58d37a03","ref":"refs/heads/master","pushedAt":"2023-12-21T18:32:24.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"andrew-appel","name":"Andrew Appel","path":"/andrew-appel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9196811?s=80&v=4"},"commit":{"message":"Merge pull request #22 from JasonGross/coq-native-ignore\n\nIgnore .coq-native folders","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1908062989\" data-permission-text=\"Title is private\" data-url=\"https://github.com/VeriNum/vcfloat/issues/22\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/VeriNum/vcfloat/pull/22/hovercard\" href=\"https://github.com/VeriNum/vcfloat/pull/22\">#22</a> from JasonGross/coq-native-ignore"}},{"before":"367a315cc7a208cc9ff95c7f27e8ce931c71693a","after":"6aa6e0cc342d191cb3216ff71ad3144cc674e4af","ref":"refs/heads/gentype","pushedAt":"2023-12-12T13:59:23.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"andrew-appel","name":"Andrew Appel","path":"/andrew-appel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9196811?s=80&v=4"},"commit":{"message":"Adjust statement of relate_fold_add lemma,\n\nused by the prune_terms tactic, to match the statement of\nrelate_fold_add that appears in my recent pull request to coq-mmaps.\nhttps://github.com/coq-community/coq-mmaps/pull/14\n\nThat way, when coq-mmaps is (soon) made part of the coq platform,\nwe can easily switch vcfloat from using FMaps (the old, obsolete version\nof functional maps) to the new MMaps (which is better).","shortMessageHtmlLink":"Adjust statement of relate_fold_add lemma,"}},{"before":"3b0161166f126ad9b3fb1f1e76868a4c904c681d","after":"367a315cc7a208cc9ff95c7f27e8ce931c71693a","ref":"refs/heads/gentype","pushedAt":"2023-12-06T14:14:15.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"andrew-appel","name":"Andrew Appel","path":"/andrew-appel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9196811?s=80&v=4"},"commit":{"message":"Put the CPP'24 camera-ready pdf in this repo","shortMessageHtmlLink":"Put the CPP'24 camera-ready pdf in this repo"}},{"before":"768f79017d7b36a93ffd8467eaf997358005fb14","after":"3b0161166f126ad9b3fb1f1e76868a4c904c681d","ref":"refs/heads/gentype","pushedAt":"2023-12-04T20:55:41.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"andrew-appel","name":"Andrew Appel","path":"/andrew-appel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9196811?s=80&v=4"},"commit":{"message":"Fix a bug in the Reference Manual, bad chapter heading","shortMessageHtmlLink":"Fix a bug in the Reference Manual, bad chapter heading"}},{"before":"da6cfebf4d7a772b565aaf83989d44241528615b","after":"768f79017d7b36a93ffd8467eaf997358005fb14","ref":"refs/heads/gentype","pushedAt":"2023-12-04T20:47:54.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"andrew-appel","name":"Andrew Appel","path":"/andrew-appel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9196811?s=80&v=4"},"commit":{"message":"1. Remove obsolete license text; (2) tweak FPStdLib interface\n\n1. Delete obsolete copyright notices (and related text) from many files.\nThese remained from VCFloat 1, and they no longer legally relevant\nafter the Qualcomm rights transfer of 2022.\n\n2.  FPStdLib no longer Exports RAux, which means that users don't have\nto do \"Close Scope R_scope\".","shortMessageHtmlLink":"1. Remove obsolete license text; (2) tweak FPStdLib interface"}},{"before":"1a499d3ec2a96fc424b83004cc750098e7b30679","after":"da6cfebf4d7a772b565aaf83989d44241528615b","ref":"refs/heads/gentype","pushedAt":"2023-12-01T16:14:18.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"andrew-appel","name":"Andrew Appel","path":"/andrew-appel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9196811?s=80&v=4"},"commit":{"message":"Refactor to accommodate FPStdLib; adjust jetEngine benchmark","shortMessageHtmlLink":"Refactor to accommodate FPStdLib; adjust jetEngine benchmark"}},{"before":"83b296bb5fc455932cdd0f6e97f75739133a8d97","after":"1a499d3ec2a96fc424b83004cc750098e7b30679","ref":"refs/heads/gentype","pushedAt":"2023-11-30T21:44:55.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"andrew-appel","name":"Andrew Appel","path":"/andrew-appel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9196811?s=80&v=4"},"commit":{"message":"Improve compute_fshift_div tactic so Qed does not blow up in some examples;  tune some of the FPBench benchmarks to get the same quality results in less Coq time, by reducing the Interval bisection depth","shortMessageHtmlLink":"Improve compute_fshift_div tactic so Qed does not blow up in some exa…"}},{"before":"d2d4a91328ea38de520b44a82d29df6a31cd9062","after":"83b296bb5fc455932cdd0f6e97f75739133a8d97","ref":"refs/heads/gentype","pushedAt":"2023-11-29T19:45:30.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"andrew-appel","name":"Andrew Appel","path":"/andrew-appel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9196811?s=80&v=4"},"commit":{"message":"Merge branch 'gentype' of github.com:VeriNum/vcfloat into gentype","shortMessageHtmlLink":"Merge branch 'gentype' of github.com:VeriNum/vcfloat into gentype"}},{"before":"6dbe46b972a935d0bfa2ed82de8df4a4ee9d9a31","after":"d2d4a91328ea38de520b44a82d29df6a31cd9062","ref":"refs/heads/gentype","pushedAt":"2023-11-29T14:32:00.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"ak-2485","name":"Ariel Kellison","path":"/ak-2485","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/25615362?s=80&v=4"},"commit":{"message":"Rename vars for readability","shortMessageHtmlLink":"Rename vars for readability"}},{"before":"0b4d2ccf4d7e4c377deb8a30e891b9c032c1f3b0","after":"6dbe46b972a935d0bfa2ed82de8df4a4ee9d9a31","ref":"refs/heads/gentype","pushedAt":"2023-11-29T14:26:07.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"ak-2485","name":"Ariel Kellison","path":"/ak-2485","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/25615362?s=80&v=4"},"commit":{"message":"Small comments to clarify rewrites in error_rewrites tactic","shortMessageHtmlLink":"Small comments to clarify rewrites in error_rewrites tactic"}},{"before":"75d8756fd8645ce0bf7c2a101e59e5941eba0d54","after":"b427da8cbda5755825d3011b0ff41ad5f3aabf0b","ref":"refs/heads/master","pushedAt":"2023-09-08T20:21:48.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"andrew-appel","name":"Andrew Appel","path":"/andrew-appel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9196811?s=80&v=4"},"commit":{"message":"Merge pull request #21 from JasonGross/fix-native-compiler\n\nSupport coq-native by passing through `COQEXTRAFLAGS`","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1886872956\" data-permission-text=\"Title is private\" data-url=\"https://github.com/VeriNum/vcfloat/issues/21\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/VeriNum/vcfloat/pull/21/hovercard\" href=\"https://github.com/VeriNum/vcfloat/pull/21\">#21</a> from JasonGross/fix-native-compiler"}},{"before":"68118eb2e37dbf2ea7bb0fa58afe9300e78f39a7","after":"0b4d2ccf4d7e4c377deb8a30e891b9c032c1f3b0","ref":"refs/heads/gentype","pushedAt":"2023-09-08T19:11:02.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"andrew-appel","name":"Andrew Appel","path":"/andrew-appel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9196811?s=80&v=4"},"commit":{"message":"Make gentype branch build in Coq Platform 2023.03","shortMessageHtmlLink":"Make gentype branch build in Coq Platform 2023.03"}},{"before":"688347ec4082b49ab118de0a3b8ce041b6518ea6","after":"75d8756fd8645ce0bf7c2a101e59e5941eba0d54","ref":"refs/heads/master","pushedAt":"2023-08-31T19:25:39.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"andrew-appel","name":"Andrew Appel","path":"/andrew-appel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9196811?s=80&v=4"},"commit":{"message":"Update not-the-real .opam file, for informational purposes","shortMessageHtmlLink":"Update not-the-real .opam file, for informational purposes"}},{"before":"35a4c249d41c63a01c66ef67c83c0a8823b567c7","after":"688347ec4082b49ab118de0a3b8ce041b6518ea6","ref":"refs/heads/master","pushedAt":"2023-08-31T17:14:37.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"andrew-appel","name":"Andrew Appel","path":"/andrew-appel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9196811?s=80&v=4"},"commit":{"message":"Merge pull request #19 from JasonGross/17781-compat\n\nStop using `elimtype False`","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1861979163\" data-permission-text=\"Title is private\" data-url=\"https://github.com/VeriNum/vcfloat/issues/19\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/VeriNum/vcfloat/pull/19/hovercard\" href=\"https://github.com/VeriNum/vcfloat/pull/19\">#19</a> from JasonGross/17781-compat"}},{"before":"202bfb0ea1ee0b971baf8eb4b80dec3b0a639533","after":"35a4c249d41c63a01c66ef67c83c0a8823b567c7","ref":"refs/heads/master","pushedAt":"2023-08-31T17:14:15.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"andrew-appel","name":"Andrew Appel","path":"/andrew-appel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9196811?s=80&v=4"},"commit":{"message":"Merge pull request #17 from JasonGross/fix-for-interval\n\nCompatibility with coq-interval.4.7.0","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1837988586\" data-permission-text=\"Title is private\" data-url=\"https://github.com/VeriNum/vcfloat/issues/17\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/VeriNum/vcfloat/pull/17/hovercard\" href=\"https://github.com/VeriNum/vcfloat/pull/17\">#17</a> from JasonGross/fix-for-interval"}},{"before":"e7b5c82f623d0fc441c8e8295d63706cd24fe281","after":"68118eb2e37dbf2ea7bb0fa58afe9300e78f39a7","ref":"refs/heads/gentype","pushedAt":"2023-05-09T15:45:43.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"andrew-appel","name":"Andrew Appel","path":"/andrew-appel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9196811?s=80&v=4"},"commit":{"message":"Finished demonstration of a nonstandard type","shortMessageHtmlLink":"Finished demonstration of a nonstandard type"}},{"before":"33e7f394551dc81a069ca48f9493f0968dbc9941","after":"e7b5c82f623d0fc441c8e8295d63706cd24fe281","ref":"refs/heads/gentype","pushedAt":"2023-05-09T15:10:36.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"andrew-appel","name":"Andrew Appel","path":"/andrew-appel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9196811?s=80&v=4"},"commit":{"message":"Make env_ computational","shortMessageHtmlLink":"Make env_ computational"}},{"before":"59e128c21e67eb2a99a539944900e140556b050d","after":"33e7f394551dc81a069ca48f9493f0968dbc9941","ref":"refs/heads/gentype","pushedAt":"2023-05-09T14:38:24.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"andrew-appel","name":"Andrew Appel","path":"/andrew-appel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9196811?s=80&v=4"},"commit":{"message":"Added a test with a nonstandard type","shortMessageHtmlLink":"Added a test with a nonstandard type"}},{"before":"1d35acf20a4a498e5e6d36cd9b2680e26ceec1a4","after":"59e128c21e67eb2a99a539944900e140556b050d","ref":"refs/heads/gentype","pushedAt":"2023-05-09T13:22:58.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"andrew-appel","name":"Andrew Appel","path":"/andrew-appel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9196811?s=80&v=4"},"commit":{"message":"cleanup in TestFunc.v","shortMessageHtmlLink":"cleanup in TestFunc.v"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"Y3Vyc29yOnYyOpK7MjAyNC0wNy0yOFQxODozNDo1OC4wMDAwMDBazwAAAASLRetQ","startCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wNy0yOFQxODozNDo1OC4wMDAwMDBazwAAAASLRetQ","endCursor":"Y3Vyc29yOnYyOpK7MjAyMy0wNS0wOVQxMzoyMjo1OC4wMDAwMDBazwAAAAMpEHDc"}},"title":"Activity · VeriNum/vcfloat"}