coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Andrew W. Appel" <appel AT Princeton.EDU>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: [Coq-Club] VST 2.14 announcement
- Date: Tue, 16 Apr 2024 17:08:16 +0000
- Accept-language: en-US
- Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=princeton.edu; dmarc=pass action=none header.from=princeton.edu; dkim=pass header.d=princeton.edu; arc=none
- Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; 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=CKoY0od59sL4rVRujdsS5Cc+dAPKzK/rjWLo4tKBmqQ=; b=HNeZf4RYn19PfxMGl7AVVpwHcakt9YH3bDymhV8WFSi+cvGdAB5v0YEIyx9Et4+f1LauT5ntGkueVCaW/jgdzE+8/dCUlJ+xoFT43cufxXpoMFd8xbr2+bezFzAXf3jroGHgz3YmUbXfusVdYwn1NcwfJg/VMF88YQOI2wsGDIkWYRSlDMPXGEhj6qv02mOTp2eg6f6ZGOqSulSGx4VkhWb8NeNPbxDpzH7Zqcr8ZBw+3G9J7Q4eO3i6LcgLJmACzOaXgkkdbyUMNsPlUDCylRt0dLc3Cr9GAPeMRQacnC/KywmcR+dXDcMmFMuRCyvme64h8aCoIm1uxDy6B/j5hQ==
- Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=AjEvjCa6lD5l/UFKWomrzlXBPmtqabTTnFDLXEK7c4QAFWbiqJ0RS4ttFTKbDQU7P3tVJiVAPQG0BMrdiv2/JofaQwMZHQcY/Sx+C2+VLjCx+ZqHYLtLgKgv86c4Pw46hkWeCYtkDrvAZS6O0mCoq8BtQOVSxE5wZ2TUUzIRs8DBQ59dfuK6CHPCS/BP5ol8uWmzFFhUW3p4u6Ygqha7SR6UYQ3OaeYrfsaIF57/ejDjRauSnaJ2WczU7CCW69sOnDnCOToq/E9l2iR5zR5o8d/I6SOgeN1w9DuH8poEYaLL0+d3S+OwTyhVMWgbr5W4yx+x6b5kFH480BrTzCiU6Q==
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=appel AT Princeton.EDU; spf=Pass smtp.mailfrom=appel AT princeton.edu; spf=Pass smtp.helo=postmaster AT NAM12-BN8-obe.outbound.protection.outlook.com
- Ironport-data: A9a23:zDWtUakv08Sjqy4M9uR05hLo5gyNLURdPkR7XQ2eYbSJt1+Wr1Gzt xIaDG6DOK3bN2CgKNl0PIni9E1XuJXcmodhQAFsrShnHltH+JHPbTi7BhepbnnKdqUvb2o+s p5AMoGYRCwQZiWBzvt4GuG59RGQ7YnRGvymTrSs1hlZHWdMUD0mhQ9oh9k3i4tphcnRKw6Ws LsemeWGULOe82Ayaj18B56r8ks14Kyu4W1A5DTSWNgS1LPgvylNZH4gDfrpR5fIatE8NvK3Q e/F0Ia48gvxl/v6Io7Nfh7TKyXmc5aKVeS8oiI+t5uK3nCukhcPPpMTb5LwX6v4ZwKhxLidw P0V3XC5pJxA0qfkwIzxWDEAe81y0DEvFBYq7hFTvOTKp3AqfUcAzN01EB5nfogCxd1LCEFX/ OU9LGwVMzWq0rfeLLKTEoGAh+wFBeyyZsY1nCElyjvUS/E7XZrEXqPGo8dC2ys9jdxPGvCYY NcFbT1ob1LLZBgn1lU/VMp4xb/3wCOkLHsB8An9SakfuwA/yCR4yKDgNPLNYN2MTshJmUDeq 27bl4j8KkFGZYzGkWXYmp6qrvDkgim4fIs7KJ+l9tVSvXiN5FAvLyRDADNXptHi0RTiBLqzM Xc88S036KM26UaDVcj4RxT+oXievxdaVcA4LgEhwASEy66R6QDJAGEBF2RGboZ/7JRwQiE23 FiUmd+vHSZorLCeVXOa8PGTsC+2Pi8Wa2QFYEfoUDfp/fG4vN5izRfVce1fGY6sh8TQHW3on hWj+X1Wa6ooseYH0KCy/Fbiij2qp4TUQgNd2ukxdjP9hu+eTN70D7FE+WTmAeB8wJF1p2RtU VABksmaqeoIXZeEkXXXR+NXRenyofGYLDfbnFhjWYE78Cig8GKieoYW5yxiIEBuMYAPfjqBj K7vVeF5tMc70JiCNPUfj2eN5yICkPOI+TPNC6y8Uza2SsItHDJrBQk3DaJq40jjkVI3jYY0M oqBfMCnAB4yUPs+l2DuGrZMje96nUjSIF8/o7iql3xLNpLPPBaopUstbAHTNYjVEYvY/lqJq IYHZ6NmNT0GCrChMni/HXEvwaAidiNhWc+eRz1/c++IOA19H289Q/TW26tJRmCWt/U9qws8x VnkAhUw4AOn2xXvcFzWAlg9M+iHdcgk8hoG0dkEZgrAN44LOtv3sM/ytvIfIdEayQCU5a8lH 6FeIZ7aW5yiiF3volwgUHU0l6Q6HDzDuO5EF3PNjOEXJsY6GV766ZX/cxHx9SIDKCOyuIFs6 /ejzw7XC95LDQhrEM+cOrrlwkKTrEotvrt4f3LJBd1PJ2Tq0oxhcBLqgtENfsojFBTkxxmh7 TiwPys2n+f2jrUOwIH7vpzc94aNOMliL3VeBFjevOqXNzGF32+Nwr1gceevfBLkX2bw5ZT4W 71fla3hCsA9ondLrItOPLJ5xo0u59bUhuF7zyY1OF7pfliUGrdbDX3e5vZ2t4pJ3a5/uyG6f mmt6+tqE+yFF+29GWFAOTd/SPqI0M8lvwX77NM3ER3c3zB29r/WandiFUCApwIFJYQkLb5/5 /kqvfMXzAmNihAKFNKipQIM/kSuKk0waYkWhqs4MqTK1DVykkpjZKbCABDY+JuMMtVAEnc7K w+u2Zbtue5u+VrgQVESS172wutvtbYfsktrzXgDBWiztPjru/sV5CBVoBMLFll77xMfyO9iG HlZB2ssL4W0wjpYrsxiXWetJgJ/OCOk6nHBk2UuqmmIYHSrB0rsLXI8M9mj5Eo20XxRVRkF8 aC6yFTKayfLfsbw1QsQQURgjfjvYo1s0gj8m8ycPt+kGqMiamHPmZ6eZmsvqjrmD/guhUbBm /JYweZoZYD/Ng8Su6ceCbiF5Y8PSRuBGnNOccth8IwNA2vYXjO4ghqKFGycZeJPIKbs3XKjK skzOP9KaQuy5ByOoh8fG6QIBb1+x9wtxdgaf4LUNXw0iKSeohVpoaDv2HDH3kFzeOpXkOE5N o/1XBCBGDbJhXJrxkn8nPMdMW+8OdQ5dAnw2d6uy9owFrUBjfpNdH8j2b7lrlSXNwpapyivh j3hXJOP7eJeytVLpbDOQ4FjHAS/LO3hWNuYqD6Tt8t8VvKREMPsmT5MlHzZEVV3B4YBY/V2i rWHj/Dv1mznorsdcj7UiruBJYZz9OSwW+trMezRCUV7gRKBBJPI3EoCyVvlN5B5qtJXvfe6d SDld8C1JIYnZPEFzUIEdgxbQk8RJLTpZP37uBLn/uitCwcc4yPDPtiI5X/kVkAFVy4qarnVK B74hOaq3f9c9L9zPR4jA+p0JrNFO3rhZPcCW/yqkgKHH06EpF+mkZnzpyoKsD3kJCGNL5fn3 MjjWBP7SiWXhIjJ69N86KlZoRwdCSdGs9kaJ04y1YZ/tGGnMTQgM+8YDJQhD6NUmAzU0LXTR mnETEkmOBXHcQV0SzfOy/W9YV7HHc0LAMnzGRIx9UDNayuWOpKJMIE8ygheuUVJahnR58D5D +oB+0/AHAm7mbBoYucx2saVo8lawtHi+3ZZ3nylzuLTBU8SD4xfgTYlVEBIWDfcGs7AqFTTK CJnDSpYSUW8UgjqHdwmZ3dRHwoDsSjyyykzKx2C28vbp57R2dgoJCcT4A0v+uZrgAU2yL8yq bffYUKoujrT8FpD/KwjtpQunLN+Du+NEo6iNqj/SAYOnqa2rGM6I8cFmilJR8YnkOKaO02Ij SGiuhDSG2zcQH29GpXPoenKx361emoWDjfCgRL4o3nLnQFRIx3xZU2x1AyiQX3vg/GLgqibK Qv+qG6puVyQvzb4oj84m9gmzrBC7Qf9ClGcOh0VoljOfttAhYOT+H2NE6336j6JzEB5+w==
- Ironport-hdrordr: A9a23:3fmCH65NVvFVIlCEdQPXwS+BI+orL9Y04lQ7vn2ZFiY5TiXIra qTdaogviMc0AxhPk3I6urwQZVoIEmsgqKdhLN8AV7MZniDhILFFuBfBOjZskvd8k/Fh4lgPM 5bGsAQZuEYZmIK7voSlTPIdurIt+P3kpxA692/815dCSVRL41w5QZwDQiWVmdsQhNdOJY/HJ 2AouJaujuJYx0sH4yGL0hAe9KGi8zAlZrgbxJDLQUg8hOygTSh76O/OwSE3y0ZTyhEzd4ZgC P4ek3Cl++eWsOAu1PhPlzonttrcRzau5V+7fm3+4Uow/PX+0eVjcpaKv2/VXsO0ZmSAR4R4a LxSlEbTo1OAjrqDxuIiAqo1A/63Dk07Xj+jVeenHv4uMT8ACk3EsxbmOtiA2nkAmcbzaFBOZ hwrhGknosSCQmFkDX25tDOWR0vnk2ooWA6mepWi3BES4MRZLJYsIRapSpuYeM9NTO/7JpiHP hlDcna6voTeVSGb2rBtm0qxNC3RHw8EhqPX0BHsM2I1Dpdmmx/0iIjtbkit2ZF8Ih4R4hP5u zCPKgtnLZSTtUOZaY4H+sFSdvfMB29ffsNChPtHb3KLtB5B5uWke+L3Fwc3pDXRKA1
- Ironport-phdr: A9a23:uKRBhRW4FKd2Nux6lfQNRCpzKqTV8Kw/XDF92vMcY1JmTK2v8tzYM VDF4r011RmVB9Sdsq0awLaI+4nbGkU+or+580o+OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF 95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba12I RmssAnctMgbjYRtJ6sw1xDEvmZGd+NKyGxnIl6egwzy6sCs8pB97i9eoegh98lOUaX7e6Q3U 7lVByk4Pm42+cPmqwDNQROA6XUAXGoWlAFIAxXe4xHhQpjxqCr6ufFj1yScIMb7UKo7WTWm7 6dsVR/olCIKPCM3/W3LlsB9ir9QrRS8rBJ93oHUepmYOvpgcK3AYdMUS2lPUdpeWCFaGIywc 44PAvAdMepEsYXwoUYFoxukBQmrAePi0jFEi2Pw3aInyeQuDw/H1xEgEN4UrX/ZsM31NL8MX uCxwqXD0DLOYOlO2Tfl9ofIdgssr+uWXbJxd8re1VcgFx/CjlWWs4DrMD2b2eoUvmWd8uFvW v6hhXQ9pAFtvjig2N0sio/Ri48XxV7J8Sd0zYcpKNCmSkN2f9CpHZtRuiybOIZ4Td0vTmBst Ss6xLMLup+2cDUExpk6xhPSa/2KfYaH7x/gSuucJypzinxieLK6nRmy8E6gx/XzVsm1zFZKr jdFncLWun8R0BzT79CLSvR8/ke92TaPyhvc5vteLU8okqrbLpgsyaMzmJoLqUnOETP6lF/rg KOKdEgo4Pak5urlb7n8u5OQK4F5hhngPqkvhsCyD+E1PhUSU2eA+Omx0b3u8EjkTLVEi/A7l 7fVvIzcKM8GuKO5BxJV0p0/6xmhFTeozdUYnHgZI19dZB6KiZXiNUvUL/DiF/i/hkyhkDd1y PDCOb3sGo3DI2TEnrv8Y7px8lNRxhIwwNxG4JJbEa8OLOj0Wk/sqNzXFRg5MxGyw+n6Etl9z pkeWWWTAqCHLKzSrV6I5uUpI+WWY48VpSr9K/wi5/7pjn81g0MSfa6s3ZcPaXC4GOppI1mBb HfjntsNC3oGshY8QeDwllGPXzxea2yvU64g6Dw3EIemAp3CRoCpjryBxiC7HphOa29cElCMC Wnnd4GfVvcUciKSI8lhnSAaWri9TI8h0wuiuxHnxLp6NubU/DYXuor51Ndp/+3TiQ0y9TtsA siAy22NVX17nnsURz8q26ByuVByylCa0aRhn/NYEcFT6OhSXwchNZ/cyvR6BMroVgLAeNeJU lemTc+8DTE/VNJii+MJNgx2HMznhRTe1QKrBaUUnvqFHtZ8pqnbxj36I9t343fAzqgoyVc8F JhhL2qj0+RW8QTJCpGBrAPRvr6yeKBWlHrE7H+OyUK2pkBeWwNsVqODcFwiMBiF5e/l71/PG uf9QY8sNRFMnJbqwspib9ToiQ4DX/L/IJHFZHr3nW6sBBGOz7fKbYzwemxb0j+OQFMcnVU1+ nCLfRM7Gj/nu3jXWTV2DV/rS3v28O91pW+8SAkZ4zzZJ1Z52e+N8wUOzeeZV+tV27sFvCk7r DAhFU6l0tb+E8CBoQFsYKJaJ94x/QQPznrX4jR0JYfoNKV+nhgefgBw6lvpzAlyA55cnNICi loPlVA3A4TIlVRLenWfwIz6PaDRJi/q5hezZqXK21bYltGL5qMI7/d+oFLm1O2wPmwl9Xgvk 9xc0n/Ho47PEBJXSpXpFEA+6xl9objeJCg7/YLdk3N2Y+GytXfZ1tQlCfFAqF7odspDMK6CC A75EtELT8moJuswnlG1bxUCdOlM/a8wNsmierOIwqmudOpnmTuniyxA7uUfmgqF7zJxTsbwx ZcDyPyE2Q3BehvBzR+gvs3xhYFYdGQKBGPsgSPgBYNXeuhzZdNXUSH3e5LxnI4hwce1AC09l hbrHV4N1c63dADHalX82VYVzkELuTm8njP+yTVokjYvp67Z3SrUwu2kegBUXwwDDGRkk1roJ pC5yt4AW039JQExjBahzV7gxq5Qqbh4KS/eTVoCLE2UZylyF7C9sLaPeZsF4YswvCF/aP69Z 1uXVrn75TY27mmwV3sbzzc9eTawv5z/lBEvk2ORIkF4q3/BcN1xzxPSjDDFbcZYxSFOBCxxi D2MQ0O5I8Hs5tKM0ZHKruG5UWulEJxVayjii42a5mO34mhjABv3mP7W+JWvGBAi3CvTz8NrU y7FsBH6JITnyuy2PPlmcU9hGFLno5YiXNgmzc1q385WgCBBzpyOtWIKi2LyLclW1cecJDIWS DgHzsSUqAnp1Ut/L26YkofwV3GT2MxkNJGxZmIb3D547tgfVP/SteQb23Eu/Rzh9VmCBJo11 i0QwvYv9nMA1uQAuQ52iz6YHqhXBk5AeyrlixWP6dm66qRRfmemN7aqhy8c1ZisCq+PpgZEV TP3YJAnSGV59t1yNHrUynz14Yz4f9+WYN4O/E7x8V+In61OJZQ9m+BfzyN/IW/5lWU/yugwg ABp29e3sJXNeAAPtOqpRxVfMDPyfcYa/Drg2L1fksih1IeqBpx9Gz8PUcigXbeyHTkVr/iiK xeWHWh2tCKAAbSGV1z6ig8uvzfVHpusLX3SOHQJ0YAoWkyGPEIGyAEMAGdmxthgTl/snpe+N h4hvXhU71r84HOg08pQPgLkGifarQasMXIvTYSHaQFR9kdE7lvUNsqX6qRyGTtZ99uvtl7FJ muebgVORWYHPy7MT0jkJaWr7MLc/vKwIMObdqGLS5Pe7OtUWrGP2I6l1ZZg83CULMKTM3J+D vo9nE1eQXR+HMefkDIKLk5f3y7AdM+Uoh6g9zY/8pj5qay0Hli0us3WU+AaOM4n4x2shKafK +OczD10LzpVzNJExHPFzqQewE9HiyxqcGrIc/xIvirMQaTM365PWkJDLXora40StP16h1EWa qu5wpvv27V1j+A4EQJAXF3lwYSyYNASZnq6LBXBDVqKM7KPIXvKxdv2aOWyU+417q0cuhuut DKcC0KmMC6EkmyjXgi3POVklDuaOhdTpIa7NBthFCKwKbCuIg3+K9JxgTAslPcsgWjWMGcHL TVmW2Vki+TKqAl+0rB4EWEH6Wd5J+6ZnSrf9/PfNpsdrfpsBGJziv5e53M5jbBS6WsXIZ490 DuXpdlorVa8l+CJwTcySxtCpAFAg4eTtFljM6HUpdFQHGzJ9xUX4SCMGgwH8pF7X8b3tfkam b2t3OrjbS1P+NXO8Y4ACtjIfYiZZWE5P0OhGSaIXlddC2/xczmZ3wsEzbmT7iHH8sB888Cz3 sJIEvgCCjlXXrsbEhg3QYZEec8vGGtiyfnC0IYJ/Sbs9UGNApkF+MiBDrXLXr3uMGjL17AcP klRmOqqI9hLbt+pnBAyDzsy1IXSRRiKVIgU8HQ4N106/B0Woio5Ejx72lq7OFmkuCZBTKftz BBq0lAsMbx1rGW+pApuQziC7CoozhtrkI2802nIKWz/cP/rD4oOU3Km5Q9sa9v6W1gnNwTqx B49bW6WSe4J1OluLTgz2l2b5MEHXPdYSecsiPA43euWYf4lzVNa7Cir2B0ejQMkIb1LsVJwN LSK/zdH0Q8la8MpL6vNIqYP1kJXmq+Foi6v0KY23RMaIEEOtmiVfXxR0KTtHoE8Jiyj8/Br7 0qvtwYRIAAx
- Ironport-sdr: 661eb084_NmzJt6w0MY/u1WVoErG6EraI/waOQAiqKJE6s9+/WWfg1Lz 8ITywjYlh97j/vUgc3k0k20vU2mX76txN/iLG1g==
Announcement: Verified Software Toolchain 2.14
[but see also, coming very soon, the announcement about VST 3.0, which will be more interesting! ]
I am please to announce the release of VST 2.14, available in coq-released as coq-vst.2.14 and part of the forthcoming Coq Platform release. Compatible with Coq 8.17-8.19 and CompCert 3.13.1.
This release contains several minor improvements to proof automation, and some bug fixes.
CHANGES IN RELEASE 2.14 (March 2024)
- repr_inj handles int64 compares better
- Added nonempty_writable_glb lemma for user convenience (#734)
- Remove unnecessary premise in field_at_app lemma (#743)
- Improve error message in forward_if (#744)
- Fix slow unification in load/store forward tactics (#748)
- Generalize permission share in data_at_in_or_ptr_int lemma (etc.) (#749)
- Improve error messages from deadvars tactic (#751)
- Fix issue #745 (minor bug in entailer tactic)
- Localize/unlocalize more robust regarding unification vars (#756)
- Ensure veric.version is present in opam distributions
CHANGES IN RELEASE 2.13 (October 2023)
- Improved error diagnostics when compspecs mismatch
- Improved error diagnostics when change_compspecs fails
- Improved error diagnostics when VSU has missing (vacuous) funspec
- Int64.repr is Transparent, consistent with Int.repr
- forward tactic is slightly more careful about not simplifying user's terms
- bug fixes and improved diagnostic messages in list_solve tactic
- field_compatible0_Tarray_offset no longer requires naturally_aligned hypothesis
- 'forward' now interacts better with 'localize/unlocalize' (#756)
- Performance improvements in VSU system (#716)
- VSU permits sharing of globals between compilation units (#713)
- [Coq-Club] VST 2.14 announcement, Andrew W. Appel, 04/16/2024
Archive powered by MHonArc 2.6.19+.