coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Tej Chajed <tchajed AT mit.edu>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] Iris 3.6 and std++ 1.7 released
- Date: Mon, 24 Jan 2022 08:00:00 -0600
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=tchajed AT mit.edu; spf=Pass smtp.mailfrom=tchajed AT mit.edu; spf=None smtp.helo=postmaster AT outgoing.mit.edu
- Ironport-data: A9a23:6eGIcKBz4amNqxVW/1rlw5YqxClBgxIJ4kV8jS/XYbTApDgh1TxTy mYXXG7TMvzYNGCnedsiatmw/E8Fup6Dz9IwOVdlrnsFo1Bi+ZOUX4zBRqvTF3rPdZObFBoPA +E2MISowBUcFyeEzvuVGuG96yE6jMlkf5KkYAL+EnkZqTRMFWFx2XqPp8Zj2tQy2YHjX1vU0 T/Pi5S31GGNi2Yc3l08sPrrRCNH5JwebxtF1rCWTakjUG72zxH5PrpHTU2CByeQrr1vIwKPb 72rIIdVUY/u10xF5tuNyt4Xe6CRK1LYFVDmZnF+A8BOjvXez8A/+v5TCRYSVatYo22jwYtL2 uUdib6hEF4DIKDSitsPcyANRkmSPYUekFPGCX+ircOUzkvJNX7t37NjAFxe0Y8wo7YxUCcUp bpBcVjhbTjb7w6y6K6wSuBui8gLKcj3eo4TpxmMyBmAUqh9G8qcEs0m4/dd9TgtjctMI8rGS NAFaRtiVz7PUy9mbwJ/5JUWxbrx3SKXnydjgFmSvO8853XZ5Bdg1aDkdtvTYN2DA8tP9nt0v UrB4nj2BRAcO5mW1CaFtyvqg+7T2y73Rer+CYFU6NYyqgPI/H4jWCE0RALii+e0lFyBSfJmf hl8FjUVkYA+80miT9/YVhK+oWKZshN0Zza2O7BmgO1q4veIizt1FlToXRYaN4N77J5eqSgCk w7Wz4mwVFSDpZXMESrFnop4uw9eLsT8EIPvTSgZUQQC4t/s5YgukhKKF5BmEbLzg9Hocd0R/ 9xohHZi71nwpZdQv0lewbwhq2n0znQuZlVkjjg7pkr/smtEiHeNPuREE2Tz4/daN5q+RVKcp nUCkMX2xLlQUcvcynbTGL1cROnBCxO53Nv03wcH834JqWjFxpJfVd44DMxWfh4xY59UJVcFn meJ6FIIjHOsAJdaRfYqOtnqYyjb5a3pDs/sXfDJdddSfoM5dQmc4CByeFKdl2fj2FQhmqE5P pOcftfEMJrpIfoP8dZCfM9EieVD7nlnnQv7HMmrpzz6j+b2TCPLGN8tbQvfBshkvfjsiFiEr L5i2z6ilk83vBvWOHeHqOb+7DkicBAGOHwBg5UHL7HYels/RjhJ5j246epJRrGJVp99zo/gl kxRkGcBoLYmrXGYewiMdF55b7bjAcR2oX4hYn4pPEru1nQ+ON794KAafpoxXL8m6O0/naMqE qVZI52NUqZVVzDK2zUBdp2h/oZsQxKm2FCVNC2/bTljIpNtHlSb+tLtcgb12jMJCy676Zk3r 7G6iVHeQIZFSgh/VZ6EZPWqxlK3nH4chOMuDxaWf4UPIB3hqdE4JTbwg/k7J9A3BS/CnjbKh RyLBRo4pPXWp9Nn+tf+g63Z/ZyiFPFzHxYHEmTWseS2OC3d8jbxyINMSr/WLzfASGzz+aOtI +BU07fxPOBexARGtI91ErBKy6Mi5oe/+uEHklg8RHibPU62Dr5AI2Wd2ZUdvKN6wLIE6xC9X ViC+4UHNLjVatnpFkUdeFgsYuiZj6pGnSTO4vM0Jkq/7TJr/P/eF0BTI1+BhDEEdOl5N4Ysw OEAvs8K6lDv10R3bore1i0EpX6RKnEgUrk8ss1ICoHcjAd2mEpJZobRC3Or7ZyCAzmW3pLG/ tNJaGv+a7VgKo7qdGcvGn/M2+UbgJUS/h1G0Tfu4rhPdsXt3pcKMN95qFzbjTi5Cj1C0v41N 2R2X6GwDbvb5C9m3aCvQEj1czysx3SlFojZzloV0mDVUiFEk4ALwHIVYY6wwazSz46QkvW3M l1VJKYJnAsGpP3M4xY=
- Ironport-hdrordr: A9a23:ztMBHq1KlQp9/BOtzDr2tAqjBIYkLtp133Aq2lEZdPU1SL3+qy nAppQmPHPP6Qr5O0tPpTnjAtjjfZq0z/cciuMs1NyZLWzbUQWTXeVfBEjZrgHIKmnR8uZc0O NHaKhxCNr5CBxfgdzh6Ae1V/YMqeP3k5xASd2z856ld25XV50=
- Ironport-phdr: A9a23:1bDp/x06JHweUmHssmDOkwoyDhhOgF0UFjAc5pdvsb9SaKPrp82kY BaFo68wxwaRBc2bs6sC17CP9fi4GCQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgH c5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTajf79+N gu6oAXeusULnYduNrs6xh/VrndVYehbyn1kKU+Jkxrg+su8+YNo/jhNtf4m68NOS7jxcb4iT bxfAjQmMmQ169PuuBLeUwaB5WYSX3sPnBZQDAfL8B/1XpHqsivnreV9wzWVPdf3Tb8vRzuv6 bpgRQLyhycGMz4593zXitB1galGrh+tuwBzzojJa4yTKfFwfL7SfckCSGVOXshfWS9PDJ6iY YQTFOcOJ/pUopPnqlcSsRezBw+hD/7vxD9SgX/22LU33fo/HgHEwQctAdIOv27WrNrrKagZT Oe4zLXUwjXDdfxW2yny55XTfxAkoPGMQah8ftTMxkkyDg7IiEibpoP5MT2PzOsNr3Sb4PR6V eKpk2MrtRx9riSry8oxloXHiIYYx1/G+Ch9zog5O9K1RUB/bNOkEpZdtD+XOoVyT84mQWxlp Ts3x7MYtZO6cyYH1pQpyhjCYPKJdIiI5wjsVOeXITpghXJlYrO/hw2r/Ui40O38Ucu030hWo SpZiNXMsWoN1xPL5siCUvt9/16t2S2B1gDI8O1EJlo0laXDJ5E9wr4/jJwTsUvdES/yn0X2g 7WadkA59eWu9u/pYa3mq4eBO4J3kA3zNr4iltK8DOgiLwQCQnCX9fqg2LDn50H0Q7VHgucon qXEtJ3WP9kXq62nDwJTz40t8QywDy2839QdhXQHLExKeBaAj4XxPFHOPez4Dfi4g1Stljdry OrKPrjgApXRNHTMjqrufatl505dzgo808xf6opJBrwCOv7+XlX9uMLbAxMjLgC43v7rCNBn2 YMfXWKPDLWZMKTXsVKQ+uIgP+mMa5UXuDnjNvco/PvujX4lmVMHY6amwIYXZGiiHvt6O0WZf WbsgtAZHGgWuQo+VfXmh0GGUT5OfHm/RLk85zE+CIK+F4jPXIGtgLqb3Ce6BJJafG5GCkrfW UvvIo6DQrIHbD+YaptqlSVBXry8Qacg0wuvvUn00ew0APDT/3gkuJCr/9h85eDf3UUu/jx9D cmR+2SMUyd5kn5eFGx+57x2vUEokgTL6qN/mfENTbS7httMWwY+b9vHyvBiTsr1UUTHd8uIT 1CvRpOnByswR5Q/2YxGeF5zTvOliB2LxC+2G/kNjbXeGJc0+6DR01D0Jto7xnrbh+E6l1dze sJULiW9g7JnsQ3aBorHiUKcwrqhda0e0SLl8Wafi2eCoRIQSxZ+BIPCW31XfU7KtZL560fFG qepEqgiOxBdxNSqLbZWZdroi1oAQfb/ftnSfgpdgk+WAhCFjvOJZYvuISAG2TnFTVIDmEYV9 GqHMg43AmGgpXjfBXpgDwCnZUSk6uR4pH6hKy18hwiXc01s0aa08R8JlLSdTf0UxLcNpCYmr X19Al+829vcD9fIqRBmee1QZtY04VEP0my81UQ1IpegJqJvinYbchgxsk/zll12BohGjck2v SYy1gMhYamc0V5Ha3aZxcWpavuGbDOiukn2OMu0khnE3d2b+7kC8qE9olTn5kSyE1Y6tm9g2 J9T2med4ZPDCEwTV4jwWwA57UsfxfmSby8j6ofTzXApP7Ozt2qIx9kpDekoxj6lfssZPa+ZX ly6A4gBCs6iJfZ/0USibhsGMex68a8oec6qarHVvczjdPYllzWgg2Nd5Yl72U/Z7CtwRNnD2 JMdyu2Z1A+KP9vlpG+oqdu/2YVNZDVIW3G61TChHolaIKt7YYcMD26qZcyx3NR3wZD3CTZU8 1uqBlVO38HMG1Lac1f91A9d2WwSoGDhlCelhzB5iDAmqKOD0TeGmrSkJVxdaigSHSFrlh/0L JKxjswGUUTgdAUvmBa/pCOYj+BaqKl5M2jPUBJNdinyIXtlV/j4vb6DbshTrZIw5HwHFrX6O wDcE+euxnlSmznuFGZf2j0hIjSju5Gj2gd/lHrYNnF46nzQZcB3wx7bot3aX/9YmDQcF0waw XHaAEaxO96x8JCajZDG56qiXGKoVJBfWSzq0cWNuDbxtiV6RAaymfy+gIitDQM62C322/FvV DmOoRrhKNqOtezyIadseU9mA0X54sxxF9Rlk4c+s5oX3GATmpSf+XdU2Xe2K9hQ3rjyKWYcX TNeicCA+xDrgQcwSxDBj5K8THiWxdFtIsW3cn9DkDxo9NhEUe+V9OAWxHsz/Rzi9ESJJqIh1 jYFlal3uDhFxbpV/lJqlHn4YPhaHFEEb3W80UvOsYr49OINOC6uaeTijRo4wpb/XPfa5VsAE HfhJsV7TWkvqJomdgqLiiGWiMmsecGMP4tD8EzSylGYyLIJYJMpyqhT1Ww2fzik+yVikbJzj AQyj8jq+tnBcTgrpOXjXns6fnX0f59Bo2Gr3OAEzoDOmNrzVpR5RmdQA921HLTyTGNU7bO9a 06PCGFu8SjdROuZQ17ZsR026CiSdvLjf3CPeCtEkZMyFF/GdQoP2UgVRGlowMJ/T1r6gpK+N h4nrjEJugym9l0VkLIuaUa5CD+6xk/gay9oGsbOakALqFgTtgGNdpbCpuNrQ3MHpNv88UrUd jTdN10ADHlVCBPYQQ65eOD0v5+ZqbjfXLfbTbOGYK3S+7MDEabYg8PylNI4pnHWaY2OJiUwX 6J9gBcYGyoiQYKB3G9WAy0Py3CdMIjB+Uz6oHYp6JrmrJGJEEru/dfdWuUUbY4pokzqx/nfc LXJzCdhdWQJiNVQnjmRlOhZggJV0HgmdiHxQ+1a5WiUF/yWwfARV1lBN0YRfINJ9/5uh1Mcf 5KCzIqqjPgp07Y0EwsXDAew3Jj1O4pTfz/7bQmXQxzWfLWeeW+SmJCxOP/iD+QO1KMM8Eft3 FTTW077YmbazGivCUjpaacUy3vBdB1G5NPkLkYrUDC+CoqgMlribpd2lWFkmONpwCqbbyhBb 34hLSYv5vWR9X8K26siXTUQtTw8dbDCwnrAp+jAdsRP76YtW3Uv0bsCuTJjl+Ed7TkYFqUrx W2L/4Uo/g/gzrPqqHIvUQIS+G8U1MTQ5gM7YPyfr8UcEXfcoEBUsjXWUE9M/oA6TIe36+cKm pDOjP6hcWgStYmPu5FGXo6Mb5jbVRhpeRvxRGyNXFFDEGbtajGZ2RAayqHa92XJ/MFq9t61x 8FIE+IAEgZsSLsbEhg3RYxfZs4nD3V+yuDd1IlSvx/c5FHQXJkI58CaEKjLWLO2cm7f1f4eP VMJ2e+qdNVDcNe9ghYyLAE9xdSCGlKMD4oV/ms4Mklu+x8LriQ5FD1WuQqtaxvxsiVLSbjtw lhs0Vc4P7hqrmek4k9rdACS+W1qyBB3wI+1x2jWKma5Lb/sD9sOVmyu7hd3a8m9GlsoCG/61 U18aGWeH+8X1eI/MzkxzlaD5tNOAaIOF/UZJkVLmrfOP6tuiRMG9m2m3RMVv7ObT8E/0lR1N 8TxyhAIkwN7MIxvffOWfvMQiAMKwPrJ5HPg1/htklVGeABXqTrUJHBO4R1SceN4byuwor42s VPEwWIaPjZUEaJt+K4PlAt1OvzcnXi4jPgZcxn3abXZd+TD5yDBjZLaGApukBpTxw8fpugwi JZ5NBDKMiJnhLqJS0ZTbJSEdlwTNpsNsiGCJ2HU763M2c4nZtX7SaaxE6nW8/xIykO8QFRwT tRKtIJYRcPqiR2CSKWvZL8DwhEw6Am5P02LSuxTfw6GmysGpMf5y4Jr2Y5aJXcWBmA1MCO84 qvbq10nnLy0R884JG8TRIcDKjQ9X8jf+WYRvnJLCCS737ACxQ6O4CX9qmLWASW0btxoYOqYa EFpAdCyvycy9aS7kl2R+ZLbQgOyfdVksdvS5e5IkI2HDOlIVqFz9UPVho9TR3mnT3TOGsXzL J/1DutkJd3yAXKnXlHtvCktQYHqNdKgNaaPmwrlA41TtcHe1TQnf6dRDxk4HBF976EG7aN4P 0gYZoYjJATvvEI4PrC+JwGR1pOvRXysIH1YVasXy+LyfLFRwyc2C43ygHI9UpE3yfW2+k8RV dkLiB/Z3/Oqe4hZV2D6BHVcfwzFoSdxmXJmM64+xeI2wRWAtld5UXjDbOtydGlNpM0xH3uVP Gl5DWs+SBmZjJaF7wKxnvgT8yZbg9dIwLhFvXz57fq9KHqnXK2mr4mQsjJ1NIhg8usrYcq6e 5jj1tuWhDHUQZjOvxfQVSe7E6Afgd1MOGdCR/IOn2g5OMsAsI4H6EwrV854KaYcbctk7r2sd zdgCjYfiCEDUIbVliAJgu6+1rfykxaMNpkuLVZX1fcKystYSCNwbi4E8eW7UJ7KkmafVmURC AAO8QtL5QQP0IpxYqbo7JeCH/oug3ZG5vlzVCXMDJxh8VD2H3qXjVbPQ/Kki+W13AhWwZoEM /EcRQJwDklbyKBTl1duJb1qefF4Vmvitz6UM072oTC1oANJDFxQ1YvZe0CqVeL4
- Ironport-sdr: 84rikO9gCEP13l5YSIqwogHtvGQgsUtztmdfQXQU+jjWzjE3dhx5CdJcFJZTVOMnvvnqowSV1C SUWbFw6u2BthNX+kt2gzHXo6JfCpBZR3jvwGjMdpwUSu73flm52jtHEQA0GvF1JCJBkxtbZGhT hbkg77KDpTuDaSyFBO53T68q4zrivOwlXxPmc4u2j1mpssPt2XgT0cv0xZ9uAcXx7HSN4SrRHv ziTNPlNxMymfJT4JGl12PNAudfCi+YsLQHxCi1s5nPTGm8D/V+L7xXj3fMB0pg7Kkii1MKWVWK CCv/QHyKrSFOosfqZrM0cMPo
Hello everyone,
We are happy to announce the release of Iris 3.6 and std++ 1.7. 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 and most notable changes of Iris 3.6 are:
- Coq 8.15 is now supported, while Coq 8.13 and Coq 8.14 remain supported.
Coq 8.12 is no longer supported. - Support for discardable fractions (
dfrac
) has been added togmap_view
authoritative elements, and to themono_nat
library. See below for otherdfrac
-related changes. - A new
mono_list
algebra provides monotonically growing lists with an
exclusive authoritative element and persistent prefix witnesses. Seeiris/algebra/lib/mono_list.v
for details. An experimental logic-level
library wrapping the algebra is available atiris_staging/base_logic/mono_list.v
; if you use it, please give feedback on
the tracking issue
iris/iris#439.
Further details are given in the changelog at https://gitlab.mpi-sws.org/iris/iris/-/blob/master/CHANGELOG.md#iris-360-2022-01-22
This release was managed by Ralf Jung, Robbert Krebbers, and Tej Chajed, with
contributions from Dan Frumin, Jonas Kastberg Hinrichsen, Lennard Gäher,
Matthieu Sozeau, Michael Sammler, Paolo G. Giarrusso, Ralf Jung, Robbert
Krebbers, Simon Friis Vindum, Tej Chajed, and Vincent Siles. Thanks a lot to
everyone involved!
For std++, Coq 8.15 is newly supported by this release, and Coq 8.11 to 8.14 remain supported. Coq 8.10 is no longer supported.
This release of std++ was managed by Ralf Jung, Robbert Krebbers, and Tej Chajed, with contributions from Glen Mével, Jonas Kastberg Hinrichsen, Matthieu Sozeau, Michael Sammler, Ralf Jung, Robbert Krebbers, and Tej Chajed. Thanks a lot to everyone involved!
For further details, see the full changelog at https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/CHANGELOG.md#std-170-2022-01-22
Both packages are available in the Coq opam registry. For further information and installation instructions for Iris and std++, see the respective project websites:
If you have any questions, feel free to reply to this email, or join our Iris community chat room.
Best,
The Iris and std++ teams
- [Coq-Club] Iris 3.6 and std++ 1.7 released, Tej Chajed, 01/24/2022
Archive powered by MHonArc 2.6.19+.