coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Iris 4.3 and std++ 1.11 have been released

From: Jesper Bengtson <bengtson AT itu.dk>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>, "iris-club AT lists.mpi-sws.org" <iris-club AT lists.mpi-sws.org>
Subject: [Coq-Club] Iris 4.3 and std++ 1.11 have been released
Date: Thu, 31 Oct 2024 10:58:57 +0000
Accept-language: en-US
Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=itu.dk; dmarc=pass action=none header.from=itu.dk; dkim=pass header.d=itu.dk; arc=none
Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector10001; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=Kgh453AR7nclk5H+2VjrhV0sXZ8zXQLoBy2vQ4Rwvxg=; b=yWWJjxIKwKbSHLPN+DsbmhEXuvK1uYJu7BKP3aHq1TgrR/q2ArbnsmxGe09IjTMqenudTbYuOWxvdSRcixkKOridzyJ0F05Ghfd2Fi1jvybeVcJWQCnh5lU7xwBZvxz/DqY6RpSU/EHXWTPIV2gocBpqKMM/oyfUVRwENRL5fNaqJ3EAfHkEVreqmYOtD1gn93vCXuQMWe83/413iYoDGkbwcoSxJVBgIixZKxhjRF8MTw+Jad8AbhizuYxIsImR441ItbcIgdMtWhC6NImoK56wIn/bCHmiAdDmnqbU+4fda9LS9eSQWIE4AV8h0saayO8qtdhedqPPE5RJZPForA==
Arc-seal: i=1; a=rsa-sha256; s=arcselector10001; d=microsoft.com; cv=none; b=sNZ3UoxuEFMQUoOeNY9g/PIu38M4Ve/f/0EWea2cfD1lGtQ98J/ThgbRc/49xhWOxbFKEYf94qyobvKEZ8OpkdzGndj8ThzBCkXnJtLjm3dh0/rYRg9tMkMwe5A/28fxPKvhBWIJVVyzpevLx2q8xX/SQhFI+J9VrPQ6gUuXK2zRKU/MKOMmeS7oaCngzA83xjhKVPSPkijLL2PRMBn1ZJA8nz/VidQSQs8OnUvrLYgUNo0ePgAjU69j0VRmtzBbLg5ZrrH10Z6DNk+bNw12AC1kIifP4+/M0qRHdnkR9rHWzb4FSX/dLks3tvL2vk1gl1RzdFnLEN8KJ1NElL5hxw==
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=bengtson AT itu.dk; spf=Pass smtp.mailfrom=bengtson AT itu.dk; spf=Pass smtp.helo=postmaster AT EUR05-AM6-obe.outbound.protection.outlook.com
Ironport-data: A9a23:NOHqn61OzYZB3MX3ofbD5Vdwkn2cJEfYwER7XKvMYLTBsI5bpzUHm 2QZUDyDPvnZZWr9edFyOdi+9EgPuJTSyIJjHQM93Hw8FHgiRejtVY3IdB+oV8+xBpSeFxw/t 512hv3odp1coqr0/0/1WlTZhSAgk/vOHNIQMcacUghpXwhoVSw9vhxqnu89k+ZAjMOwa++3k YqaT/b3Zhn8glaYDkpOs/jf8Us05ayr0N8llgVWic5j7Ae2e0Y9V8p3yZGZdxPQXoRSF+imc OfPpJnRErTxon/Bovv8+lrKWhViroz6ZWBiuVIKM0SWuSWukwRpukoN2FXwXm8M49mBt4gZJ NygLvVcQy9xVkHHsLx1vxW1j0iSlECJkVPKCSHXjCCd86HJW0Xm4OhMJVwcB7Q/x90nJjpM0 uBAGj9YO3hvh8ruqF66YsRRvJx+aeDOYsYYsHwmyizFB/E7R5yFW7/N+dJTwDY3gIZJAOraY M0aLzFoaXwsYTUTYhFOUM14xr3u3yOiG9FbgAr9Sa4f6WXVwxBq177FMcbIPNCJLSlQth/J/ z+XojWoX3n2MvSQyBi8qV+nq9TzjB/wQIQtNaKqp9p11Qj7Kms7TUd+uUGAifK+kwu1X89VA 1cF/zIn66k07k2iCNfnNyBUu1aBtx8YHtNVTeAn8lnQzayOulzEQG8ZUjRGddoq8tcsQiAn3 UOImNWvAiFztLqSSjSW8bL8QS6OBBX55FQqPUcsJTbpKfG5yG2epkunogpLeEJ0sjH0Jd006 x23lnBjwpw204sM3aj9+k3biTWxoJSPVhQy+gjcQmOi6EV+eZKhYIurr1Pc6J6s6a6HG0KZs iFsd9e2tYgz4VOlzURhg9nh2Jmo++vDPD60bZtHAcw67zr0k5K8Vdk43dy9TXuF9u4FZSKvb Ey7Vca9InNMFCPCUJKbqL5dxyjnIWYM2Dgluj3pggJyX6VM
Ironport-hdrordr: A9a23:5zyrCq2WtRTQ5P80xWZ9aQqjBTlyeYIsimQD101hICG9Lfb0qy n+pp4mPEHP4wr5AEtQ/+xpoMG7MDrhHO1OkPAs1NCZLUHbUQqTXfdfBO7ZrwEIdBeOktK1uZ 0AT0EcMqy6MbEZt7ec3ODQKb9Jr7e6GcuT9ITjJgJWPGRXgtZbnmVE42igcnFedU1jP94UBZ Cc7s1Iq36LYnIMdPm2AXEDQqzqu8DLvIiOW29KOzcXrC21yR+44r/zFBaVmj0EVSlU/Lsk+W /Z1yTk+6SYte2hwBO07R6e030Woqqv9jJwPr3MtiEnEESttu9uXvUjZ1S2hkF6nAho0idprD CDmWZkAy050QKoQoj8m2qX5+Cn6kdl15aq8y7kvVLz5cP+Xz40EMxHmMZQdQbY8VMpuJVm3L tMxH/xjesjMftR9B6NneQgeisa5XZcm0BS49I7njhaS88TebVRpYsQ8AdcF4oBBjvz7MQiHP N1BM/R6f5KeRfCBkqpyVVH0ZipRDA+Dx2GSk8Ntoic1CVXhmlwyw8dyNYElnkN+ZohQ91P5v jCMK5viLZSJ/VmGZ5VFaMEW4+6G2bNSRXDPCabJknmDrgOPzbXp5v+8NwOlZGXkVwzveoPcb j6IS1lXDQJCj7T4OW1reJ2ziw=
Ironport-phdr: A9a23:lEbeBRNlZdmsLKbcoj4l6namBRdPi9zP1u491JMrhvp0f7i5+Ny6Z QqDvq0r1g+UFtyLo9t/yMPo8InYGlY8qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpV O5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebgtUiDanf79/L xW7oQrMusQVnIBvNrs/xhzVr3RHfOhb2XlmKVWPkRji+8y+5oRj8yNeu/Ig885PT6D3dLkmQ LJbETorLXk76NXkuhffQwSP4GAcUngNnRpTHwfF9hD6UYzvvSb8q+FwxTOVPczyTbAzRDSi8 6JmQwLmhSsbKzI09nzch8pth6xZvR2hvQRyzY7Kbo+IKPpwcKDTc9QGSmROUclcTDBBDZi5b 4cTD+oNIeRVoo/grFUOtxu+AgysCfvrxDBWnX/2xbM10/48GgzbwgMgGd0OsGjPrNXyMqcZT Oe4w7LWwjXFYPNWxSz96I/Och06oPGMQa9wfdDMxkksDg7IiEibpoP5MT2PzOsNr3Sb4PR6V eKpk2Mqqh18rzaty8oohYTFm4AYx1TH+Cllz4s4J9m1RUF4bNK4H5ZeuTyWO5V4TM4/QGxkp js2x7wJt5KmeCUHyIoryhjCYPKJdIiI5wjsVOeXITpghXJlYrO/hw2r/Ui40O38Ucu030hWo SpZiNXMsWoN1xPL5siCUvt9/16t2S2B1gDI8O1EJlo0laXDJ5E9wr4/jJwTsUvdES/yn0X2g 7WadkA59eWu9u/pYa3mq4eTOoNokA3yL7gil86lDegmLAQCRXWX9fq82bH740H0QalGg/Mzn 6XErJzVP8UWq6ukDwJVzoou7guwAjej3dkdgHULMVRIcw+ZgojtJlHOO+z4Aumlg1qxkTdqx u7JM6X9DpjLM3PNiq3ufaxn5E5Z0Aczzc5Q55ZTCrwZL/z8VFP/uMDYAxMgLwG6xOfqBMx61 owFR22DGKiZML7OsVCT4eIvPu+Ma5IPtDblMfgl4OLugmElll8BfKmp2p0XZGq/HvR7P0WZZ X3sgtACEWsQogU+S+nqhEWDUT5VeXmyQ7ox6z4nBI68EIvPWoKgjKaf0CulBJFae35KB1CUH XftbYqEWvMMaCyIIs9mlzwJTaOuRJEn1RGhqA/60L1nLuzP9y0ZqZLjycJ56PDQlR0q8zx7F NyS03uRQGFsgmMIWzg20bhirUBl0FeMzbB4g+BEFdxU//5GTgA6NYfFw+NmD9DyRxnOc8ySS FemR9WmGSs+Qsgww98IeUZ9Gs+tggrN3yqwUPcpkOnBD5stt6nYwnLZJsBnyn+A2rNrxw0tR dIKPmm7jIZ+8RLSDsjHiRPd3+yrb6UHmSXJ6W2ryWuVoFoeVRZxFL7aRjYYfESc5YD4/ELZC rSqFL4PNgpa1dXEL7NLL8b2lhNBXvi1a/rEZGfkuWqrHRuSjpmBaoX2YGIblHHXBU4LjxsU+ 16HKRV4CiT38DGWNyBnCV+6OxCkyuJ5sn7uFifcrimPZkxljf+u/wINwOabQLUV164FvyEor 3N1Gky81pTYEYnIvBJvKYNbZ951+1JbzSTBrQUoNJGmILx5gVg2chhq+U/thF1sEosVqcExt zsxyRZqb6eR0VdPbTSdiJr9PLLLMW701BGzduja2QKWy86Yr58G8+9wsFD/pEepG04lpm1gy MVQ2mCA64/iITcoCc+0e2Npsh9wqvfdfzU34J7S2Tt0K66ovzTe2tUvQuw41hKneNQZO6SBf OPrO+sdAcXmaOkjmlzzKwkBIPgX7qk/ecWva/qB3qeveudmhjOvy2pdssh71QqX+ixwR/Stv d5NyuyE3gaBSzb3jUuw+sHxl4deYDgOH225gSH6DY9Vb6d2cM4FE2Cra8Gww9x/gdbqVRs6v BapClUJxNSufzKTc0G70Q4RnUUbrHq7mDepmiRummJhpa6e0SrShuX6IUZffDcTGy841xG1e 9Xn6rJSFFKlZAUoiha/sEPzxqwB4b96M3GWW0BDOS7/M2BlVKK08LuEec9Grp0y4kA1GKyxZ 06XTrnlrl4UySTmSiFUyTY0ayqtvL34gwE8hGHXfz5j6WHUf81930KV7tHaSuJK2TwuRTVlz zXUTAvZXZHh7ZCfkJHNtfq7XmSqW8hIcCXl+oiHsTOy+WxgBRDXc+mbotT8CkB61Cb604MvT iDUtFPmZYKt0a2mMOVhd00uBVnm6sM8FJss2oc3gZgR3zAdiPD3tTINnGH8Lc5c34r/cGdLS T1Dz9PO4Qfj0VFuNTrVn8SgDirbmJEnPoPnKmoNkjow9cVLFLuZ4PRfkC15r0D5yGCZKflxk zEByOc/vXsTguUHog0onW2WBrEfG1UdPDS5y0zOtojh6v8NIj/1LOvVtgI2h92qAbCcrxsJX X/4fs1nBips9oBlN1mK1nTv64bicd2WbNQJtxTSnQ2T6oodYJ83iPcOgjJqfGznunhwgeQ2i xNyxpa8lImbNiNh/+jqSg4dLTDza84Jr3vngKBRgt2R2aiuAognFjZBD/6KBbq4VTkVs/rgL QOHFjYx/2yaFbToFgia8E56rnjLHsPjJzSNKXIe19knWAiFKRkVnlUPRDtj1M1cdEji1In7f Ux+/DxU+lPotk4G1LdzLxemGmbH+FX0MnFlEt7HakIRt1wK5l+JY5DGqLsrQGcAuMXm9VLoS CTTZhwUXzxTHBXcXxa7eOHpvISI8vDEVLfkaaKWO/PW77QZDqnAxIrzgNY8uW/UbYPXeCElV qJeuAILXGglSZ2Bx3NTFGpP0XqKNpHTpQ/iqHd+9pntqa2yCgyzvdPdWfwOYbANs1i3mfnRb efI3XQgcG8K2M9Uni2aj+ROlF8K1XM0fmH0Q+1Z7HzDEPqLyP8PV0ZJOWQuba4qp+o9xlcfY 8eD04Gsj+cqgKJtUAVODQS5yJPuOJVCInnjZgnOXB/Zbe3fdzOXm5qlb/vkEe8Cy7gO/1i5v TLRe6P6FgyKjCKhFxWmMOUWyTqeIAQbooa2NBBkFWnkStviLBy9Kt5+yzMsk/U4gXbDNGhUN jYZEQsFtrqL8SZRmelyAURs00A9cKytvnjc6OPVbJELrfFsHyJ40fpA52g3wKdU6ycCQ+Fpn CzVrZhlpFTD8KHHxjd8URVIoypGn8rX5QM7YfqfrMMGACyZtBsWpX2dERELu8doBpX0tqZcx 8KO3KP/JTFe8s7FqMsRA8+HTaDPeHElMBfvBHvVFF5ZFXjybT6Z3RYbyavPpRj35tAgp5Phm YQDUOpeXV0xTLYBD1h9WcYFK9FxVy8llriSiIgJ42C/pV/fXpY/3NiPW/SMDPHoMDvcg6NDY k5Cy77+IpgIMYvT2lB/LFV51teveQKYTZVWryttYxVh6l1K62R7R3Yv1ljNRz6XuCJWPNvq2 xk8h015fPgn8yrq7xEvPF3WqSAskU4339L4nTSWdz23J6C1F9IzaWK8pw06NZX1RBxwZAu5k Bl/NTvKcLlWiqNpaWFhjAKP8YsKA/NXSrdIJQMB3fzCLet9ykxS82/0oC0PrfuAE5ZpkxEmN IKhv24VkRw2d8Y7fOTRPPYbkgAW1/jI5mnwkblsiA4GexRRqCXLIHFO4ApQceB4Qkjgtu10t V7fwX0aIDBKD7xy5as3vkIlZ7bdlWS5i+QFcgbpcLXBZ6KB5zqdz4jRGgh2jgVQ0BAamNo+m cY7LxjNDxxpkOTXT1JRcpOdYQBNMZgI/SCKL3/X6LfDncotbdf6SrCNL6fGtb5K0BitRF97R t1VvMpdRsL+ggaEfI/mNOBXkxx1vVayfQzXAqgRI0DbyG9f8ZP4kcYSv8EVJylDUz90aXzlv ++O9AF22KHRV49uOiVIGdZdfnMuBp/gknYA7S0ZVWu5jrpCmgbat2eu9GONVnG5Zt5nLp98h DtBNevupHAW1vbzjlTatJLDO2v9KNJu/MfV7v8XrIqGDPUSSqRht0DbmM9TQHn4CgYn/va0O 4W2Z4p+NLQc7167TkH5hzFnF6/M
Ironport-sdr: 672362ff_CZ8ePLK4+lUwFJQuOTpWoKwHaMTqeKcMM7edSVOYQsvuQf2 md6x2jvJXOws7FFY87aapzKEGx9tclqQrh+UTxw==

Hi everyone,

We are happy to announce the release of Iris 4.3 and std++ 1.11. 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
improvements to iInduction, a new iUnfold tactic, and improved errors in
iInv. For std++, the biggest new feature in this release provides stronger
versions of the induction principles for map_fold, exposing the order in
which elements are processed. Both releases of Iris and std++ now support
dune compilation.

For Iris, the supported Coq versions are 8.19 and 8.20, while std++ also
supports Coq 8.18.

For further details, see the full changelog of Iris at
https://gitlab.mpi-sws.org/iris/iris/-/blob/master/CHANGELOG.md#iris-430-2024-10-30
and std++ at
https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/CHANGELOG.md#1110-2024-10-30.

This release was managed by Jesper Bengtson, Ralf Jung and Robbert Krebbers.

std++ received contributions from Andres Erbsen, Lennard Gäher, Léo
Stefanesco, Marijn van Wezel, Paolo G. Giarrusso, Pierre Roux, Ralf Jung,
Robbert Krebbers, Rodolphe Lepigre, Sanjit Bhat, Yannick Zakowski, and Yiyun
Liu.

Iris received contributions from Benjamin Peters, Isaac van Bakel, Jan-Oliver
Kaiser, Janggun Lee, Michael Sammler, Ralf Jung, Robbert Krebbers, Rodolphe
Lepigre, Sanjit Bhat, Tej Chajed, William Mansky, and Yusuke Matsushita.

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: Iris Chat Room: https://iris-project.org/chat.html.

Best,

The Iris and std++ teams

[Coq-Club] Iris 4.3 and std++ 1.11 have been released, Jesper Bengtson, 10/31/2024