coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Ralf Jung <research AT ralfj.de>
- To: coq-club <coq-club AT inria.fr>, Mailing List for the Iris Logic <iris-club AT lists.mpi-sws.org>
- Subject: [Coq-Club] Iris 4.2 and std++ 1.10
- Date: Fri, 12 Apr 2024 15:21:12 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=research AT ralfj.de; spf=Pass smtp.mailfrom=research AT ralfj.de; spf=Pass smtp.helo=postmaster AT r-passerv.ralfj.de
- Ironport-data: A9a23:Se+7TqA1ckCR7xVW/0nnw5YqxClBgxIJ4kV8jS/XYbTApDNz0WdUy 2YeXDrUPvmLZjOgKt4kPISy8k0FscCHxtdlOVdlrnsFo1Bi+ZOUX4zBRqvTF3rPdZObFBoPA +E2MISowBUcFyeEzvuVGuG96yM6j8lkf5KkYMbcICd9WAR4fykojBNnioYRj5Vh6TSDK1rlV eja/YuHZzdJ5xYuajhIs/7a8ks11BjPkGpwUmIWNagjUGD2zCF94KI3fcmZM3b+S49IKe+2L 86rIGaRows1Vz90Yj+Uuu6Tnn8iGtY+DiDS4pZiYJVOtzAZzsAEPgnXA9JHAatfo23hc9mcU 7yhv7ToIesiFvWkdOjwz3C0usyxVEFL0OavHJSxjSCc5xXDInnX0cd1MEI3IMoHosJUMGVkp MVNfVjhbjjb7w636Kj+UuB3nck5Mo/xNYcRuDdswFk1D95/GcGFGf6So4UDgnFh26iiHt6GD yYdQSBidxnJeRZPEk0eDJw82uul7pX6W20E9gvK9PFni4TV5Etv1LT8Gdn4Q/fJHPpHx2eWr zvEx12sV3n2M/TElWTeqyj17gPVpgvwX5tXH7ml/NZxkViLzyoSDgcXXB21u5GEZlWWQZdHI lcP9zAw67I78EKpCNXwN/GlnJKalkYZCthrAd8h1AKM1+3LuyK6N2wuHwcUPbTKq/QKqSwWO k6hxoywX2024O3OEhqgGqGoQSSaFQV9EIPjWcPnZVFdizUbiNtv5i8jt/46eEN15/Wscd0K/ xiErTIlm5IYhtMR2qOw8Djv2m31/MiXFlRrt1qPAgpJCz+Vgqb4P+REDnCGt559wHqxFwHY1 JT5s5HAvLFQZX1zvHXdEI3h441FF97ebGOH2AQ2d3XQ3z2m53+9cMgJqD57LkcBDyr3UWKBX aIS0CsPjKJu0IyCNvAmO9vrW5t3lMAN173ND5jpUzaHWbApHCfvwc2kTRf4M7nFwRZyw5Isc 4yWa9itBns8AKFqhmj+DeQE3LNhgmh0yWrPTNqph16qwJiPVk6zEL0lCVqpavxmzaWmpA6Oz c1TGfHXwDpiUcr/QBLtz6gtEX4wI0MWO7XKuu1MV+vaIgNZCGArUPDQ5rU6er1apadel8aW3 3ecRkR35kj030PWJQTXe0FceLbmXMt8n0kaJg0pB06jgFI4ULas7YAeVpo5RqYm/+pd1sxJT +EJVsGDI/ZXQBHV0m45Qbiki6I6bzWtpwaFHxT9UQgFZ5Q6GjD4oI71TDXg5AwlL3SRt/Jnh 5aCywmCY54IZzo6PfbscPj1km+A5ykMqtlTAXnNDMJYInj30Y5QLCf0sP87DucMJTjHxRqYz wymOggZl8acv74K9MT1uo7co7eLC+deGm9oL1vf55uyNgjY+TOH6q1EW+CqYzvcdT3V/IOPW OZr9Mz/YcY3xAtyj4lBErhQ3f0f4fnrrORk1QhKJijAQGmqLbJCGUO4+/dzmJdD/IIEhjvua HmzooFbHZ6rJPLaFEUgIVt5T+abitARtDrgzdU0B0TY9R5I7L+OUBhRDSKtkw1YFqN+a6k+8 NciuekXyg2xsQUrOdC4lRJp93yAA3gDcqc/vLQYPdPbsRUqwVR8fpDsMC/6z5WRYdFqMENxA DurqIfdprZbnGzuTmESECXT4O9jmpg+ghBG41scLVCvmNCepPsW3gVUwAsnXDZu0RRL/OJiC FdFb3QvC/21wA5po8xfU0SHOQJLXkSZ83Os7Wo5rjTSSk3wW1HdKGE4B/22w3kY1GBhZRlew qCTzTf0cDTtffyp5BAIZ2xel6XBQ+Bypyr4o+L2O+SeHpI/Xyjpvb/2W0oMtCncIJ0QgG/pm LBU2dheOIzBGwwemakZM7Wh9K8xTUmELVNSQPs686IuG3rdSQ6I2jOPCh6QfOFNLdP46Gu9M chPJ91OZTu6xi2hvjAWPo9SAr5WzdoCxssORaPvHkEC64CglztOtInB0BT+iEsAYcRcoexkJ qz/Lzu9Q3Gt311KkGrznex4E2ufY+hcQjbj3eqwod47J7havM5CKUgNg6aJ5VOLOw5a/jWRj gPJR4nS68dAkY1MvY/dIp9vNjWOC+HYdbq3qVioktF0c9nwH9/EtFoVpnnZLg1mB+YtdOotp 4udkuzc/R3jh6k3YVD7ipPaNqhu5OeOZsR1HP/zDkFnmXqlZJexzToFomy2EMkc2pcVrMyqX BCxZ8aMZMYYEYUVjmFcby9FVQ0REeLrZ6PnvjmwtOmIFgNb6wHcMde77jX8WAm3rMPT10HWU WcYespC5+y0aKxWQQcNHOprGYE+OlbnV6lge9CZWfywEDyzml3b0lf9vUNI1N0JIiDs/AXGD VbtXBH6ehb0tKygIBRxrdlpphNOZJpiqbBYQ6/ekuKaTxigBWoIL6IRPP3qz32SfjPajPnFW d0GUIfu5egRk9iJndUQLekPhjuiO9E=
- Ironport-hdrordr: A9a23:fDA8zKl7QFJ0lod+H1ogC/GGTAHpDfI73DAbv31ZSRFFG/Fw5P rOoB19726RtN9xYgBEpTnkAsO9qBznmaKdjbNhXotKPzOIhILLFuxfBOLZqlWKJ8SUzJ8+6U 4PSchD4ZHLY2RHsQ==
- Ironport-phdr: A9a23:IKse4BXrt0DEEAHemwH1FJRv1szV8KwVXzF92vMcY1JmTK2v8tzYM VDF4r011RmVB9SdsqwdwLSP+4nbGkU+or+580o+OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF 95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba12I RmssAnct9QajYRjJ6os1xDEvmZGd+NKyGxnIl6egwzy6sCs8pB97i9eoegh98lOUaX7e6Q3U 7lVByk4Pm42+cPmqwDNQROA6XUAXGoWlAFIAxXe4xHhQpjxqCr6ufFj1yScIMb7UKo7WTWm7 6dsVR/olCIKPCM3/W3LlsB9ir9QrQm/rBJj3YHbfICVNOJ/fqzDe9MaWXFBVdtVWyBYH4+wc 5cDA+8HMO1FrYfyukEOoAO9CweiC+zgxCFGiH/r06Im3OosCh3G0Q86Et4SrHjYstf4OaEPW u611qnIyjDDYutK1zjn7IjIfA0qr/WRXbJ2fsra1E4iFxnbgVWLt4PqJSmV2fgNs2WA9epvT +avi2Alqw1rvzeg2N4hh4/UjY0a1l7K7z92wJopJdKmUk57Z8apHptfuSyGKYZ4Qt0vT31qt Ss0xbMLpZC2cTQFxZonyBDSduCLfouG7x//UOucLjd2iG9rdr+imRq/9Uqtx+38WMSyzV1Eo C1FktzWuXAM0Rze8smHSuF8/ke6wDqPzxrT6uZGIU8qiaXbN4QtwrkqlpocqUjDGzf2mETvg K+NeEQk4fKk6+P9YrXpvpOTK490hRv4MqQhhMO/BeM4MgcUU2ie5Oux0qDo807hQLhSk/E6j q3UvIrEKckVuqK1GRFZ34gi5hqlCzqr0MwUkWcbIF5Zdh+KipbmN03LLf/jA/eyjUqjnTJpy v3IIrHtHpDAImXNnbfvYLlw7lBQxxAtwt1c4p9ZC78ML+jxV0L0sNHXEhA0PxGyzu36Fth90 p4eWXmTAqCHKqPcrF6I5+MxLOSUeIMYviv2JeI/6P70l3A5nEcQfam30psTb3C1Bu5mL1yBY XX2mdcBCnkFvhAgTODwkl2NSzpTZ3iwX64m+z40FpqqDYbFRo+znLyMxDq3EoFSa2xcFFyBH 2vke5+aV/oCaS+eOMtsnzwcWbikUYAh1BWutAHgy7pgK+rZ4jcYuoz41Ndr/eLTjw099TxvA sSHyW6NS290nmESSzArwq9zuUp9xUyb3qhin/NYDcBT5+9OUgoiKJLQ1/Z6BMzqWgLdYteJT 06rTcmhATEoV94+39sOY1tmFNi5lRDC3y+qA6cPmLCRBZw09Ljc33nrKMpnxXbGzvpps15zS cxWcGaim6Q3owPUHsvCl1iTv6esb6UVmiDXoiPL6GOPuEBeX0ZUUL7ZFX4YfAPKrdmxx1nDV PeKDrsmOUMVyNSDMe5BbsDjpVFHX+v4ftHGYieqhHz2AgyHkOCido3vLl8U2CuVKlUCnEhH5 3udOAEkDSeJuWvaAj4oGV+5MBCkyvV3tH7uFhx89AqNdUA0kuPtonb95NSZQvIXhfcfvTs57 i5zBBC71s7XDNyJo0xger9daJUz+gQPznrX4ip6OJHoNKV+nhgGaQ0ipU712hxtAYVoi8Euo nFswAchYbmA3gZ5fiiDlYv1JqWRL2Dz+B61bKuDwFzF3d+M8acn8v08pVelsAz6XlE6/SBf2 sJOm2CZ+o2MDAcWVsfpVV0r8hFhu7zASjN4/4rPznB2L++uuzvM2ZQlCYPJ0z6GeNFSeOOBH Q72SIgBAtS2bfctgx6vZw4FO+Zb8Og1Odmnfr2IwvzjOuEohz+ggWldheI1mkuR6ypxTPLJ1 JcZ0rmZ2AWATTL1kFamtIj+h4lFYTgYGmf3xzLjAcZdYah7fIBDDmnLQYX/3Nhlipf3UH5w7 lenCVFA1MLoMRueYlrh3BFBgFwNqC/vki+5wjpo1jAx+/PHjWqUmLykLkFZfD8WFwwAxR/2L IO5js4XRh2tZgktz16+4FrigrNcvOJ5JnXSRkFBe273KXtjW+2+rOnnAYYH5ZU2vCFQSOn5b 0qdT+u3uRYB3ir5FGt23jk/eTPstpizzHkYwCqNaW1+qnbUY5Q63xrE6dXGTv55xDMCSis+h TSdVRCsetKu+9uTjZLKtOuzAnmgWpNkei7u1YqctSG/6AWGGDWHluuo0p3iGAk+imrg0sVyE D7PtFD6a5Xq0KKzNaRmeFNpDRny8ZgyFoZ7m4o2zJYevBpSzo+Y5ncOi2zzGc9S3az8KnYAD TIG2N/a5gH51VYrdyrYgdiiDjPHmZUnNoTya3hewi8n6sFWFKqYid4M1TB4pFa1t0OZYPRwm Csc1ep77Xcbh+8Tvw9+hi6ZA70UAQxZJXm1z0XOtYvm6v8MOiD+LOvVtgI2h92qAbCcrxsJX X/4fsxnBips9oBkN0qK1nTv64bicd2WbNQJtxTSnQ2T6oodYJ83iPcOgjJqfGznunhwgfQ2l hFnx5q6lJKOL2tvuq60SE09VHW9d4YI9zfhgLwL1NybxI2mBJ5hMi8CWJXqC/6lWmFapbHsM ACAFyc5o3GQFO/EHAOR30xhqmrGD5GhM3zEQRtRhcUnXhSWI1ZTxRwFRDhv1IBsDRiknYayO Fc8/D0a4UT07wdB2v49fQeqSX/R/U+ten9jQZybZnK69yl67lzOeYyb5+N3RGRD+4G56ReKM iqdbhhJCmcAXgqFAUriN/+g/4uI/++dD+u4Z/zABNfG4fRZTOuNzImz35FO5XOUP96UM2N8S ecy3kRBG3x0U8jUgDQATSULmjmFNpbK4k3nomst9Z75oamjURmKh8PHE7ZINNRz5x26ybyOM eKdnmcxKDpV0I8N2W6dyLUb2w1agCVvej+xVLUY4HeVHeSKwfcRVUVFLXIuZ64qp+om0wJAO NDWkIbw37981bsuDktdEEfmgoevbNALJGe0MBXGAlyKPfKIP26uoYm/bKWiRLlXlOgRuQe3v GPRCUL4Mz2ZnDnBTRmrP+MKgCzRb3k88MmtNw1gD2TuVoeschqgLNp+liE725Uuw2vDLnURK yY6aUpJoL/W4S4S0ZAdUyRRq3FiK+eDgSOQ6eLVf40XvfVcCSNxj+tG4X4+xugd/GReSfdyg ieXss92rgTsjLyU0jQ+GkkryH4DlMeRsE5lI6mc6pRQRSOO4kcW9WvJQxEa74xsDtml00i/4 sLGkKzxbjtPoYu8FSo0HY3MIdmcPWA/dwDgHDDWSgcIH2fD3YT3nUVZnvPU+nDH9vAH
- Ironport-sdr: 6619354a_69vHPt7sG1TMPh0nP7QFSlZrVOA3NWFQ9uDhFUI1hdIXU7G +H8JX7veOM/n/vmydZDCOQd/A2pbgZtvd00iToQ==
Hi everyone,
We are happy to announce the release of Iris 4.2 and std++ 1.10. Iris is a concurrent separation logic framework for Coq; for an overview of the numerous research projects employing Iris, see https://iris-project.org/. std++ is an extended “standard” library for Coq.
The highlights of this new Iris version are:
* We have new laws to "undiscard" discarded fractions, allowing one to update from `DfracDiscarded` to `DfracOwn(q)` for some fresh `q`. This gives rise to new laws for all constructions that use `dfrac`, such as `ghost_map_elem_unpersist : ∀ k γ v, k ↪[γ]□ v ==∗ ∃ q, k ↪[γ]{#q} v`.
* The `gmap_view K V` camera now supports value types `V` that are arbitrary cameras, and lifts their composition to the whole map. The previous `gmap_view` type can be recovered as `gmap_view K (agree V)`.
* The `iFrame` tactic has become stronger for goals that contain existential quantifiers: `iFrame` will now attempt to instantiate these. For example, framing `P x` in goal `Q ∗ ∃ y, P y ∗ R` will now succeed with remaining goal `Q ∗ R`.
For std++, the biggest new feature in this release is the bitvector library with support for fixed-size integers. It is distributed as a separate package, `coq-stdpp-bitvector`. The library is developed and maintained by Michael
Sammler.
The supported Coq versions are 8.18 and 8.19.
For further details, see the full changelog of Iris at https://gitlab.mpi-sws.org/iris/iris/-/blob/master/CHANGELOG.md#iris-420-2024-04-12 and std++ at https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/CHANGELOG.md#std-1100-2024-04-12.
This release was managed by Ralf Jung and Robbert Krebbers.
std++ received further contributions from Mathias Adam Møller, Michael Sammler, Pierre Rousselin, Pierre Roux, and Thibaut Pérami.
Iris received further contributions from Ike Mulder, Jan-Oliver Kaiser, Johannes Hostert, Pierre Roux, Thomas Somers, and Yixuan Chen.
Thanks a lot to everyone involved!
Both packages are available in the Coq opam registry. For further information and installation instructions for Iris and std++, see the respective project websites:
* https://gitlab.mpi-sws.org/iris/iris
* https://gitlab.mpi-sws.org/iris/stdpp
If you have any questions, feel free to reply to this email, or join our Iris community chat room: https://iris-project.org/chat.html.
Best,
The Iris and std++ teams
- [Coq-Club] Iris 4.2 and std++ 1.10, Ralf Jung, 04/12/2024
Archive powered by MHonArc 2.6.19+.