Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Rocq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Rocq


Chronological Thread 
  • From: Ralf Jung <research AT ralfj.de>
  • To: coq-club AT inria.fr, Calvin Beck <hobbes AT seas.upenn.edu>, Patricia Peratto <psperatto AT gmail.com>
  • Subject: Re: [Coq-Club] Rocq
  • Date: Fri, 9 May 2025 08:56:02 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=research AT ralfj.de; spf=Pass smtp.mailfrom=research AT ralfj.de; spf=Pass smtp.helo=postmaster AT r-passerv.ralfj.de
  • Ironport-data: A9a23:+uleGKNNSP3UYdnvrR24k8FynXyQoLVcMsEvi/4bfWQNrUok3zADn WdLUWuGOKveNmP0eo0iOtm3oB9V75Pdz4c1SXM5pCpnJ55ogZqcVI7Bdi8cHAvLc5adFBo/h yk6QoOdRCzhZiaE/n9BCpC48T8mk/vgqoPUUIbsIjp2SRJvVBAvgBdin/9RqoNziLBVOSvU0 T/Ji5OZYQLNNwJcaDpOtvre8EI35ZwehRtB1rAATaAT1LPhvyJNZH4vDfnZB2f1RIBSAtm7S 47rpF1u1j6xE78FU7tJo56jGqE4aua60Tum1hK6b5Ofbi1q/UTe5EqU2M00Mi+7gx3R9zx4J U4kWZaYEW/FNYWU8AgRvoUx/4iT8sSq9ZeeSUVTv/B/wGXsVFirnK0/EHssFpECp8l+OTth+ /IXfWVlghCr34pawZqhD/Flnd8uNtetJoobtHMmwTyx4fQOGMiSBf+RvZkCh2l2150m8fX2P 6L1bRJ1YQ/NagdEOn8NAZYwnqGkixETdhUB8QzM+/VouTi7IApZzr28D8vUSp+2GOpskB6k/ FKeoGLlK0RPXDCY4WHZrCn13LancTnAcIkVDfiz8uNgqEaCw3QaThwQT1qy5/ej4nNSQPpFb lQd4TEjt7Z07kWvQNu7UxDQTGO4UgA0cf1zVLJiuR230IHI+Vu2D1BeYTBPZ4lz3CMpfgAC2 liMltLvIDVgtryJVH6Qnot4ShvoYkAowX8+WMMScecSy/XOyLzfYzrVC85qC7W4lMOzAzj0z TLMoCVWa1QvYSwjjPjTEbPv2WrESn31oukdvF6/Y45dxlklDLNJnqTxgbUbhN4ZRGpjcnGPv WIfh++V5/0UAJeGmUSlGbpRQu7ztq/cbmCE3DaD+qXNERzwoxZPmqgMsFlDyLtBbpxbEdMUS BaD4FwPjHOtFCLyNv8fj32N5zQClvS+To2/D5g4n/JHaYRwagLPpWlhYESQt10BY2Bx+ZzS+ P6zL66RMJrtIf84lWDpFr5Ege5DK+JX7Tq7eK0XBi+PidK2DEN5g59YWLdXRrFnsvG3s0/O/ sxBNsCH7RxaXaesKmPU6IMfZxRCZ3QyGZm8+YQde/+hMzhWPjgrK8bQ5rc9JK1jvaBezdnT8 l+HB0R39VvYhF/8EzusVExNUr3VYMtAnSoJBhB0ZVeM8Fo/ULmr95YaJscWf6F41elNzsxUb vgieueRM8tfTz3GpjcvVrjmjYlYbB/wrxm/DymkRzkefpBbWA3C/OH/TDbv7CUjCimWt9M0h r+dijPgXpsIQjp9APbsaP6Ay027uV4fkrlQW3TkD8ZyekK21qRXMA300+EKJv8TJSX5xje10 xicBTEar7Lvp6436Nz4urCWnby2EudRHltoIEeD1OyYbRLlx2uExZNMdM2qfjqHDWP9x/iEV NVvlvr5NKUKoUZOv49CCI1U9KMZ5eb0hrpk3w9hTWTqbVOqN+taGUO4//Jz749D+rwInjGNe BOr2sJbMrC3Ks/aAAYvBA46XN+ii9AQuBfvtMoQHmurxRVZ3rS9VWdqAyKtkw1Ydbt8D5Mky 7wuuekQ8A2OtSApOden0AFS1WSGAU4Zd6AdsrAbH47ZpQ45wX5SYZHnK3HX4bPeT/5uI0UVM juvq66avItlx23GaGsVKXjB+cF/lKY+kklG43FaLmvYh+efoOE82SNg1AgeTyNX/01h6P1yM G06DH9FD/yC0BkwjfcSQl32PR9KASCY3UnDy1Epsmn9ZGvwX0zvKFwNA8q8zHo7wUl9IAcCp Kq5zVz7WwnEZMvyhys+eXB0oszZEOBeyFfwp9CFLe+kQb8BfjvXso2/bzEpqjzmI/8Lqm/pm O1IxNt0OIrHbXM+gqtjEISL96UieDbdLkx4fPxR1qcoH2bdRTKM5QazO32BIsNjG9Ga8GuTK dBfGcZUZhHviAeMtm86AIAPEZ9VndkoxssmSpnrLjUgt7CZnyditbzLxC35mV0EftRKuuQ+I 7P3aDitPDGxh3xVummVt+hCGDOyTuclbT3G/tKe0bs2BbccluBzYGcO0reQlFeEAjtNph67k lvKWP7L8rZE149pobrJLoxCIAeFcfXIS+WC9VGIgeRkNN/gH5/HiFIIlwPBIQ9TALo2XuZ3n 5SrtPrc/hvMnJQyYlDjt6ixLYt7zuTsY7MPKePyFmdQogWaUsy14xcjxXGxGaYUrPxjvPuYV ymKQ+ruU+UKWuVt5mxfMAlfNBc/N57ZTIndoQGFkvDdLSRFjCLmKoqr+0a8OCsfPmUNNoblA wD5h+e265oK5M5QDRsDHLd9D4U+PFbnXrA8esbssSWDSFOlmU6GpqCogC9IBesn0ZVYOJ2SD VP5qhnCmNCaouTQxcpCvpZs+AceCHh/x+U9Fq7Y08AjkCi0VQbqMsxEWajqyLkN+sAx6H08T CvEaGUgTynwNdiBWQup+8ztB29zGcRXUuoU5VUVE4e8cS6yCoHGDLYJGuKMJZtpUmOL8dxL4 u3yNpE90tZdD32pqSsuCiSHvNpa
  • Ironport-hdrordr: A9a23:PCT2KKDs6XySBzLlHemv55DYdb4zR+YMi2TDpHoBLCC9Ffbo8f xG/c5rsiMc7Qx7ZJhOo7y90cW7IE80sKQFhbX5Xo3MYOCFggaVxehZhOOJ/9SjIVydygc378 ddmsZFeb7N5BRB4/rH3A==
  • Ironport-phdr: A9a23:lifXvB9yaI7tJv9uWQe2ngc9DxPPW53KNwIYoqAql6hJOvz6uci5Z gqHvb433QaYAc3y0LFttan/i+PaZSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQF cVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pDdfQlEniaxba99I BmoqQjdq80bjIR/Iast1xXFpWdFdOtRyW50P1yfmAry6Nmt95B56SRQvPwh989EUarkeqkzU KJVAjc7PW0r/cPnrRbMQxeB6XsaSWUWjwFHAxPZ4xHgX5f+qTX1u+xg0ySHJ8L2TLQ0WTO/7 6d3TRLjlSkKOyIl/GzRl8d9l7xQrg6/qBNjwo7UeICVO+R4fqPBZtMRWG5NUt9MWyBdHo+wa o0CBPcDM+lFtYnwv1gAoxWxCgaiBO3h1yFGhnH00qIm3OosCh3G0Q46Et4SrHjYstf4OaEPW u611qnIyjDDYutK1zjn7IjIfA0qr/WRXbJ2fsra1E4iFxnbgVWLt4PqJSmV2fgNs2WA9epvT +avi2Alqw1rvzeg2N4hh4/UjY0a1l7K7z92wJopJdKmUk57Z8apHZlNuiyVNoZ7X8MvTmJ2t Ss717ALu4C2cigWxZg6xxDSZfKKfoiH7x/iSuucIip1iGxhdb+jiRu8/0qtxOLgWsSyzV1Eo C1FktzWuXAM0Rze8tKHSvxh8Ue4wDqPzxrT6uZaIU8qj6rXMZkhwqQ/lpYLq0TMBCv2mEv0j KOMa0or5O6l4PnkbLX+vpKQKpN4hwXkPqgwlMGzHf40PhYAUmWa4+ix0L3u8VXkTLhFjvA6i KbUvIzAKcgFuqK0AhVZ34Yt5hu5EjyrztAYnWQcLFJZZh2HlZXnO1DPIf/mFfqzn1Khmypxy f/cJL3uGJDNI2DDkLj/ebZ97FZRyBAqwdBH/Z1UEaoBL+zpWk/vrtDYFAU2Mwi6w+blEtlyy 50RVXqOAq+fLqzSrUeF6v8zL+SIfoMZpjjwJ+Q/6/Lwg3I0mEURcK2p0JcPbXC3BPVmI0GXY Xr2hdcBFH8HvhAgQ+zxllKNSyRTaGqyX68n/DE0EoamDYnBRoy3nbOOwj+3HptNaW9eEFCDD W/od5mYW/cLcC+eP9dtkiYYWri5V48hyRauuRfmxLpgN+rY4zEXtZb+1Ndu/ODTjhEz9TlsD 8uHyW2NTmd0nnkJRzAsxqx/r1Z9mR+/1v1zhOUdHthO7dtIVB07PNjS1agyINn2RAPHNv2EQ 1XuFtWhCzs8VfoqztYVJVtlFtOkyB3PwnzuS4cci6aKD509uprRxXHtO8E1n27dzKQ7hkU6R eNAMGSnguh08A2FVKDTlEDMra+ue+w+wSjCvDOZwHGDtVtTUCZqWKHLXzYTax2F/pzC+kreQ ur2WvwcOQxbxJvHc/MSAjWIpVBPRfO4fc/bf3r0gGCoQxCB2rKLaoPuPWQbxiTUTkYewEgI5 XjTEw84C2+6pn7GSiR0HAf1bljh+PN1qFuhR0s6zUeGYh4pzKK7ryYcnufUUPYPxvQBsSYlp S9zGQOn0snbAsCLpyJ7daFSY5Ux7QQPznrX4jR0JYfoNKV+nhgefgBw6lvpzAlyA55cnNICt jYyxRFpJLiGlklIcz2am5z9UlHOAk/1+h3nK6vf21WFlc2T5r9K8/Mg7VPqoACuEEMmtXRhy dhclXWGtN3MC0IJXJT9X1xSlVAyrqzGYiQ7+4Lf1GF9eaiyvDjY3ts1Bewjgh++dtZbOamAG Uf8CcofT8SpLeUrnRCuYHdmdKhI+bU5Ntmtd9Oc0aqlPqBskXPujGhK5px8zlPZ7zB1GabD2 5cIxe3d3xPSDm+tyg366oatwt4CNGxBewj3gTLpD4NQeKBoKIMCCGP1Ztay2s07nJn1HXhR6 F+kAVoCns6vYxubKVLnjmgynQwap2KqnSygwnl6iTYs++CF0TfDyv7pdDIdM2pFRi9ugB2/R Or8x8BfR0WuYwUzwVG/6F33zrJQpIxlJm3dQwFEcmKlZ3EnWay2uL2YZsdJ4559qiRbXtO3Z lWCQ6L8qR8Xu8/6N1NX3ytzNzSju5Gi2gd/lHrYN3Fr6nzQZcB3wx7bot3aX/9YmDQcFmF0j jzeB170ONfMn53cjZrYv+mkXGKJTJRXfyutwY7IuCag5GJsCAGyhLjqwoyhS1Nil3WgiZ87C G3Bt17kb5Pu1rimPO4CHAEgH1L658dgW8l/noY2mJAMyC0fj5SR82AAlDS7OtFa1KTiKXsVE GdTkpiPu1CjghY9aCPUlOebHj2Hz8BsZse3eDYT0yM5tIVRDbuMqadDhW1zq0a5qgTYZb58m C0cwL0g8i1/4alBtQwzwyGaGr1XE1NfOHmmjRmT4tmkp6V/fm+rf7r22Ec0zrXDRPmS5xpRX nr0YMJoByJr48xlO1LkynT35IOidNSaPpoD8xaTlRnHle1cLpk8w+ELiSRQMmX4pXQ5yuQ/g E8Lv9nyrM2dJm5q5q78Hg9AO2i/eZYI4j+0x/UWjoOM0ouoBJkkBjgbQM6iU6ezCDxL/fH3f 1GHFDl2wpuCMYLWBhTXqEJvrnaUVouuK2nSP34Bi9NrWBiaIkVbxgESRjQz2JAjREimw8noc UEx4T50hBawshxX1udhLAXySE/F4R+hcSw5UobZNhNS4AME60qdPcGF7+11Fj1V5dX49F3Lc DfDIV4TUydYBwSNHDWBdvG26MPF8vSEC+b2NPbIbbiU6KRfW/qO2ZOzw95m8jKLZY2EOnhvC eF+21IWBCgoXZ6Cw3NVEHJRxn+eCqzT7A2x8SB2sM2lpfHiWQa0oJCKF6MXKtJ3vRa/naaEM eeUwid/MzdRkJ0WlhqqgPAS2kAfjyZ2enyjC7MF4GTXQbndk7VcDzYBYid9No1E4uhvu2sFc d6ekd7z2rNi27QtDExZUFX6hsyzTdZPO2imL17dGgCRPbCIJ3vHzoukBMH0Aa0Vh+JSuRqqv D+dGEK2JTWPmQ7iUBW3OP1NhiWWb1RO/ZuweRF3BS3/XcrrP1elZcRvg2R8kthWzjvacHQRO j9mfwZRo62MuGlG1+5nFTUJ62oteuCAn2zxBwzwMJ8Sv/ktDikmz4qyD1wgwr9b7mdISa4s8 MMzhsQru1i9ieSV1Hx9WR5AqHBHidDS1Xg=
  • Ironport-sdr: 681da704_T9psy0v2oQLDYjqKymN/s2U9ujUtn8CQB4nn8x8/cXJPzNK PgjQZW+esqRTR82ittmN2WiYvN4XqcEZeT1ckuA==

Hi,

The old standard library names still exist, they are just deprecated. So at least for Iris, we had to change nothing to "port" it from Coq 8.20 to Rocq 9.0. There are just some new deprecation warnings, which we'll fix eventually when we drop support for older versions.

Kind regards,
Ralf

On 05.05.25 16:44, Calvin Beck wrote:
The proofs done in Coq can be used in Rocq ?

Typically yes, but there are a few changes. I believe there are
deprecated / renamed lemmas from the standard library, imports should
change because of the new Stdlib split, and Rocq itself has some
improvements that might make things like rewrites succeed when they
previously failed, command line tool names are also changing.

https://rocq-prover.org/doc/v9.0/refman/changes.html#porting-to-the-rocq-prover
https://rocq-prover.org/doc/v9.0/refman-stdlib/changes.html#changed

Generally the changes to proofs themselves are relatively minor. It's
not too different from a typical version bump in Coq. There's mostly
just a bit more renaming of imports and stuff this time around.



--
Website: https://research.ralfj.de



Archive powered by MHonArc 2.6.19+.

Top of Page