Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Coq Platform 2022.01.0

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Coq Platform 2022.01.0


Chronological Thread 
  • From: Théo Zimmermann <theo AT irif.fr>
  • To: Coq Club <coq-club AT inria.fr>, coq+announcements AT discoursemail.com
  • Subject: [Coq-Club] Coq Platform 2022.01.0
  • Date: Thu, 27 Jan 2022 20:16:47 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=theo AT irif.fr; spf=Pass smtp.mailfrom=theo AT irif.fr; spf=None smtp.helo=postmaster AT korolev.univ-paris7.fr
  • Ironport-data: A9a23:cbrZNanatRMKG+EfLrtbp4ro5gy+IERdPkR7XQ2eYbSJt1+Wr1Gzt xIdUT2FafyJNmL9eNtwa4i//UICv5fdmoVkTgM/qHpgEVtH+JHPbTi7BhepbnnKdqUvb2o+s p5AMoGYRCwQZiWBzvt4GuG59RGQ7YnRGvykTres1hlZHWeIcg944f5Ys7N/0t4AbeSRWVvX4 4ur+ZKHYjdJ5hYtWo4qw/LbwP9QlK+q0N8olgRWiSdj4TcyP1FMZH4uDfnZw0nQGuG4LcbmL wr394xVy0uCl/sb5nxJpZ6gGqECaua60QFjERO6UYD66vRJjnRaPqrWqJPwZG8P4whlkeydx /1nqaCxCiEDDpHW28QsEFp9CCRlZ71/reqvzXiX6aR/zmXFdGHrx/hwSlwwPJNd4u9tAHoRs /ICQNwPRknS26Tsne79FLAq359zRCXoFNt3VnVI0THUCt4nW5HNBavQjTNd9Gtq1p0WTKe2i 8wxMyooVAXKSTl2M3A8NrgVweSj30P2fGgNwL6SjfNrsjmMnFMZPKLWGNHSY5mBQdhftl2Jo 3rPuWX/GBATctKFoQdp6VqvgfXImS7lHp8UFaP97vdwgUbMgGIJYPELabelidOltk/9ffhvF 1ZX2htt7o0p8VfxXuCoCnVUv0W4lhIbXtNRFcgz5weM1rfY7m6l6o4sEmYphDsO6JReeNA66 rOat4+5VWc16tV5XVrHqu/L8FteLABPdTdqWMMScecSy/fZyG3ZpirGVNd4eEJepoKoQWirq 9xmhIPYg7hWgcNO+b+y+1vK6w9AR6QlrCZrum07vUr8vmuVgbJJgaTzuDA3Ct4cdu6koqGp5 iRspiRnxLlm4WuxvCKMWv4RO7qi+uyINjbR6XY2QcV6rW78qyfzJNEBiN2bGKuPGptVEdMOS BGI0T69GLcIZSLCgVJfPtrtWpR3k8AM6/y8DamOMrKinaSdhCfeoHA/Oh7Pt4wcuFIhl6gjN I3zTCpfJShyNEiT9xLvH711+eZzmEgWnDqDLbimkUjP+efANRa9FOdUWHPTP7tRxP7V8G39r YwCX/ZmPj0EDYUSlAGMrdVMRb3LRFBnba3LRzt/L77afVE+STh/Upc8A9oJIuRYokicrc+Ql lnVZ6OS4AOXaaTvJVrYZ3Z9RqnoWJoj/3s3MTZzb1ey2nZlb5z2tPUTcJ4+fL8G8u1/zKcoF KBYIZXcW6VCGmbd5jAQTZjht4g+Jh6lsgSDYni+az8lcp88GgHEo4e2fgbm+CQUIDCwsM8y/ ++p2g/BHsgCXQVsSsjMMar9w1S0tHkbueRzQ0qRfoIKJR+8rNE7JnWo3PEtIswKJRHS/Reg1 l6bUUUCuO3Ag44p692V16qKmIGkTrllFU1AEmiHsLu7OHWI/menxoMcAu+EcSqHDjH3/7+lY ehLiez6MeNChF9QspEjVbhxlPps69zqrr5c7wJlAHSSNw3xWu07fCHe0JkdrLBJy59YpRCyB BCF9O5aDqrVasnrJ1gceVg+ZeOZ2PBJxDSLtaYpIF/37TNc9aacVRkAJAGFjSFQcOlvPIU+z btzscIa8Vbl2BktKNGCgz4S6mKNMDkYWr8mrc5cDpWy0lgnzVRLYJr9DC7q4cjXMo8cbBJ0e meZ1PjYmrBR5kveaH5tR3LD6upqmshcsh59ylJfdU+CncDIh6Jp0UQJoyg3VAlc0j5Oz/l3Z jpwL0RwKKiDl9uyaBOvg4x498B96BylFojZyFwTk2nUUQ+1UG3TaXU0I+eWowYX6Qqwu9SdE K6wkA7YvfTCJakdHRfenWZksf3tC9JrnuEHsN7yBNyLRvHWfhK86pJDpgM0R9/PANkwigvJv 4GGOQq2hbLTbUYtnkHwN2VWOXn8hvxJyKyujMyNJJ80IFw=
  • Ironport-hdrordr: A9a23:pvNwW6jyS5l9HhlSzWcaSuirMXBQXlsji2hC6mlwRA09TyX4rb HUoB11726RtN98YgBEpTniAtjjfZq/z+8S3WB5B97LN2OL1wWVxepZnPLfKlPbalXDHy1mtJ tIQuxRDNXxCBxdlsb14A6xFpIFzMOc+K6lwcfypk0dKj2Cp5sB0+/3ZzzraHFedU1jBZ8lGI GR66N81kedkL0sH6eG76Y+MtTrlpnJ0JjmYxoPBxtixA6QgTav8af3eiLoois2YndNhb0i82 zMkwm83K+kqP3T8G6i60bjq5cTktriztNCAYi3l8AJNi+EsHfXWLhc
  • Ironport-phdr: A9a23:GoKdBRIhpFcpIFnfGNmcuI5tWUAX0o4c3iYr45Yqw4hDbr6kt8y7e hCFv7M21RSQBNmTq6odzbaM6ua4AS1IyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxB sVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexf61+I A+4oAnMucUanJZuJ6kswRfNvndEZv5ayGx2KV6OhRrw+tu88Jt++ClMpvwt8NJNX7/ndKoiV 7xYCzomM2Ex5ML1sBTIUBWC6HgBXGgIixREGwfK4g30UZf3qSv6q/Fy2DKGMs3sTLA7Qiqt4 qF2QxL1kigHNjo58GbKisxsia9QvRysqwBjz4PSfYqYL+R1cL/DctwGRGpBRsdRWDJHAoOgd IsEEu4NMf9Fo4Xhu1cCqB2zDhSuCuzy0D9FnnD506003eoiDA/IwhAvEskSsHjIttj5KLseX fy3waTO0D7Nb+lW2TD46IXQbB4hoeuLXbVofsXSyEkvEgbFgUuKqYzgJTyV0OINuHWc4up8V eKglWknphpwoji1x8cshJPFhowPyl3d8yhy3Yk6K8GiRkFhfd6kDIVftzucN4ZuX88sQ2Vlt Sg+x7AFuZO2fygExIgoyhDQZfGKb4mF7x39WeuPPzt1hX1rda+9ihuv8Uauyu/xW8ip3FtOs CZLnN/BvW0D2RzU78iIUPp9/kG51DaA1gDT9uFEIV0vmqbBN5Ehxbswm5wOukrABi/7gFj6g auZe0k+5OSl6+vqbq/nq5OBLYN4lw/zP6c2lsChHeg1NhICUmub9OimybHu/FH1TK9XgvA0j qXUto3RK94Bqa6jGQBV154u6xahADei19QVhXoHLFVfeBKAi4jmJU/OLOrlDfe5glSsji5nx +jcMb37A5XNNXrOnK3vfbZn80JcyQwzws5D559MF70MJP3+VlXvuNHYARI1KQ25z/v9BNlg2 I4TWnqDAqqDP6PTtV+I6PgvI+6JZIINpDb9K+Yq5/n1gH84g18dfKep0YEZaHCiBvhmOVmWY WLwgtcdFmcHphYxTOvziFGbTTFTY2uyULkn6zEgCIOmCJ/DSZq3jLyA2ie7BJxWaXpcBlCCC 3e7P7mDDtwLcWq5JtJr2mgPUqHkQIs83zmvshX7wvxpNLyQsiYfrNHq0t5y+uvYmBQ/8yBvJ 8icyGqKUntvk2YBRjtw16d68mJnzVLW7aj5hMtqFNlW6ulMWwE8fcrAz+F9I9HoWwyHcM3fG wXuecmvHTxkFoF5+NQJeUsoXoz61ngrvgKvCr4RzPmQAYAst7nbxz73Ltp8zHDP0O8giUMnS 41BLz7unbZxoi7UAYOBiECFj+Cyb61JwC7A80+C12uA+k9CA0ZrSauQZXkEfQPNqMjhoEbLT rugE7MiZxdBxMmqK7FLZJvnlwYOX+/tbfLZZW/5gGKsHVCIy7eLOZLtYHkY1T7BBVIskAcJ+ nKLK04jACa/5nrXFj11ShTheSsA6MFYr3W2Bg8xxgCONAh60qatvwUSnbqaQu8S2bQNvGEgr S91FRCzxYCeDd3IvAdncKhGBLF1qF5ayWLUsRB8NZ28PuhjgFAZaQF+o0Lp0V1+FIxBlcEgq H5iwhB1LOqU11ZIdjXQ2p6VWPWfNmn/+ziuca/YnF/EkZ6X9qoJ9PUkugD7pgj6XkEm8nhhz 5xUyy7Ft8mMVldOF8yoFB9sp0sfxfmSeCQ26oLK2Gc5NKC1tmSHwNc1HK4+zQ7med5DMaSCH Qu0EssABsHoJvZ5/jrhJh8CIu1W87Y5es28cP7TkrKrMeFInSingyJJ+soumlLJ7Cd6RuPSi twZw/yf9gqdVjm6gk3r4aWV0chUIDoVGGS40y3tAoVcM7ZzcYg8AmCrO8Srx996ivYBQlZg/ UW4TxMD0c6tIl+JakDlmBZXzQIRqGCmni2xy3p1lSsop+yRxn6Gz+PnfRsBcmlFIQsqxUvsL I+cjsobUg6mdUAlmQCk6kDz26VA7P0ucy+JHBsOIXGwdjoyGqKr/qKPectO9I8lvW1MXeKwb ErbL9y16xoW3iX/HndPkTUydjWkoJL8zFRxjGOQKmo2rWKMIJAsg02CuJqCHLgIhWpVIUsww SPaDVW9IdSzqNCdlpOY9/u7S3rkTZpLNy/i0YKHsiK/o2xsGxy22f6pybiFWUA31zH2095yW GDGthH5N8P316m9GeN9f0cuCkW2uIJqX5pzlIc9nsRaxXgXgb2U53sJ12npe4Y+u+q2fD8GQ jgFxMTQ6Q7u1Rh4L36H8In+U22U3sprY9TpKnNTwC826NpGTbuF9LER1zUguUK29EiCBJo11 idY0/Yl72QWxv0EqBZ4hDvIGagcRAFdLWS7nhCMpbhStY1xY2CiOfi13Ut6xpW6Ca2a5xpbQ DD/c4sjGil56oN+NkjN2Tv98NOsft6Ydt8VuhCO9nWIx+FINJI8kOYLjit7KCr8u3Mi0esyk R1p29mzooGGL2xn+K/xDARfM3X5YMYa+zeliqg7/I7ex4e0ApBoASkGRrPrSuivFD8M8+nhN hjLCDQmq2zEX7TFXEee5Epgs3PTAsWrOnWQdxx7hZ1pQBiQIlAagRhBBWRm2MRkSkb0nYq4K xcqg1JZrkT1oRZN1O9yYhz2U2OE4Rytdi9xU5+Hahxf8gBF4U7Rd82Y9ON6WS9CrfjD5ESAL HKWYwNQACQHQEuBUhr/PrSpzdja8ubeCPD0fJ6sKf2e7PdTUfuF38flyox94zOFLdmCJFFhC Oc83kddG21/GtqcgzwVSjdI0SzXJZ3+xl/06mh8qcax9+7uUQTk6N6UCrdcBt5o/gi/naaJM +P4bMlRKCxZ2NUC3y2RoFD69F8Iii8oeSP/SdzoVAbOS7jXnqJJSQMdaj02LMJS7rljmAdXa 5aztw==
  • Ironport-sdr: uOJRXCt40N9FF4AqzAWuKIGj29/ya2umZnglS2dF4zYkSSDQ0fRlV9MhfUAq7Bggt9Rcw5/bxx ebmPmb9NKy8HHM4g3mYgcCAvKrOhDVV1JJnhcIAJ8L0GZAFC2uVoZcGrwb3tKiMJhKwiSj9Tat 0cVuV5q7QDOHaduzoFUSJx7EG+Zrh4CPgc5RKobEbJ/c2NbT3KSmdrBzQNHvww8J2+hZH3Xm1U svapQSoXGHizmwvIiTRADimMDnvLrZogvVM1XTR3jwMO7MDBHmkDW5SRnpEw/arkVzOFKImfc3 bT9n/D7z7GnmA7BdYVt4vUmw

Dear Coq community,

On behalf of the Coq development team, the release managers of
Coq 8.14 and Coq 8.15, and the Coq Platform team, we are happy to
announce the immediate availability of the Coq Platform version
2022.01.0.

Release highlights:

- An important newly added package, coq-hammer, provides the hammer
tactic, which uses external ATPs (Automated Theorem Provers) to
automatically create Coq proofs. Besides the plugin, Coq Platform
provides two automatically installed ATPs: E-Prover and Z3-TPTP.

- Another interesting new package, coq-coqprime-generator, provides
the executables pocklington, o2v and firstprimes which automatically
generate Coq proofs for the primality of (largish) prime numbers.

The main supported version is:

- Coq 8.14.1 with an extended and upgraded package collection.

Several compatibility versions with Coq 8.13.2 and 8.12.2 are
available. Furthermore, we provide the following preview version:

- Coq 8.15.0 with a preliminary (beta) package collection.

You may install the Coq Platform using opam-based scripts, or Windows,
macOS and Snap binary installers.

To learn about the Coq Platform and get access to the
installers, please refer to:

https://github.com/coq/platform/releases/tag/2022.01.0

(The Snap installer is still in preparation and should be available in
a few days.)


  • [Coq-Club] Coq Platform 2022.01.0, Théo Zimmermann, 01/27/2022

Archive powered by MHonArc 2.6.19+.

Top of Page