coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Andrew Appel <appel AT princeton.edu>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] VST release 2.9
- Date: Thu, 27 Jan 2022 14:38:46 -0500 (EST)
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=appel AT princeton.edu; spf=Pass smtp.mailfrom=appel AT cs.princeton.edu; spf=Pass smtp.helo=postmaster AT violeteyes.cs.princeton.edu
- Ironport-data: A9a23:wJAHfaxeFoke8zdhdMN6t+fcwCrEfRIJ4+MujC+fZmUNrF6WrkUFm jFMDWuCb6mOMTDzKN8naYq//UhTsJPRndFmSlc9q1hgHilAwSbnLYTAfx2oZ0t+DeWaERk5t 51GAjXkBJppJpMJjk71atANlVEliefQAOOU5NfsYkidfyc9IMsaoU8ly75RbrJA24DjWVvU4 4yq+aUzBXf8s9JKGjJMg068gEg31BjCkGtwUosWOJinFHeH/5UkJMp3yZOZdxMUcaEIdgKOf Nsv+Znilo/vE7jBPfv++lrzWhVirrc/pmFigFIOM0SpqkAqSiDfTs/XOdJEAXq7hQllkPh+8 tUKpJ/qbD0uBY7suPoiaBZeSx1xaPguFL/veRBTsOSNzkrCfmfh0vh1Skote5UC++B8DH1J8 7oVJC1lghKr3rjmhuviEK813ZplcZSD0IA34hmMyRnQFe4rRbjIWOPS/95e1zosgcYIEPrDD yYcQWY1PEqYPE0n1lE/Aa1guO2V2yjGfBoHsmuP/4w971jh01kkuFTqGIeFK4fSGK25hH2wr WXfum/9HxsyL82a0TPD83S2h+aJkzmTZW4JPKO58fpnnFCCy3dVAwZQTUG6p/K0lkm4Hd9TN iT45xbCs4A9zkzsX9qneie/m12kngAjYNVWS9E1vVTlJrXv3y6VAW0NTzhkYdMgtdMrSTFC6 rNvt4+1bdCImOHIIU9x5ot4vhvuYXNLfD9qiTssCFRZvYKz+OnfmzqVFr5e/LiJYsoZ8N0a6 wiQrS41iqkUi6bnPI3jrQ2b21pASrDvQxF9xAjNRW+0hj6Viaa7Zous5ETW/Ptbao2CCEGbv X4PltSZ6qYDAYzleM2xrAclQO/BCxWtaWO0bbtT834JrWnFxpJbVdoMiAyS3W8wWir+RRfnY VXIpSRa74JJMX2hYMdfOtztUJ5wnPm4TIm/C5g4i+aihLAtKWdrGwkyOyatM5zFyiDAbIlmY sjHLpzE4YgyU/w9pNZJewvt+eJ7l3tmmAs/tLjj1RWh2reCY3jdVLEELlaUdeEl/cu5TPb9r r5i2z+x40wHCoXWP3mGmaZOfAtiBSVqWvjLRzl/K7frzvxOQzp6VZc8ANoJJuRYokiivr6Yp y7mAh4BlgOXaL+uAVziV02PoYjHBf5XxU/X9wR1Vbpx83R8M4up8okFcJ47Iesu+OB5lKAmR OJDY9+BBP9CVjPBvTkRcMCl/oBlcR2qgyOIPjakPWRjI8Y+G1SR94+2ZBbr+QkPEjGz5Jk3r LCX3w/GRYYOGlZ5B8HMZfPzl1685CBPmO97U0bSDMNUfUHgrNpjJyDr16RlO9sNLx7O2jyck QuaHE5A9+XKpoY09vjPhLyF8tv1T7MgQhICEjCCv7isNCTc8m6y+qN6Ub6FLWLHSWf52KS+f uEJnfvyB+IKwQRRuI1mHrc1ka9nv4nzp6VXxxhPFWnQawj5EatpJ3SL0JUdtqBJwbMF6wK6V ljVpYtEOLKNNd/oAVMKYgE+KPyZ1PcflyXV67I4LFijvH17+7+OUENzORiQiXEBcOctbt99m epx6tQL7wGfiwYxNofUhy9ZwG2AM3gcXvh1rZodGoLq1lImxw0Qe5DaESOqspiDZ88WbRs0I ziQibbPlrlHgEHZNWIpFH7G0PZag9IDtA0TlA0OIFGAm9zkgP4r3UANrWhvEFgNlhgXgfhuP mVLNlFuIfTc9jhls8FPQmSwFlwTHxae4EHwlwMEmWCxo5NEjYARwLnR+Nph/Xz1N0pCfz9f8 a2V2Wv+Fz3xOtnr3y05VFJirbruQcEZGsjqhpW8B8rcd3UlSWONv0NsTTNgR9jb7QcZj1aBv fNr+u19dar9cyMcvsXXzqGEgK8IRknsyHNqGJlcEWBgIY0YUCmo2D6FJly2fIVAK+GiHYpUz SBxDponailSHxpiYtzW6WDg7lO0cDMUCAI+R47W
- Ironport-hdrordr: A9a23:Ej9HTql47NyHy++vYbC/N65aiDzpDfI73DAbv31ZSRFFG/Fw9v rPoB1173XJYVoqNU3I+urgBEDjexzhHPdOiOF7AV7IZmfbUR6TXeRfBPzZslnd8kPFmtK1rZ 0QEZSWX+eAbmRHsQ==
- Ironport-phdr: A9a23:2lY3Chy5SGo2ZIzXCzLJwFBlVkEcU1XcAAcZ59Idhq5Udez7ptK+Z haZvqwm1QaVFcWDsrQY0bOQ6/ihEUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7F skRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCSjbb9oI hi6sArdutQLjYZtN609zgfFrmZSd+lZ229kOEifkwrg6su14ZVu7zlet/U9+sBaTK70Zb44T btWDDQnN2A6+sjmvgTdQAWM+3URTHwYngJHDAbZ4h76WIzxsjbhuepmxCaaJ8z2QqsqVjmk8 qxmVQXniCYDNz4+7WHXlsl9h79VrR69uxByxZPfbYeIP/R8Y6zdZ8sXS2RBUMhPVCJPH4yzY JcOD+QGIeZVtJPyq0cSohakHwSgGOHixzlVjXH2x6061OEhHBna0QwmAt0OqmrbrdvoP6oOS eC11LfHzTHeZP5Rwzj98JDIfQ4lofyXRbJwa8vRyU8zGAzbklWQrorlMymL2esQrmiW9uxtX v+ghGA7sQ9+uCSvxtsyhYnTgIIY0lTJ+ypnzYorJdC1S1J2bNqkHpZTtCyXNI97T8EgTm9mu Ss3yL4LtJGmcSUI1JkpyBHSZ+KJfoWM/x7uVPidLSp+iXl4dry/gBOy/lKhyu36TsS031dKr jZFktnRrX8BzQDc6s+CSvdl5EihwzmO1wHN6u1eJkA0j6XbJpg8ybAzjpoeqVnPEjH1lUnsk aOaa1so9vK15+npY7jqvJ+ROo9shgz/MakigNKzDfg4PwQUQmSW9+Sx2Kf+8UD4WLlGk+M6n 6rDvJzHOMgXuLS1DxJb34si8RqyDzWr3dIFlncdNl1FYgiIj43xNlHOPv/4CfC/jkyykDdqw PDGOqPuAonTIXnDjrjhZqxx5FJHyAYp1dBf/ZNUCrcdL/3tRk/xs9rYAgUnPAOp3ubrENR91 oUAVmKTGqKVLb3evFyS6u4yPuWAepUZtCvzJvUk/fLjjX80lUcYfaaz3JsXbH64Hu5hI0Wce XfjmM8BEX8UsQo6V+HllEaCXSRLZ3aoXqI84C00B5y6DYfEQIChmqKO0zqmHpFOfGBJFkiME Wv0d4WDQ/oDdCWSItZ4njMYUbihVpQu2Aq1tA76zrpnNvDb9jcZtZLlzth15vfcmQs89TxuX Iyh1DSGSHgxlWcVTXdi16dm5Ed5112r0K5igvUeG8YFtN1TVQJvHJjQ1eFlQ/nqQg/FNoOAU E6rRv2+GzA3Rd8txNlIbkpgTYbxxivf1janVudG34eAA4Y5p/q0NxnZIs98zy2Dz6w9lxw9R dMJM2S6h6l5/gyVBojTkkzfmbz5Pb8E0nvr82GOhXGLoFkeSBR5BKzdRX0bTlPMrNLy61/FS fmjBal0ehBZx5u6I7BRIsbskU0AQf7iPNrEZGfkkn+oCBKgzajKdJDrfW4QwCLbTkUIjlNb5 m6IYDA3HTzpuGfCFHpuGFboNlvr6vV7oWinQ1Uc0QCNa0B92qu44VgenrqEUfIV1b8YvyFnp jlpdLqk9/TRDdfI5w9ofaEHJMg4/E8CzmXB8Qp0Ip2nKalmwF8YaQV++U30hV1xDc1bnM4mo WlPrkI6IL+E0F5HazKT3IzhcrzRJG7o+RmzaqnQkljA2deS860L5bw2sVLm9A2uE0Mj9T1g3 bw3mzOV/o3HCCIKS5P3WUsr8B48qr3HI2E8647SyXxwIPysqDaRk9ktBeYj1lOhZ4IGavPCT VaoVZRBWY7zdb9P+RDhdB8PMeFM+bRhOsqnc6DDw6u3JKN7myrgi21b4Yd720bK9ixmS+eO0 YxWppPQlgaBSTr4i0+s987tnoURLzgKBme74SP/QpZLZ6t5cJoMDyGjL9D9lbAcz9b9HmVV8 lKuHQZM0dexdB66d0b82wZdyUMR53GrhGHrhywxmDYvoK2F2SXIyOm3bxsLNFlAQ2x6hEvtK 4y55zwDdHChdBNh1B6s5EKhgrNeuLw6NG7LB0FBYynxKWhmFKq2rLuLJcBVutsktiBeUeL0Z l7/KPa1qgMC3ifLFHAY3Co6cTqnppL/2RF2lSqRIW1yo3zQZcxrjU6FtJqFHKQXh2FYAnQlw TDMTkCxJdyo4cmZm/Kh+qilWmStW4cSOSjnwIWctTeqsGhjABmxhfe2yZXsFQk31zO+1sE/D H+Y6k+lOM+yjPr8bL80GysgTEXx4Md7BIxkx445hZVLnGMfmo3Q5n0f12H6LdRc36v6KnsLX z8ChdDPs22HkAVuKGyEw4XhWzCT2MxkMpOzensb3go29IZSEqaS57FYmi0zr1al51G0A7A1j nIGxP0i5WRPyegRoAcp5i6GRKgIHE9TMDDrkVKF4830/8A1LC6/NLO30kR5h9WoCrqP9xpdV HjOcZAnBSZs7897PQGEwDjp54rjYtWVccMLu0jejULbl+YMYsFU9LJClW99NGn6p3Fg1+Mrk Ukkw8ShpIbeY2B9tKOhXkwBbG2zPppJvGi20+AG2ZzNuuLnVpRnETEWUJa6VeipFjkfqfPhc QuCDXUqo3OfU9IzBCen4Vx95zLKGpGvbDSMIWUBiM5lXF+bLVBehwYdWHM7mIQ4H0ak3p6pf EB87zEXrln2z3kEgvpvLAX6W3zDqR2AdDYzTJWDIQtb9UdJ/AHNK82Y5e9vGCce85G85ACAM W2UYQ1UAHpsOATMXgqzeOD3v5+ZqLbeW7f2JuCGebiUrO1CS/qEjYmi1Idr5XfEN8mCOGVjE +xu2kdHWiMceYyRkDEORioL0iPVOpfB9FHlo3cx95vhtqm2C2eNrcOVBrBfMMti4UWziKaHb KuLgTphbC1fztUKzGPJz74W2BgTjTtvfn+jC+dl12aFQaTOl6tQFxNeZTl0MZ4C5rok0w1lM tWdksn00LV1kvkzTVpJSBay/6PhLdxPOGy7OF7dUQyTM6+aIDTQ38ztSb29TrldkOhFugb2s i3dC1XiOD+Oiz7vER2jLKsf6UPTdAwbs4a7fBF3DGHlR9+zcRy3Puh8ijguyKE1jHfHZiYMd CJxeERXoviM/DtV179hTndZ4CMvfozm026JqvPVIZEMvb53DzRowqhEtW8ixeId5WkBTfhx0 kM6QfZluBe+iOiJwTd7VxwIpzpW1tvjVaBKIb/Y8JJNRXHCuh8B8DfIY/zrj8VkDdnip61Bx 8OJn7m1MC1D9dnZ4cwaQcXYNZDeWEc=
- Ironport-sdr: 4qZUR00rjANid29ob19R5O3ZfvGFSknY51YXmhC8lnjW1gUhD38Pwn0MYXqVIZTcSFOTOaqJUA JCUtW6MoG9zLRp5hJF8VnfzrzubbIqqhwl43uk+CWc+iOIQ65WbUyTKBjQKaXpzC4xG7SoJF0l lDG1282R1HNDI5cIBFC7T/eMQVmGGAAzU9zEW+7bX/EZ3tFs3z3YCW+6Q+BmIj4L7/q3+R/fBJ Enh1rz6Bay2fCX+OncszaAYVbWd7Qbf5Wg9ZmE327AmzlKaug9sXF2nwYK+AhciKR36HkvMJLk Jj+WomPXveWx4tCa5ibgPTId
I am happy to announce the release of VST 2.9, the Verified Software Toolchain.
There are not many changes since VST release 2.8 in June 2021; the major changes are:
- Compatible with Coq 8.13, 8.14, 8.15 and with CompCert 3.10.
- Substantial efficiency improvements expected through use of Canonical PTrees data structure (see https://arxiv.org/abs/2110.05063 )
- Improve an error message when gvars is missing in a forward_call (#524)
- Correct the definition of pointer_val_val in 64-bit mode
- Some of the concurrency libraries now available in 64-bit mode
- Fixed issue #503 (confusion over multiple compspecs)
-- Andrew Appel
- [Coq-Club] VST release 2.9, Andrew Appel, 01/27/2022
Archive powered by MHonArc 2.6.19+.