Skip to Content.
Sympa Menu

coq-club - [Coq-Club] FormalV 1.0.0 released

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] FormalV 1.0.0 released


Chronological Thread 
  • From: <mireia.gbedmar AT formalv.com>
  • To: <coq-club AT inria.fr>
  • Subject: [Coq-Club] FormalV 1.0.0 released
  • Date: Mon, 11 Jul 2022 15:10:59 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mireia.gbedmar AT formalv.com; spf=Pass smtp.mailfrom=mireia.gbedmar AT formalv.com; spf=None smtp.helo=postmaster AT mail.guretruck.com
  • Ironport-data: A9a23:iviyjq9qtHKZtarUD4ShDrUDKniTJUtcMsCJ2f8bNWPcYEJGY0x3n 2McDWrXa/6IYDbxf992Yd+08h5T75fcxoVlQAFo+XpEQiMRo6IpJ/zJdxaqZ3v6wu7rFR88s Z1GMrEsCOhuExcwcz/0auCJQUFUjP3OHvymYAL9EngZqTVMEU/Nsjo+3b9j6mJUqYLhWVnV5 oqr+5S31GKNglaYDEpEs8pvlzs05JweiBtA1rDpTa0jUPf2zhH5PbpHTU2DByOQrrp8QoZWc 93+IISRpQs1yfuC5uSNyd4XemVSKlLb0JPnZnB+A8BOiTAazsA+PzpS2Pc0MS9qZzu1c99Zl s1pvNu2Si4QOYbTleZHfhBxTiA5FPgTkFPHCSDXXc27ykTHdz3j3u9jEFsrNo5e8eFyaY1M3 aJCbmFcKEHawbvvnNpXScE07ignBMzqJo4eszdvxzzVCP88aZ7EWaDD4cEe1zA17ixLNa+PP 5RGMmIzBPjGSw1VAE4oD7Akpb2h3EXjen5TkhHNmaVitgA/yyQqiuG9b4CNEjCQfu1emV/dr Wbb9UziExQCPZqezyCE+zSinIfycTjTXYsTEPu36+RnnEeOzW9VAxoTPbemnRWnohCmf9sYL U89wy0FsqUwrmGiZ4T8GDTt9RZooSUgc9ZXFuQ77iSExazV/xuVCwA4othpNYBOWCgeGGJC6 7OZoz/6LWA06uPPFBpx4p/R92LoYnd9wXoqOHdscOcT3zX0iKwI5v4lZvxiFKS8ibUZ8hmsk 2jS9UDSa505hNUSyqjz1lfahS62t/D0ouMd4wzWWiSq8xl0eJS4bI/u4l/ehRqhEGp7Zgba1 JTns5HPhAzrMX1rvHfSKAnqNO31j8tpyBWG3TZS82AJrlxBAUKLc4FK+y1ZL0x0KMsCcjKBS BaN5FwNu8ADZiTxMP8fj2eN5yICkPaI+TPNC6C8UzaySsYZmPKvoX40ORfOt4wTuBR9yfBX1 WinnTaEVixDWfs9lFJats8QzKQozyQiyGe7eHwI50rP7FZqX1bMEe1tGALXPogRsf3YyC2Ir Yc3H5XQl313DrakCgGJqtF7ELz/BSJmbXwAg5AMK7Trz8sPMD1JNsI9Npt7KtY6xPUFzL2Sl px/M2cBoGfCabT8AV3iQhhehHnHBv6TdFo3Yn4hO0iGwX8mbdr95asTbcJuL7cg7ulqyeAyR P4AIp3SDvNKQzXB2jIccZik8tE5LkT631rRMnr3eiU7cr5hWxfNq43tcQbY/SUTCja66Jklq Lq62wKHGZcOHlwwDMvfZP+14Um2uHwRxLB7U0fSe4ABdkL29YFuNWr6ifpue5MALhDKxz270 QeKAE5G+LKX895vqIbE3PnWoZ2oHu1yGlthM1PatbvmZzPH+meDwJNbVLfadD/QY2r45aG+a LgH1Pr7KvAGwA5HvoclSORrwKsy6sHVqqde3xhjGHmXPV2nBqk5eyuI2tNKv6lTgLRevFLuC E6I/9BbP5SPOd/kSQBMf1B1P77bivxEyCPP6fkVIVnh4H4l9bWKZkxeIh2QhXEPN7ByKo4kn b8stcNKuQyyjh0mboSPgixOrjTeK3UBV+Moq4sXHJX2gQltwVZHOMSOBijz6ZCJStNNLkh7f 2HJ2/Gc3eVRlhjYbn4+NXnRxu4D154AjxB901JfdU+CncDIh6Fr0UQJoyg3VAlc0j5Oz/l3Z jpwL0RwKKjSrS1kgtNPAzKlFw1bXU3L/0Xwzx0GiXfUU1O1XW+LJ2o4YL7f8Ecc+mNaXz5a4 LDJlTi4Dm20JpD8jnkoREpoi/3/VtgvpAfMr8CQAMnYTYIxZiDog/HyaDNQ+QfnG844mGbOu fJuoLRrcaT+OCMdy0Hh51J2CVjEpNG4yG1+rTVJ+aoIGSfTZSu/xSKTIEP3ccRITxAPHYlUF OQ2Tv+jlTznvMpNktzfLaALObp9mOBv790HEl8uDXBTqKOR91KFr7qJnhUTRwYXrxFGn8EnL 4rVaXSJFWn4ab64XYPShJEsB1dUquXoqOExMC5ZPQnJ+18+XDlQTHwP
  • Ironport-hdrordr: A9a23:fPHZIaoYziebNw9ihSPXZEcaV5oceYIsimQD101hICG9E/bo8/ xG88506faZslossRIb+exoWpPgfZq0z/cci7X5W43SOzUO01HGEGgN1+bf6gylPwG73eZM2b 1he68WMqyXMbEDt7eY3ODlKadD/PC3tJuljeq29QYJcekQA5sK0ztE
  • Ironport-phdr: A9a23:PEPoJR/1bbbbEP9uWU+2ngc9DxPPW53KNwIYoqAql6hJOvz6uci4Z wqGuq4m0QGBdL6YwsoMs/DRvaHkVD5Iyre6m1dGTqZxUQQYg94dhQ0qDZ3NI0T6KPn3c35yR 5waBxdq8H6hLEdaBtv1aUHMrX2u9z4SHQj0ORZoKujvFYPekcq62/qv95DRbQhEizqwbLJvJ xiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4U KdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4 KdxUBLmlicJOSM3/m/UhcN+i7tVrw67pxFk2YHYfJ2ZOeBkc6/Bf94XQ3dKUMZLVyxGB4Oxd 4wCD+8APeZCsYb9pkEBoQGxBQa3Guzg1zpIiWXs3aAh3eQhFhvG3Ak6ENIKrnTYtsn6NKAXU e2syqTD0DrMYe9M1zjn9IjIbg4uoeuKXb9ofsTcxlUiGgfKg1ufp4HoPy2Z2/kTv2Wa8uZtS eyihmA6pgx/vDSiyMghhpfUiowaxF3K+jt0zZs6K9CmVkN2b9ipG4ZeuSGdMot5WMIiQ2dwt SYny70Gv4K7cSkExZg9xh7fbeCHf5CT4hLiUuaRPTZ1iXx/dLK+gRay7VCsyuL9Vsmo1FZFt DFKnsPQuXAK0hzf8seHSvph/kelwzmAzBrf6uBDIU0yiKHVKIYhz6Yxm5YNq0jOGiv7lF/yg aOLbEko5/Wk5uv/brn7qZKRM5V4hwPxP6g0hMCyDvk0PhIQU2SF5Oix0qDo81fjT7VQlPI2l 7HUsJDEKsQfoa60GwpV3Zwi6xa7FTum38kYnWMZI1JZYhKHkpTmO1LULP/kCve/hkygkDZtx //YIr3sGpTAImbZnLrlebtx8UpRxBcpwdxC+p5ZBakNIPfpVU/wsNzYAAU5Mwuxw+v/DdV91 5keVnyOAqCDKq/SvkSH6fwyLOmJfoAVoi3wK/Yi5/70iH82g1sdfbez0ZQLb3C4G+xqI0OCb nX0mNcODX8KvhYiTOztkFCOTCZfZ2yuUKIk+jE7FIWmAJ/fSYCqmbyNxTu0HplLZm9dEV2MC nfpd4CcW/gWci6SI8lhkiYFVbe7UYMh2wuu50fGzO8zJe3NvyYcqJjL1d5v5uSVmwtkpgZ5F 8CM72bYSmBuk2IBATA80ax6qFZVxFCZ1KF8nbpTEtkAyelOV1JuMJ/Gwu1zTd/4Vw7Ed82hR lG8R9yiH3c6SddnkIxGWFp0B9j31kOL5CGtGbJAz9RjZbQx+6PYhD3qItpljm3BzO8nhkUnR c1GMSungLR+/k7dHd2BiF2XwoCtc6lUxyvR7CGb12PbuUBCXQ95F6rPUHwab1H+o9Pj40rGU fmlDrF0ehBZx5u6I7BRIsbskU0AQf7iPNrEZGfknmaqCBeBgLyGYYbvcn810iLHDUEAjUYY+ nPVfRMmCHKHpGTTRCdrCUqpY07o9rxmr2inS0Yv0wyQR0ho1r7z9QMPiOCGVvgQmLkDvU/Ns h1SG1Cwl5LTAtuE/E96eblEJMg6+BFB3H7YsAp0OtqhKbpjjxgQaVY/uUSmzBhxBoha9Kpi5 Ho30Ap/L76Z21JdZnuZ2573ILjeNmj1+limdafX3ljU1Nve9L0I7bw0rFDqvQfhEURHkT0v1 thP3nqVoJrAAQYXWIjZXEEt8hF+uffRZSx8r4LY2HtwMLWl5yfY0oFMZqNtwRKhctFDdaKcQ VGoVZxLQZn3brVzxwvMDFpMJu1Z+a8qMtnzcvKH3PXuJ+N8hHe9inwB5olh00WK/i46S+jS3 p9DzevLu2nPHzr6klqltdj63I5eYjRHVG++0yXlDchebKB+eI8RIWmpOci+wss4jJnoES09l hbrFxYd1cmldADHJVn8xwBR3AIYq3GrnCKi5zJziTQgqrTZ1yvLibeHFlJPKitAQ29sik3pK I6/goUBXUSmWAMukQOs+Ufww6UzSL1XF2DIWg8IeiH3KzonSa6srv+ZZNYJ7po0sCJRWeD6Y FaAS7e7rQFImy/kGmJfwng8eVTI8t38ngZ3iWvbI3x+oH/QY+l+wg3a7djCA/VW23IKSTJ5h j/eGlWnd4fzu4TF0caa9LnnCyqoTfgxOWHzwJmFtTen6GEiGhC5k/2p25XmHQU8zS7nxoxvX CTMogz7Z9qj3KC7POR7O0hwUQGmrZsrXNAn1NJp2MJ1uzBSnJie8HsZnH2mNNxa3fm7d38RX XsQxMaT5gH52UplJ3bPxoTjV3zbzNEyArvyKm4QxC856NhHTamO67kR1y50uFe5pETea/Vxm z4H4fUp8nsTh/9Psw0ohHb4YPhaDQxDMCrgmg7dpdW/tqhWbSCge7W80UNktd6mFrSLph8aU 3H8MMRHf2c4/oB0N1TC12f244fvdYzLbN4dgRaTlg/Jk+lfLJ9i3upPnydsPnjx+GE00+Nux wI7xom05cLUTgcltLL8GBNTMSf5It8e6i24x7gLhd6YhsiqDt0kEzEPFvMEVNqOFzQf/bTiP geKS3gnr2uDXKHYBUmZ4VtnqHTGF9aqMWuWLT8X14cqQh7VP0FZjA0OOVdy1pckCgCnwtDge 0Zl93gQ4FD/sB5F1uNvMVH2TG7eoA6ibjp8RoKYKVJa6QRL5kGdNsL7jKo7ByZD4piotxCAM ESebgVMS24UQEGYHU3oPf+l4tyBu+mUC+yiLuffNLWDresNMpXAjZmr04Zg43ONLpDRZD8zX rtqgwwaBCwqfqaR0y8CQCEWiS/XOsuSpRPnvzZystj66/PzHgTm+YqIDbJWd9Rp4RG/x6mZZ IvyzG50LyhV0pQUyDrG0r8aiRQXijtjdjDrHr4NuSvEVorenbVSBhoFLSh0MYEbisB0lhkII sPdht7vg/RgieUpDl5eSVH7ssSgZMhMLHynOU/dGU2Icr+BIHeYpqO/KbP5QrpWguJOshS2s jvOCE7vMAOIkDzxXgyuO+VB5Ml+FBJZooS0dggrAm/mHoqOgvyTNdZ2iXs53Kc5mmnXPm1aO j95IRslRlK44yRCh/x7BSpK6X83dIG5
  • Ironport-sdr: y+ucTmSrR5fcrot8TTC/mS+sXQkbdZlZpMOHona00nahiykZHxdijgQWGR2I1wCvG23gQto6Pd NrTOaPwbbRERyI7M82s7AmzA14caqKN2JGc9Sx8o3zFFooptalHf+VfsP5UuBwb9B6pP60H1I/ KRu0aqFD05ewPbRtKFlsV4xjc1y6QfgKuo1fvxnZEZus1ULjAPXMcvLRTPT56SbYhOSfeUv0iI E3RkbHTGMo/LxHEMpWZkZrXditIVjGV3JQoXuX6+/XUtRH87/DiKjYcpfZHOglP4mgpEpl/EhL ZJ8TORQtVJhZQYc5gV3TElF1

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


Archive powered by MHonArc 2.6.19+.

Top of Page