coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adamc AT csail.mit.edu>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] FormalV 1.0.0 released
- Date: Mon, 11 Jul 2022 09:24:03 -0400
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=adamc AT csail.mit.edu; spf=Pass smtp.mailfrom=adamc AT csail.mit.edu; spf=None smtp.helo=postmaster AT outgoing-stata.csail.mit.edu
- Ironport-data: A9a23:y7Ncqas5UKrt8sFgyYm/C9RQHOfnVLJYMUV32f8akzHdYApBsoF/q tZmKWjTOviDNzP8co13Pom29UhUuZbTnYNjSQU9qyoxRigSgMeUXt7xwmXYb3rDdJWbJK5Ex 5xDMYeYdJhcolv0/ErF3m3J9CEkvU2wbuOgTraCYEidfCc8IMsboUsLd9UR38g527BVPyvX4 Ymo+5KGYQf8s9JJGjt8B5yr+EsHUMva42twUmwWPZina3eD/5W9JMt3yZCZdxMUcKEMdgKJb 7qrIIWCw4/s10xF5uVJPVrMWhZirrb6ZWBig5fNMkSoqkAqSicais7XOBeAAKtao23hojx/9 DlCncTuWwUsErLzpOsUFCUDERtcBohH/4aSdBBTseTLp6HHW3zx3/ppDUc5eJYE8/p+R2pV/ P0cbjUMclaOi//eLLCTE7M8wJ97apOtZtpH0p1j5Wmx4fIOSJzKRq7i7sRR3TN2g8FSW/vSe qL1bBIzMU2bMkIQaj/7DroCnf2HiCWkfgF8i2iV+6sv/mLC7QhYhe2F3N39I4HTHp49clyjj mnB5iHyBgwQHMeOzCKMtHOqnO7G2y3hML/+D5W/6+Jlh1yVySkIFBQKXB2wuvC4jgi7Ws4ZJ kAJksYzkUQs3BT1XNv4cwKHnHGN+SJHWeByKMg77zjYn8I4/D2lLmQDSzdAbvkvu8k3WSEm2 ze1czXBWWwHXFq9FSz1y1uEkd+hEXRPdjFeNUfoWSNAvIC78dFs5v7aZosLLUKjsjHi9dgcK RihpS00nbQfgsNjO06TpQqe2GPESnQkWGcICuj/WX+54QR4YoHgfJCh9VGd5u1JLYLfS1id+ nUIhqByDdzi77nQxERho81UQdlFAspp1hWH2zaD+LF7qVyQF4aLJ9w43d2HDB4B3jw4UTHoe lTPngha+YVeOnCnBYcuPd/uV5t1nfK/SY60PhwxUjaoSsYoHONg1H8wDXN8I0iz+KTRuftmY cfHKJjE4YgyUPU7klJauNvxIZdym3llngs/tLj+xg+82LGeeWWYVaseeFqIdfw48L6YrU3S/ Z5DOsCKzRJbV+LvChQ7AqZMRW3m2UMTXMisw+QOL7brClM/SAkJVqGNqZt8Jd0Nt/kFx4/go yDmMmcFmQWXuJEyAVjTApyVQOi0BsgXQLNSFXFEAGtELFB5MNzwt/ZPLcFtFVTlncQ6pcNJo zA+U53oKpxypv7volzxtLHx895vcgqFnwWLM3b3aTQzZcc7FQfS897gOA7u6G8DAjfu7Zkyp Lip1wX6R5sfRlgyUZiLNK73l17h72IAnO9SXlfTJoUBckvb9oU3eTf6ieU6Ip1RJBianmma2 g+aDA02v+7Ip4NpotDFibrd9NWiCOJ/GgxfHnWd4LqrbHGI8m2myI5GceCJYTGBBD6qpfn+P b1YlqiuPucGkVBGt5tHP4xqla9utcHyo7J6zxh/GCmZZVqcDL49cGKN2tNCt/EQy7JU5Vm2V 0aI9oUIMLmFIpm1QlkMOAUib+KMkOoIkyXbq/8uKUT+oip24PyKXVgLZ0uAjylULb1UNoI5w Ltx5ZBLt1Dn0hd6YMybii109niXKiBSWasQsJxHUpTgjRAmyw0fbJGAWDX65oqDN4dFPkUwe G/Gg7feiLNdwEWHaGY6CXGL1vFUhJBIvRFWilIOOg3RyNbCg/Y22jxX8Cg2ElQIkEgbj7orN zg5LVBxKIWP4yxs2JpJUVeqFlwTHxae4EHwlwYEmWCxo5NEjYARwLDR+Nph/Xz1N0pbYyRU+ 7CexyP+TT/2dYf6xSIzXQhgquClQNBsnuEHdAZLAOzdd6TWoxK86kNtWYbMgxD8CMI1wkjGu a9n8PsYhWjTK3sLu6NiY2WF/e14df1HTVCuhdlq56oIGSfZeS301DSTQ6x0lgWhONSSmXKF5 wdSyg6jmvhwOOtibtzWOELUH4JJoQ==
- Ironport-hdrordr: A9a23:/u9k56tk8IP7PXQ8rLn+xRl47skDYdV00zEX/kB9WHVpm7+j9/ xG/c5w6faaslossR0b6LW90ey7MBfhHP1OjrX5X43OYOCOggLBR72Kr7GSoQEIcBeeygcy79 YCT0EzMrPNMWQ=
- Ironport-phdr: A9a23:9nZTSBfiavUoCMvn2pu0RrVBlGM+idTLVj580XLHo4xHfqnrxZn+J kuXvawr0AWSG9yEsLkZ26L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQF cVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHNbQhEniexbLF8I Rm5rQjctdQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2U bJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5 KptVRTmijoINyQh/W7LicJ+gq1Urxy8qRJhzY7aYIOaOeFkca/BZ94XX3ZNU8hTWiFHH4iyb 5EPD+0EPetAs4TyukEBrR6jDgSyBOPvzj5Ihmfs0q0+yesqDAbL0xY9EN0UtXTbsM74O7sJU e+vzanIyS/Pb/ZX2Tfh8oTHbA0uoeyVUL92bMHexlUhGRnfgVWMtYzqISmV1uIVvmWG7+RsS /+ih3I6pw1vozWj28Qhh4rNi4wVyl3J9yZ0zoYoKNGmVEJ2YMOoHYdeuiybK4Z7X94uTnx1t Ss7ybALv4OwciYNyJQi3RHfavqHfpCV4hLiUuaRPTZ1iXx/dLK+gRay7VCsyvb9VsmyzFZHr yRInsPNtnALyxzf8seHSvph/kelwzmAzBrf5f1DIUAxjabbJJ8hwqI0lpUJqkvPBC72mELwg aSLdUsk4vCl5/n5brjlvJOROZN4hhvgPqg0hMCzHPg0PhAMUmWV4+iwyqDv8EnjTLhLjvA6i LTVvI7GKckdu6W3GRVa0pw55Ba6Fzqm0MoXnX0ALF9dfxKHkpTpO17JIPD5C/e/jE2gkCx3x //cIr3uGI/BIWTYkLj7fLZ971RQyA8yzdBD/Z5bFKwOIO/rVk/wstzXEAM5PhSpz+r5C9hxz I0TVX6VDqOHKq/er0KE6v43L+mJfoAVuTL9K/Y/5/7piH80gUUScrSz0psSdH+1BehpI16Db nrthtcNC2IKvgsiTODwllKNTCNTa260X60n/j47Ep6pDZ/fRoCxh7yMxDq3EoVMZm9aElCMD Wvod4KcVvgQbyKSO9ZtnSAAVbi8UIAszgqutQ//y7p/NOXY4CwYtZT51Nh0/eLfjx8y9SYnR /iahmqKViR/mn4Cbz4wxqF250JnmXmZ1q0tqvBREJR45/dISg4+PNaIxuBzDtvaURnIf9PPT Ve6BNiqHGdiHZoK39YSbhMlSJ2ZhRfZ0n/ya1d0v7mCBZhut7nZw2C0PcF2jXDPyKgmiVAiB MpJL2yvwKBlpEDIH4CctUKfmu6xcLgEmjbX/TKKwWOLt2lTSwdxVePAXGxZa0fL/pzi/k2Xd 7a1Evw8NxdZj8uLK69EcNrs2FxKTfLoEN/FamO13WKxGVCFyq7fJJHydTA72yPQQFMBjxhV/ XuCMl0mATy9pmvFEDF0PVXyf0zr8O9x7WinR1M9iQqRZkxlkb+05lgYieH0p+o7+LUCtW9hr jx1GAz4xNfKE5+aoAEneqxAYNQ76VMB1GTDtgU7MIbyZ6ZlzkUTdQh6pSaMn11+F5lAnM42r Xgr0Bs6KKSW10lEfi+Z2pa4M6PeK2379hSiI6DM3VSW3NGT86YJoPM2zjer9AilH08p23582 thRlX6d+tPHABdTGZP9X0Ar9gRr8qnAa3p17IfV2HtwdKis52aYi5RyXK1/jEz5J4Q6UuvMD gL5HswECtL7LeUrnwLsdRcYJKVI86VyOcq6dvyA0artPeB6nTvgg34UheI1mk+K6Sd4TfbFm pgfxPTNlAKLXjL3pFy6u8Hz34VFeXcfEnf1mk2GTMZBI7Z/e4oGEzLkKsG+w95WjIXkWnoe8 V+/QV4KxYX6MQrXZFv70wpK0E0RqnHygiq0wQt/lDQxp7ae1ijDqwj7XCIOIXUDBGxrjFO2Z JOxk8hfRk+jKQ4giBqi40/+galdvqV2aWfJEw9EeC3/LmcqVaXV1PLKasJG7ZgAuj5eUeD6Z FGGDLPxvlMW3jjiEG1X2D0gP2jw6tOix1ogzjjEdD56tzLBdNt1xAvD6dC5J7YZxTcASCRiy HHWClW6I9i17ICRnpbHvPq5UjHpXZlSfC/3iIKY4XLhtSsxWVvl2arqwo6Cc0ByyyLw2th0W D+dqR/9ZtOuzKGmKad9eUIuAlbg6s18E4U4k40qhZhW12JJ4/fdtXcBj2r3Ns1WnKzka39YD zcHytveyAP+0UxnaHeI28T0WmjXka4DL5GqJ3gb3C4w9ZUAAaud6bdsljB8o17+qAPNJ/Vxg 31OrJlmoG5fiOYPtg03yyybCb1HBkhUMxvnkBGQ5sy/pqFaNy6/NKK9301kkZW9HamP90tCD W3hdM5oTkoSpo1vdUjB23rp5sT4dcnMOJgN4waMnU6IjvAJestrxrxR3Ww/fzq65CBtyvZn3 0U+m8vk+tDBcyI0osfbSlZZLmGnPpNVoWir1eAG2Z/Il4G3Qsc4QGVNAcGuFbTwV2tM/fX/a VTUTmVn+CvDQbONT0jEsg9+s2iHFoDOVTnfJX8SychuSUuYJVAZjQwJFCMzmppzfuyz7Ormd koxpjUY51qi7wBJ1votLR70FGHWuAavbD4wDpmZNhtfqA9YtQ/TNoSF4+R/Ejs9nNXppRGRK mGdewVDDH0YEk2CCVf5O7Cy5N7Gu+GGD+u6JvHKbP2As+tbH/uPwJuu1MNh8VPufo2XOWJ+C vQgxkdZdXdkB8vemjMADjcLnj7EKcWArRa4vCh2soay/OmqEAPj6I2TCqdDZNVi/xfl5MXLf +WUhSt/NXNZzsZVny+Ok+BZhhhI0nk9ElvlWa4NviPMUq/Kz6peDhpBLjh2KNMN9aU3mA9EJ c/cjNrxkL9+lP88TVlfBjmD0omkY9IHJ2alORbJHkGOYf6PKTTOyOn8eqq9TftVjfkSuhGt8 2X+cQerLnGYmj/lWgr6e/lLlz2eNQdCtZuVdQtxBm/iSt2jcQGyLNYxhiY/wLlyg3LWc2MQL HIvFiEF5q3V5iRejPJlHmVH5XcwNuiIlRGS6OzAI4oXu/9masybv+lB6XU+jb5U8GdJSOEnw UM6S/ZluFinlq+KyyYhXRZT+G4jbGOjulh+NqLY8JYFQmrN4BtL5n6ZChBMotp5TNDjpvIIo uU=
- Ironport-sdr: yYAQUS9V8i9AuKcXqPrv/V9tjErDgSJRhZcGNmI4hA43w06Zuk+EGp9V7bTyJPEyTgjcZd0aef kdBqGOnIM9uoLOu+UazPW3iDF47nVaesECvgFbLRLhttk/nBm0WVm8SR6A8SCh/e6v3V8BqCU2 BmuXfm5rHoT44ey+39WIJcuW/ccYUvLbYKJ7g8y6X6McGa4r/znBH6sBOubX/uPKAaJ1Oz82TC ysgDf/cD6Ldu6SzJVdRJNLLMWcQxwVZ4qEqNx1kOczrz2bE60W0zPl2xp3a5D728frn191tOHs aOUsHl+9/xeIJDL4sUFmT9V5
Thanks, FormalV team, for making these contributions available to all!
I am struck by how varied the topic coverage is, and it seems
like we are headed to a world with a constellation of Coq utility
libraries started by different groups, with features randomly
assigned across libraries based on historical accident. I don't
have a solution in mind, and I personally even believe we are too
early in the history of large-scale proof-assistant applications
to be sure of the best way to design package ecosystems, but it's
worth thinking about.
On 7/11/22 9:10 AM,
mireia.gbedmar AT formalv.com wrote:
Formal Vindications S.L. is happy to announce the availability of
the FormalV Library version 1.0.0.The library includes three packages:
- FV Prim63 to MathComp provides conversions from the Coq primitive integers Uint63 and Sint63 to the MathComp natural and integer numbers nat and int, and vice versa, as well as lemmas to rewrite between their respective operations.
- FV Check Range provides tactics to automatically prove Boolean goals involving 1, 2 or 3 Uint63.int/Sint63.int bounded variables through brute-force computation.
- FV Time is a library for managing conversions between time formats (UTC and timestamps), as well as commonly used functions for time arithmetic. As a library for time conversions, its novelty is the implementation of leap seconds (which are part of the UTC standard but usually not implemented in commercial libraries).
The code and installation instructions through opam are available here.
A coqdoc presentation of the documentation is available here.
This release is compatible with Coq 8.14 and 8.15, and with MathComp 1.12, 1.13 and 1.14.
The library has been developed by the FormalV Development Team, with former and current members: Ana de Almeida Borges, Quim Casals Buñuel, Juan Conejero Rodriguez, Mireia González Bedmar, and Eduardo Hermo Reyes.
You are welcome to contribute by opening issues.
Best regards,
--
The FormalV Development Team
- [Coq-Club] FormalV 1.0.0 released, mireia.gbedmar, 07/11/2022
- Re: [Coq-Club] FormalV 1.0.0 released, Adam Chlipala, 07/11/2022
Archive powered by MHonArc 2.6.19+.