coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Johannes Hostert <s8johost AT stud.uni-saarland.de>
- To: coq-club AT inria.fr, iris-club AT lists.mpi-sws.org
- Cc: research AT ralfj.de, mail AT robbertkrebbers.nl
- Subject: [Coq-Club] Iris 4.1 and std++ 1.9 released
- Date: Thu, 12 Oct 2023 10:06:41 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=s8johost AT stud.uni-saarland.de; spf=Pass smtp.mailfrom=s8johost AT stud.uni-saarland.de; spf=None smtp.helo=postmaster AT theia.rz.uni-saarland.de
- Ironport-data: A9a23:/LcUl6nsL/dX0itvopEJ4Fbo5gwaIkRdPkR7XQ2eYbSJt1+Wr1Gzt xIcC2+AaK3cZ2H0f9klYY6+8RwCuZTQzoM3QAtvqSk1Q1tH+JHPbTi7BhepbnnKdqUvb2o+s p5AMoGYRCwQZiWBzvt4GuG59RGQ7YnRGvymTrSs1hlZHWdMUD0mhQ9oh9k3i4tphcnRKw6Ws LsemeWGULOe82Ayajl8B56r8ks1562q4WlA5zTSWNgS1LPgvylNZH4gDfrpR5fIatE8NvK3Q e/F0Ia48gvxl/v6Io7Nfh7TKyXmc5aKVeS8oiI+t5uK3nCukhcPPpMTb5LwX6v4ZwKhxLidw P0V3XC5pJxA0qfkwIzxWDEAe81y0DEvFBYq7hFTvOTKp3AqfUcAzN1IVGpqM844pdomXz1O6 fMXNRM9YAu60rfeLLKTEoGAh+w/LMTqNcUFqDd9yzCcFv8vW5TKRamM6dIwMDUY35sSW6eAI ZVfMmMHgBfoO3WjPn8MWJA5nOCzmlHkbyBU7k+TpO8s6mHJyAV33P7hPbI5f/TUFZkFxR/D9 goq+UzpHQEWMMW8zwOazVmqosmVowj0ZJAdQejQGvlC2gTInzdDWXX6T2CTqv6gz0W6Rth3M F0R4iNorK4o9UXtQMOVYvGjiGKEsx8VHcBCVfA86USWw6PO5w+fCi4IQ1atdeDKqucQHRd22 BypwO+4W2BvrLKaVFGt+Kyt+Gba1TcuEUcOYioNTA0g6tbloZ0ugh+ncjqFOPLp5jESMW2tq w1mvBTSlJ1P3JRRhv7TEUTv3WP998Shohsdu23qsnSZAhRRSKPNi2aA0lHS9/xah1KSTVSH1 JTvs5bAtbpVZX1hvBeESf8JFbelj8tp3RXAgVNuFt875XKw/X/mZolZ+jV3IksvPstsld7Vj K375lk5CHx7ZSXCgUpLj2SZUJ9CIU/IToqNaxwsRoASCqWdjSfelM2UWWae3nr2jG8nmrwlN JGQfK6EVChLVvw7nWLtGbxNi9fHIxzSI0uNHvgXKDz5jdKjiIK9E+xUWLdzRr9ms/vf/lW9H yh3bpbQkU43vBLCjtn/q9dIdAtafBDX9Lj6ptFLbeWDLxEuFmY7EPTR3LUuYIpog7Y9qws71 i7VZ6Os83Km3SevAVzSNBhLMeq/Nb4h9ihTFXJ3Yj6VN40LOtvHAFE3LMdsItHKNYVLkZZJc hXyU5/RWKsSFWubpml1gFuUhNUKSSlHTDmmZ0KNCAXTtbY6L+AQ0o6+IFnc52MVAzCptMAzh bSl20mJCdAAXgluRoKeIv6m01r77zBXlfNQTnn4BIBZWHzt14x2dA33rPs8eP8XJTv5mzC16 gexADUjn9frnbMbytfyqJ6hk5aICMp7R0pTIHna5+25NA7c5WuS/rVDW+epIxHbbmTGx6GiQ eN3kdX6DuAOpw9YgrVSArxE478MzIbslYR71SVhJm3ANH6wO4NjI16H/MhBjbJMzblnojmLW lqD191ZGLeRMub3OQY1CC86SN+cxNcomjX2xtYkEnXQvSNY0uKObhRPAkOqlidYEopQDKok5 uUQ4Ogt9A21j0sRAOas1yx72TyFES0dbv8BqJofPY7MjzgrwHFkZbj3KHf/wLOLWuV2HngaG B2mr4ucuO0E3WvHSWQ5KlbV1+kEhZguhgFD/GVfG3u3wOj6lt0F9zwP1wRvVQlE7AR148QqM EhRCkBFD6Gv/TBpuct9Y16RCzxxXB20x0ig5GYKxUv4TlapXFPjNGcSG/iA12FH/nN+fgp0x qC5ymHkWm3QJfPag3I4XE15oKbNTdd05g3Infm6Leu4Hr0RQznssomxb0Um9jrlBsIQghXch O9IpexfV4zyBRQykYYaVbaI8Ks2Yw+VAlBCTdVK3rI7LUuFdB6cgTGxel2MIOVTLPn0wGqEI s1JJPMXcS+h1SyL/wspNYRVL5BaxPcWtcc/IJX1Lms7spyanDpjkLTU0gPc3GYLYdFfofwRG 7PrVQCpMzKv3CNPumr3ssN7FHKyYoAEaC3CzemFyrg1OKxZgt58U3MZ8+WSjy2OPRpF7iCkm lrJR5XrwtxIzaVumIrREZt/OTikFOOrasO29FGcjtcfS/LOLsbEiC0NoHbFIQl9HOUcSvZ3p 5u3of/120LO54xvYUuEwpOEFLVCv+uyV+9HMsjyFWRoshaDfOTO4BIz3X+yBrIUsdFa5+ihH xCZbunpf/Eret5t/l9nQAkALAQ4FILccbbGmSOxi9+uGyot+1XLA/3//EC4cFwBUDEDPqPPL zPdutGs14h+l5tNDhpVPMNWKcZ0D3G7UJR3auCrkyeTC1SppVawurHCsx4EwhOTA1mmFPfK2 770diLcRj+T5p6RlMp4trZstCI5FHx+2Ok8XnwM8u5M1gyVMjQ0EvQ/A74nVLdkyyD87cStL nWFJm4vEj70Ujl4YA3xqoarFBuWAusVfMz1PHo19keTcD27H56EHKAnzCp7/nNqYXH2+YlL8 z3FFqHYZXBdA62FRNr/ItSngepmz7XA1DQV/0G4iMX7GRIXB7lM2HEJ8M+hk8DYO5mlqakJD TFdqaN4rIWTUlLsHYB9fX8QAxgQpjfmyTluYSrnLBP3pdCA1OMZoBHgE7ib71DABfjm4JYVW W77AXaL4iWN03UJvaIvt5QljMeYzB5N8teSdMfeeOHZo018BqnL8S/PcerjgfzOIDJiLm4=
- Ironport-hdrordr: A9a23:w1QyCaglbdfEPOGqiVImwhFtunBQX9523DAbv31ZSRFFG/FwyP rCoB1L73XJYWgqM03IwerwQ5VpQRvnhP1ICPoqTM2ftWjdySCVxeRZgbcKrAeQfBEWmtQ96U 4kSdkHNDSSNykxsS+Z2njfLz9I+rDun86VbKXlvg5QpGpRGsNdBnJCe2Km+zpNNWx77PQCdK a0145inX6NaH4XZsO0Cj0sWPXCncTCkNbLcAMLHBku7SiJlHeN5KThGxaV8x8CW3cXqI1SvV Ttokjc3OGOovu7whjT2yv66IlXosLozp9uFdGBkc8cLxTrk0KNaJ56U7OPkTgpqKWE6Uoskv PLvxA8Vv4Dpk/5TyWQm1/AygPg2DEh5zvJ0lmDm0bupsT/WXYTF9dBrZgxSGqW12MQ+PVHlI 5b1WOQsJRaSTnamj7m2tTOXxZ20mKpvHsZl/IJhXA3a/peVFYRl/1ewKpmKuZDIMvI0vFjLA CoNrCZ2B9iSyLYU5kehBgp/DXjZAV0Iv7MeDl+hiXc6UkroJk+9TpW+CVXpAZ+yLstD5ZD/O jKKaJuifVHSdIXd7t0AKMbTdKwEXGle2O7DIu+GyWSKEg8AQO7l7fnpLEuoO26cp0By5U/3J zHTVNDrGY3P0bjE9eH0pFH+g3EBDzVZ0Wk9uhOo5xi/rHsTrviNiOODFgojsu7uv0aRsnWQe y6Np5aC+LqaWHuBYFK1QvjXIQ6EwhWbOQF/tIgH16eqMPCLYPn8uTdbfbIPbLoVS0pX2vua0 FzKQQb5P8wnHxDdkWI8CQ5AUmdBHAX1agAYZTy7qwU1JUHMJFKv0wclUm5j/v7WgF/jg==
- Ironport-phdr: A9a23:+fLdlh+dhhDXmv9uWQy1ngc9DxPPW53KNwIYoqAql6hJOvz6uci4b AqCtb401gOBHd2Cra4e1ayO6+GocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wE ZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmjmwbalyI Ri1ogndq9cajIR/Iao11hfFv2FEdutIyW5pP16fgwrw6sKt95N/7ipcvO4s+dRdWqvgZaQ4S rJYDDUiM28r4cDgqAfOQwiS6HYCS2saihVHDRTL4xH8RZfxrzD1tvFh1ymAPM35Vq47VDK/5 Kp2UhDoiSMHNzkk8GHLj8F7kaxWrA69qxF53oXbZ52bOvpgc6/EZN8XWHBOUdtNWiNcBIOyc 5cAD/QcMupGsoLxo1sDoQa7CQSqGejhyCJHhmXu0KIm0OovHw7J0wI+EdwOrXrZss74O70OX e2v1qTE0SvPYvFQ1Dzg6IbIaBchofSUULx0dsrRyVMgFwXDjlqOsozuIjGb1uMWs2iH8eVgT /6vgHMgpgFqoTWvxMAsionOhoIO1lDJ7j55wJooJdKlUkJ7fNikEJpJuyGBLYR5WNkiQ2Vyt yY817IKo4O0czYTxZkh2hXQZOCJfZKS7RL/SOaePy14hHR9db+8hhu/7UauxOPgW8e60ltHr SRLnNnDuHwTyxDe98eKRuZh8kmvxzqB2QTe5+BZLEwpm6fVJIAsz7A/mJYOs0nOGDL9lkvxj K+TbEok++6o5vzmYrX8p5+cLJZ4ihnkMqQpmMywH/g3MhQUU2ic4+S826Xv/U3jT7VOlPE2i bXWsJHEKsQduqG2HRdZ0oki6xajCzepys8XkWMGLFJCYB6HipDpO1DXLPDjA/a/mE6gkDBxx /DJJrHuHpXNIWLFkLfuY7l970lcyAUpwdBa+p1ZDKwKLvHrWkLpqdDVABA0PxawzuvmEtlw1 JkSVGySDqOBLa/fv1CF6vgrLuSNfoMYtyrxJ+In6vPhi3IyhEUTcrOz3ZQNbXC1BvRmLFudY XrrmtoBDWcKsRQ/TOPwklGCSz9Sa2yvX6I65zE3EZmmAp3ZSYC3hLyOxiG7EYBMam9bFF+AC Xbod4OaVPcQcC+eP8FsnzMeWbWlSoItzxOjuBX0xrZ6NubU/zcXtZPn1Nh7/e3TkhQy+CRvD 8me0WGNSGF0nmQTRz8qx61/ulB9ykqe3qRinvxYE91T6+pSUgggL5Hc1eh6BMr0Wg3cZNuGV UipTs2gAT4qVt0x2cMBY15hG9W+iRDOxzemD6cPl7OXHJw07r7c33/pKslhzHbGzbAtgEUiQ stSLmKrnbV/9gjWB47RiUqVjaeqdaIG3C7M7miP12SOvFsLGDJ3BK7CRDUUYlbchdX//ELLC bG0TfwmKApajMWGN6FibtzykU4AQe/ifc/BeCS2gWjjKwyPw+aua4rjfWMQx239D1MYnhoPt SKdZQo5BiC6v0rFECFiU0/pYgb3+OBkrHq9Qgk4wlfZPAVay7Op90tN1rSnQPQJ0+dZ4U/Jy h1xFVe5hJfNDsaY4hFmZONaaM8851FO0STYsRZ8N9quNfMqnUYQJiJwuU6mzBBrEsNYi8F/t yMoywp1Mr6wy09ce3WF25G1IbTeMG37+hzpZ6OFkkrG3oOu87wUoO89t02luQioEkQ49HAyy IlX1Hub/YniFxYPXdTsVEdy7BFzvbXTZCV7646HnWZ0P/yStTnPk8ksGPNjyhukeIJHN7iYE QbpD8AAL9SuJe0j3UK7KA8CPaVJ/acuO8qge72K1cZHJc5GmzSrxSRC6YF5iQeX8jZkD/XPx 9ADyu2Z2Q2OU3H9ik2gu4b5g9IMYzZaBWe5xSX+YewZLqRvYYYGD3uvKMyr151/gZDqQXtR6 F+kARsPxsaofROYa1G10xdX0AwbpnmumC3wyDIR8Xlhtfqd2yzJ2PjKbwYaNihWQmgnll7lO 4y9idxcUEXpJwklmR255FrrkrBBrfcaTSGbSkNJci7qamB6B/Lr6vzTPYgQrshx4kA1GKymb FuXS6DwuU4f2iLnRC5FwSwjMiqtotP/lgB7j2SUKDByqmDYcId+30S6hpSUSPhP0z4BXCQ9h yPQAw32JImr+tWTjIvrqfyjWyS8UJwWaiDi14eJsif96WAgUnjd17ij38bqFwQ3y3qxzIloU iXPtwrUeZX22+KnN+MiZUBhHlv17cY8Fow0we5SzNkAnHMdgJuS538Ol2z+ZM5a1azJZ30IX TcXwtTR7WAJwWVbJ2mSj8L8X3SZmY56YsWiJ3gRwmQ75txLD6Gd6PpFmzF0qxy2t1CZbf94l zYbgfwgjRxSy/pZug0tyT6BKqsOAEUeICrt0g+B5sq6paNbImqiObS9z0txm9m9AarK+1oAH ienPMhkRnY4594aUhqEyHDp74D4ZNTcJckesBGZiVaIjuRYLo4wiutfgCNmPWznunh2g+U/j BFowdS7pN3ecDkrrfz/XVgDb26QBYtb4DzmgKdAk9zD2omuGs4kATAXRN7zSuruFjsOtPPhP gLIETsmq37dF6CMeG3XoEpgsX/LFIimcn+NI3xMh84yRh6dI1dDqBsIQTl8g5g4Uxujzdble UF1oDwcrA2dyFME2qdzOh/zX32K7hz4aDA0T4ODBAFK8w0E+kHUdNeX5/h3FidUuJGs5l/oS CTTd0FDCmcHXVaBDlboM+y15NXOxOOfA/K3M/rEZbjd4fwbTfqDwoijl5d35zvZfNvaJWFsV rdovygLFWA8AcnSnC8DDjAahz6YJdDOvw+yo2V+5sWvuPXzBFC2vtfJWuUUbpM3vErq5MXLf ++I2HQgcmoeh81KmSeOluRYhg5aijkwJWP1Se1S63WdHviIwv0HUkU1OXshbZkaqPtlhEFbM MrfwLsZz5Zeifg4QxdAXF3lwYSyYNASZnq6LBXBDVqKM7KPIXvKxdv2aOWyU+8YiuIcrBC2t TuBdi2rdj2eiznkUQyuOuBQnWmaOhJZooS0bhdqDyDqUtvnbhSxNNI/gycxxPU4gXbDNGhUN jYZEQsFtrqL8SZRmelyAURd7ndkJK+eiWCE6eidMZ8fq/9iBCgym+8bqHU2xr1J7T1VEfx4n CyBy7wm61qik+SJ1n9mSE8X8WoN1dzN4gM5YPa8lNEIQ3vP8RMT4H/FDh0Lo4AgEdjzo+VLz cCJkqvvKTBE+taS/M0GBsGSJtjUVRhpeRfvBjPQCxMICDCxMmSKzVcNkvaS8WaJhoMmt5Sqh ZwPD6RSXUYxH/UWTEhoVo9nQt8/TnY/nLiXgdRdr2K5twXUTd5Gs4rvSvKfAPypMiTfkL9FI gAByKn8JIIfcIH2kR8HCBEyjMHBHEzeWspIqytqY1ovoUlDx3N5S3U6x0Pvbg7FCJ47Cf65n xdwkBk4fOIssSzl6k0zL1zG4ic9whFZcTDNmiyMfHjsKqb1RohfES79sUR3Pp6pG26dgiWpg VFocirCRvdKhrJ6cWlthEnQtMkWccM=
- Ironport-sdr: 6527a917_OEvXyF9EvbLIT6md26/lLWTXUQdDzOu8RiuH5yFfYouQeDp RaTjwUERLGGYihnBAWjnt9Bkc8+8T20NyRg2WBQ==
Hello everyone,
We are happy
to announce the **release of Iris 4.1 and std++ 1.9**. 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.
This Iris
release mostly features quality-of-life improvements, such as
smarter handling of `->`/`<-` patterns by
`iDestruct`, support for an arbitrary number of Coq intro
patterns in the Iris proofmode tactics (`iIntros`, `iDestruct`,
etc.), and support for immediately introducing the postcondition
of a WP specification via `wp_apply lemma as "Hpost"`.
The biggest
changes and new features are:
* Logically
atomic triples now support private (non-atomic) postconditions,
and the notation was changed to not clash with Autosubst any
more. Existing users of logically atomic specifications have to
update their notation, see the full CHANGELOG for more details.
* The
meaning of `P -∗ Q` as a Coq proposition has changed from `P ⊢
Q` to `⊢ P -∗ Q`. If you are only using the Iris proofmode, this
will not make a difference, but when writing proof scripts or
tactics that `rewrite` or `apply` Iris lemmas, the exact
position of the `⊢ P -∗ Q` matters and this will now always be
visible in lemma statements.
* `iCombine`
is starting to gain support for a `gives` clause, which yields
persistent facts gained from combining the resources. So far,
this remains mostly experimental. We support `↦` and the
connectives of ghost theories in `base_logic/lib`, but support
for `own` and custom cameras is minimal and will be improved in
future releases.
* Some
initial refactoring prepares Iris for eventually supporting
transfinite step-indexing.
* New
resources algebras have been added: `Z`, `max_Z`, `mono_Z`, and
`mra` (the monotone resource algebra of https://iris-project.org/pdfs/2021-CPP-monotone-final.pdf)
For std++,
the highlights of this release are:
* `gmap` and
related types are re-implemented based on Appel and Leroy's
[Efficient Extensional Binary Tries](https://inria.hal.science/hal-03372247), making
them usable in nested inductive definitions and improving
extensionality. More information can be found in Robbert
Krebbers' Coq Workshop talk, see https://coq-workshop.gitlab.io/2023/
* New
tactics `ospecialize`, `odestruct`, `oinversion` etc are added.
These tactics improve upon `efeed` / `edestruct` by allowing one
to leave more terms open when specializing arguments. For
instance, `odestruct (H _ x)` will turn the `_` into an evar
rather than trying to infer it immediately, making it usable in
many situations where `edestruct` fails. This can significantly
shorten the overhead involved in forward reasoning proofs. For
more information, see the test cases provided here: https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/tests/tactics.v#L114
For
further details, see the full changelog of Iris at https://gitlab.mpi-sws.org/iris/iris/-/blob/master/CHANGELOG.md#iris-410-2023-10-11
and std++ at https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/CHANGELOG.md#std-190-2023-10-11
Iris
4.1 and std++ 1.9
support Coq 8.16-8.18.
This
release of Iris and std++ was managed by Ralf Jung, Robbert
Krebbers, and Johannes Hostert.
This
Iris release received contributions from Amin Timany, Arthur
Azevedo de Amorim, Armaël Guéneau, Benjamin Peters, Dan Frumin,
Dorian Lesbre, Ike Mulder, Isaac van Bakel, Jaemin Choi, Janine
Lohse, Jan-Oliver Kaiser, Jonas Kastberg Hinrichsen, Lennard
Gäher, Mathias Adam Møller, Michael Sammler, Paolo Giarrusso,
Pierre Roux, Rodolphe Lepigre, Simcha van Collem, Simon Friis
Vindum, Simon Spies, Tej Chajed, Yicuan Chen, and Yusuke
Matsushita.
This
std++ release received contributions from Dorian
Lesbre, Herman Bergwerf, Ike Mulder, Isaak van Bakel, Jan-Oliver
Kaiser, Jonas Kastberg, Marijn van Wezel, Michael Sammler, Paolo
Giarrusso, Tej Chajed, and Thibaut Pérami.
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.1 and std++ 1.9 released, Johannes Hostert, 10/12/2023
- Re: [Coq-Club] Iris 4.1 and std++ 1.9 released, mukesh tiwari, 10/12/2023
- Re: [Coq-Club] Iris 4.1 and std++ 1.9 released, Ralf Jung, 10/12/2023
- Re: [Coq-Club] Iris 4.1 and std++ 1.9 released, mukesh tiwari, 10/12/2023
- Re: [Coq-Club] Iris 4.1 and std++ 1.9 released, Ralf Jung, 10/12/2023
- Re: [Coq-Club] Iris 4.1 and std++ 1.9 released, mukesh tiwari, 10/12/2023
Archive powered by MHonArc 2.6.19+.