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 <post 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:55:42 +0200
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=post AT ralfj.de; spf=Pass smtp.mailfrom=post AT ralfj.de; spf=Pass smtp.helo=postmaster AT r-passerv.ralfj.de
  • Ironport-data: A9a23:rT2AvKyFgzJgNcxTvFB6t+cmwirEfRIJ4+MujC+fZmUNrF6WrkUPy mYbDGiEPviOMDb0ed51aY2w8RkEuZ+EzYNqTFBtrlhgHilAwSbnLYTAfx2oZ0t+DeWaERk5t 51GAjXkBJppJpMJjk71atANlVEliefSAOCU5NfsYkhZXRVjRDoqlSVtkus4hp8AqdWiCmthg /uryyHkEAHjgmMc3l48sfrZ9Usy5KWq4Vv0g3RnDRx1lA+G/5UqJMlHTU2BByOQapVZGOe8W 9HCwNmRlo8O10pF5nuNy94XQ2VSKlLgFVDmZkl+B8BOtiN/Shkaic7XAhazhXB/0F1ll/gpo DlEWAfZpQ0BZsUgk8xFO/VU/r0X0QSrN9YrLFDm2fF/wXEqfFPdgPA0K0IGP7Y1/6FdPEhBq tMzLQokO0Xra+KemNpXS8F2w9wqN9LmJp1ZoHhkwzOfAftOrZLrGv2bo4UDhHFq3Z4ITKu2i 8kxMVKDaDzYZAZTEk0eDJw82uul7pX6W2cC8QjK+fdougA/yiRq9qfMP/vFYeWAG8xqrHuE+ TrU8GfAV0Ry2Nu3kmbbqSv234cjhxjTU4ULUba86/RCm0yW3mVVCRsMVFL9r+PRt6Klc8gaM 0UP4Sc0s+4o/UilTJ/xUnVUvUJooDYtGN8KNO4K6jqgz+3+3i+WWUcvSwRoPYlOWNANeRQm0 VqAntXMDDNpsaGIRX/1yltzhWnpURX5PVM/iTk4oRwtz/SLnW3epgiKVt94C6OvkJvvEDX+w XaGoUDSZon/b+ZQis1XHnid21pAQ6QlqSZvvW3qspqNtF8RWWJcT9XABJiyxa8owHylZleAp mMYvMOV8foDC5qA/ATUH7lTQ+v4vq/bbWWB6bKKI3XH32n1k5JEVdwAiAyS2G81aJlslcLBO R+K5l05CGF7ZSPxPcebnL5d++xxkfa7TI68PhwlRtNFfplveUfetC5rb0744oweuBVErEz+U L/FGfuR4YEyUvs+lmXnHr5NgNfGBEkWnAvueHwy9Dz/uZL2WZJfYe5t3IKmP75nvpCX6h7Y6 chePMaswhBSGr+2KCrO/IJZaRhAIXEnDNqk44ZaZ8ySEDpAQWsBMv72xa9+WopHm68OqPzE0 EvgUWBlyX3+p0b9FyO0Vl5ZZonSAKlP9UAAAXR0PHKD+WQSXoK03aJOK7o1ZeYG8cJg/95VT t4EWdSxPeRKQzWa+AYmTILcqbZ6f0+BnjO+PCuCYRk+caV/RgfPxMTWQwv3+AQKDQu1rcEbo YD85jjEQJEGeRtuPPzWZN2r0Vm1m3oXw8B2YGflPfhRfx/K3LVxCimskMIyHd4AGS/DyhSey QySJxUS/svJgo0t9ej2lbK2lJioH8R+D3hlMTHit5juDhbj/02n3YNke8SLd2qEVGrLpYOTV d8MxPT4aPA6jFJGtrRnKIlSzIU82sDOooFLxQE1DVTJaFWWUolbGEek5vUWlKNxxe5+gzCUC 2av4dhRPIubNPz1SGAxIBUXVcXd9PU2tASL09ELDhTb3hJnxJuGTkRYADeUggN/MrZeEd0o0 MUhiuEs+i29jRshM4+ZvxBy5Va8DCYkVYcnvL4oGavusA4Ky05DU7PYGCTZ8JGCUPQSE0gIc xu/prvOuKRY/WXGK0EMLHnq2fFPoLg/ozVI8QMyHEuIkd/7mfMH5h1d3jApRABzzB8c8eZMF kV0Fk9yf4OiwixJgZVdYmWSBA1xPh2V1UjvwV8vlmeCbU2JVHTIHVItK9S240EV3GJNTAd1p IjC5j7ebg/rW8Xt0g8Ze01v8aXjROMs0DzyopmsGsDdEqQqZTbgvLSVWlMJjBnaGuI0ulzMo Lh73eR3aJCjDxUqnY8AN9C424gTGTe+H04TZdF6/agMI3PQRyHq5xiKNHKKW51sI97kzBaGL vJAd+N1eTaw7iKslgwgJLUtJuZ0lcE55dBZdbLMI3UHgoSlrTFokczx8Ar+jkAZWvFrq8IcK 5zQRR2GAGe/lXtZoE6Tjchma06TQ8gIWx3458+xqN42LpMktPp9V30y3p+fnWSnACE+8z265 Ar8NrLrlcp8woFSrq7QO6RkBTTsD+jsVe6NoTuBg/4XYfzhac7x5h4o8H/5NAFrPJwUadR9t ZKJlPXVhErlnrIHY1r1qqm7NZtixJuNBbJME8fNMnNlszOIW5bs7zs96mmIE8F1v+0H1Pa3Z TmTSZWWTsEUaed/1XcOSil5EjQhMYrVQJrkhxuAq6WrNkBA/y3Bdd+pzCq8JyUTPCoFIIb3B QLIqu6jrIIQ5phFABgfQepqGdlkKVvkQrErbMD1qSLeNGSzn1eeofH3oHLMM90Q5qWsS64WI K4pRyQSsDyo/bnB18pUqZI0pBQTAnQ7jeRYkoc15Yttkz7jZIIZBb11DHnEIsg8fu/OOFXQf jjJYmlkBSiVsfFsb0Dn+Nq6NuuALrVmBzo6TwDFO2uOYiO4BsWMDdONM8umD2heIlPe8Q1sF T3SFrAc8PR8LlGFiNv/PsCGvNo=
  • Ironport-hdrordr: A9a23:+tHxcKysGAwRKpJJYROUKrPwL71zdoMgy1knxilNoG9uA66lfq eV7ZImPH7P+VEssRQb8uxoV5PtfZqxz+8R3WBVB8bHYOCEggSVxeNZgLcKqgeIc0fDH6xmpM RdmsNFaeEYY2IbsS+32meFL+o=
  • Ironport-phdr: A9a23:YcmDJxO6b1pftnPhPLAl6nafBhdPi9zP1u491JMrhvp0f7i5+Ny6Z QqDvq8r1AeCB9SCuq4MotGVmp6jcFRD26rJiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wE ZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhFiiSxbaluI BmqogndqM0bjZZmJ6s+1xDEvmZGd+NKyGxnIl6egwzy6sCs8pB97i9eoegh98lOUaX7e6Q3U 7lVByk4Pm42+cPmqwDNQROA6XUAXGoWlAFIAxXe4xHhQpjxqCr6ufFj1yScIMb7UKo7WTWm7 6dsVR/olCIKPCM3/W3LlsB9ir9QrQm/rBJj3YHbfICVNOJ/fqzDe9MaWXFBVdtVWyBYH4+wc 5cDA+8HMO1FrYfyukEOoAO9CweiC+zgxCJGiGH43aM60esuDQ7I0Rc8H98MqnnYsMn5OLkQX O2z0aLGzS/Db/RT2Trl9IbHaBQhof+RVrx0bMrRz0YvHB7Cg1WIrozlJC+V2/8Xs2eB6+pgW +Cvh3Q6pA5vuzWiwNonhYbViIwP0F/E6Tl5z5gvJd2+UEN3fNCpHpteuS2GM4Z7Qt4vTmNmt ig0xLMLp5q2cTUJxZk7yRDSdf6KfoyH7B7+W+ifITd1iG5kdb6ihxu8/0eux+vhXce611ZKq zBKktjKtn0VzRzT7dSISuJk8ke5wzaP0B7T5f9eIUwukqrbMZEhz7gtnZQQqUTOBjL6lFnyg aOMaEkp9PSk5/75brjop5KQLYt5hwHmPqgzlcGyAf40PwcSU2SB5+iwyLzu8Vf5TbhEiPA9j 7fUsJTHJcQAuq62HRVV3Jsi6xe+ETiryMgUkH8aJ1xfYh2HlZLmO1TWLfD4E/i/h1OsnS9xx /zfJr3uGI7NLmPdn7f7Y7Zx8VRcxxA3zdBR5ZJYEKwOL+zrVk/wstzXEAM5PhSpz+r7DNhxz J0SVGyTDqODLq/fv16F6vgrLuSMfIMVvSzyK/kh5/7gl385nlodcLGx3ZsQc3C4Au9rI1+Db nrojNcBE30GsRcgQ+Dyjl2NSiZcZ2yuUKIk+jE7FIWmAJ/eSoy1mryOwD+7HoFKZmBBEl2DD XDod5ydV/gQbCKSP9RunycfVbmhTo8hzQuhuBX7y7phNOrU+zcXuYjt1NhvtKXvkkQ58iUxB MCA2UmMSXt1lyUGXXt+96l7v017gn2O2qsw1/xfH9Ze/NtSXw4hc4PEwup8Td3+R1SFNu+AV EynSdSvSQk8VNst39hGN15mA9i4hwzf2AKlBrYUk/qAA5lioYzG2H2kHc95xT7kya8uxw0+R dBTHXevgqB9sQTeUd2a236FnrqnIPxPlBXG832OmC/X5BkwuG9YVKzEWSpafU7KtZHj4UiES bayCLMhOw8HyMiYK6IMZMe6xU5eSqLFP9LTK3m0h3/2HQyBk6uLd5bCYWwZ0iebBEVX2xsL8 yO+PBMlTjykv3qYCTVvEVz1ZEa56e5ltFuhR0s6zUeGYh4pzKK7ryYcnufUUPYPxvQEtSMm/ i1zB0q41snKBsCovU95db5HbMkjpk1O0Wzb8QBwVnC5B4ZlgFNWMwF+vke0kg5yFp0Fi88h6 nUj0At1L6ucllJHbTKRm57qaPXRLSHp8RajZrSzuBmW2cuK+qoJ9PUzqkny9ACvGE049nx70 t5Tm3KC75TOBQAWXNr/SEEyvxR9orjbZGE66ea2nTV0NrKomiXL39wrQucoi16hc9pZLKKYB VrqCcRJT8OqKeEshx2odkddZLEUrvVseZn9Kb3Xhf3OXq4ohj+tgGVZ7Zoo10uN83A5UevUx 9MfxPre2AKbVjD6hVPns8btmIkCaytBewj3gSXiGoNVYbV/OIgRDmL7adWw3clWnZfpVXwe+ FPpVBsWndSkfxafdQm3xQpLyWwNqHipm220wnYn9lNh5rra1yvIzeP4cRMBMWMeX2hug2DnJ o2shswbVkylB+QwvCOs/l2yh61SpaAlanLWXV8NZS/9aWdrTqq3sLOGJc9J8pIh9ytNAqywZ lWTS7i1pBV/sWurB2xF2BghfjWkuNP1klR2hXmcI3B6sHfCMZgolFGFv4SaH6UPmGtbDCBjw SHaHF29I8Wk8Z2PmpHPv/r/MgDpHpxffC/3zJ+R4S6y5GlkGxq6zLi4ntzqFxR/0DeujoE7E 3+T9FCmOdethvnpVIAvNlNlD1L99cdgT4R3k49qwYoVxWBfnJKeu3wOjWb0N9xfn6P4dnsEA zARkLu3qEDo3lNuKnWRysf3THKYl4F5YMKmSnkf3iw/qcxHQvTc/PlfkC15r0Dt5xrWeuRVh D4Zx/lo5HNQ0IRr8EI9iy6aBL4VB0xROyfhwg+J496Jp6JSfG+zcLK02Rk2jZW7AbqFuA0ZR Gfhd8JoA3pr9ssmegGpsjW7+sT+ddLXd95WqhCEj0KKkb1OMJxo3v8azX1uPWa31ZE849Yyl gcmnZSzvYzdbn5o4Lr8GBlTcDv8e8IU/Djpy6dYhMefmY61TN1tHTACXZ2gSvzNcnparfP8K wOHCyExsF+BXKLWBhSS8lkgtXvLHZLtO3zfKHQCzNpkTQWQPwQG2FFSBm5i2MRiSEb7mYToa yIbrngJ60T9qwdQx+4gLBT5XmrF5U+pZjoyVJmDPU9W4wVFtA/eNc2T6P42HjkNp8Xw6lbWc irBPFoOXDxaPy7MT0ruNbSv+9Tapu2RB+7kauDLfa3Ls+tVEfGB2ZOo1IJiuTeKLMSGeHd4X JhZkgJOW250H8PBlnABUSsSwmjVaNWHjA21/iN16MyyuqeOOkqn9c6UBr1ePM86sQixmruGP vWMiTxRM3NA34gXyGXWjqIW2FAQzS1jPWrIc/xIpWvGS6TenbVSBhgQZnZoNcdG2Kk72xFEJ c/Rjt6mnq49lPM+DE1JEEDwgsz8L9JfOHmzbRmUYSTDfKTDPzDAxNv7JL+xWaEFxvsBrAW+4 H6eAwe0NzCH3VEBsji1OOVCjmeXMU4G0GlSWgxkDWbhCt7rOETT2D5fl3guyKYvi2nUc3QVN TZ+NU9A/OT40A==
  • Ironport-sdr: 681da6f3_2LiL1fCTlO8Yxv6Vr8p6Fq66C4LMkVQoFrUyPcxUtCEBP6J IWuG/mf0vwb4dD9GPXvKp8MzydI64+6xBOQ7+lA==

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.





Archive powered by MHonArc 2.6.19+.

Top of Page