coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Abhishek Anand <aa755 AT pm.me>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] ensuring .v files have no query commands
- Date: Fri, 18 Feb 2022 03:52:15 +0000
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=aa755 AT pm.me; spf=Pass smtp.mailfrom=aa755 AT pm.me; spf=Pass smtp.helo=postmaster AT mail-40134.protonmail.ch
- Ironport-data: A9a23:w4lcrq2xEcFwMehJBvbD5TJ3kn2cJEfYwER7XKvMYLTBsI5bpzQPz mMdDTrXM/aPa2WmfdwjO42//UMPvcWAmIc2QApu3Hw8FHgiRejtVY3IdB+oV8+xBpSeFxw/t 512hv3odp1coqr0/0/1WlTZhSAgk/nOH9IQMcacUsxLbVYMpBwJ1FQzy4bVvqYy2YLjW1nU5 oupyyHiEAbNNwBcYjp8B52r80sHUMTa4Fv0aXRjDRzjlAa2e0g9VPrzF4npR5fLatU88tqBe gr25OrRElU1UPsaIojNfr7TKiXmS1NJVOSEoiI+t6OK2nCuqsGuu0o2HKJ0VKtZt9mGt9te+ YkK6ZCKcCgkJZDHoPQlbwdgTy4raMWq+JefSZS+mcmazkmDLyO1mKkoFFsxIYoe/+92BSdF9 ZT0KhhUPk3F2LrwnOr9E7Iw7iggBJGD0Ic3s3g/kGzxFfNgRJ2rr6Diu4UGgWhv2KiiG97bP 8kfbgUyUi/LehZsJFtQWKtijsqn0yyXnzpw8w7F//NrswA/1jdZ27/0ddHRZ9aiXtRQhk/ep 2Tc/m2/DAtyCTCE4T+M83bp2reWxn+9QJgVCLq+8/drhBuYxgT/FSH6S3OwjsjlzRKyYetwJ lcp8RI+lZQszBCkG4yVswKDnFaIuRsVWtx1GuI86R2Qxqe83+p/LjVVJtKmQIF33PLaVQDGx XfVwIq1WW0HXKm9GSvAq+/8QSaaYHBNRVLucxPoWiMuw7HeTGwbixvOSpM/SPfu0pvtAzbsx DaPpSk6wb4T5SLq60lZ1Q6X695PjsKTJuLQ2ukxdj76hu+eTNL7D7FEEXCBsZ59wH+xFzFtR kQslcmE9/wpBpqQjiGLS+hlNOj3u6vcameC2QU/R8dJG9GRF5iLINE4DNZWeRYBDyr4UWaBj LL741gJuPe/wlPzNfcfj32N5zQClvSwT425Bpg4n/JWeJ9tcwnP9S4GWKJj9z6FraTYqolmY c3zWZ/0Ux4yUP07pBLrGbt1+eJ1l0gWmDOCLbimnk/P+efPNBa9F+xfWHPQNb9R0U9xiF6Im zqpH5DWkEo3vSyXSnW/zLP/2nhQcyBgXMiu85Y/myzqClMOJVzNwsT5mdsJE7GJVYwM/gsR1 n3iCEJe1nTlgnjLdVeDZnx5NeH3WNB6oCtjbyArOF+p3VklYJqutf1DJ8drJOd9rOEzn+RpS /QletmbBqgdQDrw/TlAP4L2q5ZvdUj2iA/XZ3ilbTEzcoROXQvM/tO4LALj+DNTXDKy884z+ uXy2gTeSJsFZgJjEMePMq7/kw/o4yJFlbsrDUXSI9RVdEH9y6RQKnT83q0tPsUBCRTf3T/Gh QyYNhEV+LvWqIgv/diV2K2Jot7yQetzF0ZXBVPW9bKnKS7e8jbxyINMSrvaZTWbUW6toPeuY uBczvfdNvwbnQ8Q79ogT+81l/ozt4n1urtX7gV4B3GXPV6lPbVtfyud1s5Vu6wRm7JUtFfkW k+L/dUGa7yFNNm/TAwULQshK7jbjKpI3CHI6ugyJkDz5Ssx97reCRdeOByFiSp8KrppMdp+n rh+45JKs1Sy2kgwL9KLriFI7GDSfHYOZKUQsM1ICoHcjAd2mEpJZobRC3Ot7ZzTOc9ANFImf m2diKbY3egOw0PDdz9vTSGWgaxFn5MSvxZPxV4GYV+Jw4KXivgy1RxX0DI2UgUMlUoYjLkvZ jAzOh0nP7iK8hdpmNNHATKmFTZBMxvFqEb//F0EyT/CRE6yW22Rd2AwNI5hJqzCH76wo9Saw F2Z9IoheTPjfcW0gnNrAhIjs+bkUdt38wTDnIasH6xp2rEkNCH9jPbGiXUg8nPa7QEZ3SUrZ tWGOM5obOv+OEb8ZoUlXpKC2+14pA+sfQR/rDIIwE/NNXnZPjS/sdRLx4ZdZesVT8H3HYSE5 wCC6y6Bu9lSFMpDk9zDOZMxHg==
- Ironport-hdrordr: A9a23:NSIoyK6UdLmKvOflyQPXwMnXdLJyesId70hD6qkRc20xTiX8ra qTdZsgviMc5Ax8ZJhko7C90cq7MBHhHPxOgLX5VI3KNDUO+lHYT72Ki7GM/9SKIUPDH4BmuJ uIa5IOb+EYE2IK6frH3A==
- Ironport-phdr: A9a23:0+PV2xfFeqCj1kq5JVt9xBM0lGM+Z9XLVj580XLHo4xHfqnrxZn+J kuXvawr0AWTG9qKoKwdw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzH cBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94PNbwlShjewZbx+I RSroQ7MqsQYnIxuJ7orxBDUuHVIYeNWxW1pJVKXgRnx49q78YBg/SpNpf8v7tZMXqrmcas2S 7xYFykmPHsu5ML3rxnDTBCA6WUaX24LjxdHGQnF7BX9Xpfsriv3s/d21SeGMcHqS70/RDKv5 LppRhD1kicKLzA3/n/XhMxqkaxVoxCupxJwzIHIe4yaLuZyc7nHcN8GWWZMXMBcXDFBDIOma IsPCvIMMPpDoIn9plsOthu+ChevBOjy1jJIgGX53asn3O88FgzJxhYvEtAOvXnUt9j1LKISX fqwzKbW1DjOae5d1jjh5obSaB8hve2MUqxqccrX0UQhGAPIg1eOpIH7PT6YyvgBvmea4udvS O+jlXIrpg9srzWv28shhIbHi40Ix1zZ9St03Yg4KMG3RUJnbtOoDJhduieHPIV4RcMiRntnu Cc8yrAetp67fTQKyJQ6xxHEcfCIb4+I4hflWe2MIjl4nGpodK+8ihuy60StyPHwWtO73VpWt CZJj9fBu38L2hfO8MaIUOF98V2k2TuX1wDc9OVEIUcsmKreMZEhw7owmoMcvEjfAyP7lkr7g LWOdkU+/eio9+PnYrPjppCGNo90jhvyPbgumsCnAOQ4NBYBX3SD9Oih17Du/Vf1TbdWgvEsn aTVrIrWKdkVq6O2GwNV15ws6xe7DzeoytQYmnwHIUpfdx2djYXkO1HDLevgDfe6mVislSlky +jAPrL6GprNNGTMkK/9fbZh7E5R0Bc/wchF551IErEBPO7zWkjpudPECR85KhW4zPrjCNVgz YwTQnmPA6+cMKPKq1CE/OMvI++WZI8UojnxMfYl5+S9xUM+zFQaZOyi2YYdQHG+BPVvZUuDM kDhmtMQLWBflwA+TffqhV7KeDhaYXr6C6s1uWxmIJqjS4LOENODmruEiQ6xHpxNZm1FQnmKG HHkP9GNUqhRNQqKJ4lkn2pXBvCaV4Y92ET250fBwL19I7+MksV5nZfq1dwuovbWiQl37jtsS cKUz2CKSWhw2GIOXT4/mq5l8gRm0lnW969+jrRDEMBLoetTW1IzPMGBksRiDpb3V1GJZc+HH W6vWc7uGjQtVpQ0yt4KbVx6HoCrh0+eggKyBvkQmu/DH4Q6p5rVxGO5PMNh0zDG2a0m2kEhW ddKPHa6i7RX8gHSA8uVyxzCy+Cyb6MA2yjI/WaHi2GO1K1BeCh3V6iNHXUWZ0+N6M/8+luHV Li2T7IuLgpGz8eGbKpMcNzgy1tcFr/lP5zFbmS9ln3VZ17Az66QbIfsZ2QW3TnMQEkCnQcJ+ H+aNA84Ti6/qmPaBTZqGBrheUTpueV5rXq6SAczwWToJwVo3uXopzYNgLqZRrJb374Jvjsgt yQhBEy0jJrdD9uNoRYkfb0JOINgpggfkz6B8VUmYs/FTegqnFMVfgVpslm70hx2Dt4Fis02t DYxyxI0L6uE0VRHfjfe3JbqO7SRJHOhmXLnI6PQxFza186bv6kV7/Ft4Vzq41z0PlIntXBqm Yodwz6H65PGARBHG5v4DRtq3wB/4bTXKHpYhcucxThnNq+6tSXH0tQiCb4+yxquSNxYNbuNC A74F8By69GGEOUxgBDpaxsFOLsX76soJ4a9cOPA3qe3PeFmlTbgjGJd4Yk73FjevyZ7T+fJ2 d4CzZT6lkOOXmih0X+5t4bylMhIaCoTEWy21SX/TNcBO+stJcBXUSH3eJH/z842n5P3Xn9E6 FOvT0gL3sOkY1v3DRS13AFd01gWvW3ynCK5yzJulDR65qGb3SHI36HjbE9eajMNGzEk0Q+qe NPo3LV4FACyYgMklQWo/xP/zqlf/+FkKnXLBFxPZ27wJn1jVa25svyDZdRO4dUmq3YyMqz0b FaER7r6uxZf3TnkGj4UzTlkKmyCopC/mhEw2yqNaW1+qnbUY5Q6zB6AuYH0XfsX2zdMF0waw XHHQ1O7Odeu59CdkZzO5/u/W2yWXZpWaSD3zImEuXjz9ShwDBa4hfz2hsz/HF1wz3rgz9czH 3atzl60cszx2q+9K+4iYkR4GAq29Z9hAo8n2ooo2MNJiSVc2c3ToSJBySCpbZ1awf6sNSpQA 2FThYKMplCighEGTDrBxpqlBCzNn40+P5/mOSVOnXhhp8FMA6OJ4LEWqjBtrAD+tRjWff97m z4czb0l6DYMiuUN8mLB1w2lC6sJVQldNC3ozFGT6sym6b5QfCCpeKSx00x3mZagCquDq0dSQ iSxdpAnFC52psJxVTCEmGX08Z3hccLMYMg7sxSVl1Kc17EOdNQpjP0WgixiMGP5+3Ylg+I2l h1h25imsZPPcjUwuv3hREIAcGSuO6Zxsnnklu5Gk9yT3pyzE5kpATgNUJbyDLqpHD8UqfX7J lOOHTk7+T+QHbvSGxPa6V8z9iKSVc/zcS3PYiBCkYYHJlHVPkFUjQEKUS9vm5c4Elvv38n9a AJi4ShX4FfkqxxKw+YuNh/lU26Zqh37D1V8AJWZMhdS6RlPoknPNsnLpOt6QHwF1oWk6gmAY D/+BUwAHSQSV0qICkq2dKGp/sXF+vOEC/CWKvLPZfDS8bUFC7GQ35Wz1Y1j9jeIcM6PdCoHb bVzyg9IWnZ3HN7ckjMERnkMli7DWMWcoQ+15ix9qs3suOSuQg/k4pGDTqdDKdg6sQ7jmr+Nb qTD4UQxYSYdzJ4HwmXEjaQSzEJHwT87bCGjSPwBrXKfFfKN3PAPSUJDLXooaINe5qY4lGGl3 ObDj5Xw2+wg5hbUI1JMVFikxpnwPpBMO3u6KFTBAU+KMPKNJW+SqykYSbu5D7hd3rw8ig==
- Ironport-sdr: 3l1V021hwMGY5Wx44rweQsKSm6w9mwR0aHcn3tBPDEkQUqXFvjdUPnnVEshiNBS47qb3llk1dC LL0Wfo20skWvMcWraPaFbU0hsUdXc8we0KCbe7u2sRcLf3YNikPm414ebWD47wMkq/nxGteSGm I7gLGZpjd4RXSaXQ7cB3oH3CpSV5/NgPiBs2pZFxtq4bc7Ya0QeMmplKKV+LWqiptlu9dNL0SP Kdh+3P45hXBYjSOZf7SdbHecWOChTP+igqQwxxPDL8ShPMQht9ulsoD0xiOTOYOhVWkrg2nI4x UZGORjgf3tgrrHeFGKEg0o1P
for just checking compliance, would it be easier to have a hook in coqtop/coqc that errors on query commands?
--
Abhishek Anand
------- Original Message -------
On Thursday, February 17th, 2022 at 10:09 PM, Timothy Carstens <intoverflow AT gmail.com> wrote:
On Thursday, February 17th, 2022 at 10:09 PM, Timothy Carstens <intoverflow AT gmail.com> wrote:
This would be (another) good feature for a Coq formatter/linterI have slowly been working on such a thing but it is not yet in a “production ready” stateJust for fun, the repo is here:https://github.com/appliedfm/vstyle-toolsSent from my iPhoneOn Feb 17, 2022, at 4:39 PM, Abhishek Anand <aa755 AT pm.me> wrote:Has someone written some automated check to ensure .v files dont have leftover query commands like Locate/Print/Search?If not, what would be an easy way to do it?Naively, I thought I could write a regexp search with grep, but with unicode in identifiers and the rich syntax of Search, I'm not sure how to do it.--Abhishek Anand
- [Coq-Club] ensuring .v files have no query commands, Abhishek Anand, 02/18/2022
- Re: [Coq-Club] ensuring .v files have no query commands, Timothy Carstens, 02/18/2022
- Re: [Coq-Club] ensuring .v files have no query commands, Abhishek Anand, 02/18/2022
- Re: [Coq-Club] ensuring .v files have no query commands, Tej Chajed, 02/18/2022
- Re: [Coq-Club] ensuring .v files have no query commands, Vedran Čačić, 02/19/2022
- Re: [Coq-Club] ensuring .v files have no query commands, Ralf Jung, 02/21/2022
- Re: [Coq-Club] ensuring .v files have no query commands, Freek Wiedijk, 02/21/2022
- Re: [Coq-Club] ensuring .v files have no query commands, Ana Borges, 02/21/2022
- Re: [Coq-Club] ensuring .v files have no query commands, Ana Borges, 02/21/2022
- Re: [Coq-Club] ensuring .v files have no query commands, Freek Wiedijk, 02/21/2022
- Re: [Coq-Club] ensuring .v files have no query commands, Ralf Jung, 02/21/2022
- Re: [Coq-Club] ensuring .v files have no query commands, Pierre Courtieu, 02/21/2022
- Re: [Coq-Club] ensuring .v files have no query commands, Vedran Čačić, 02/19/2022
- Re: [Coq-Club] ensuring .v files have no query commands, Abhishek Anand, 02/21/2022
- Re: [Coq-Club] ensuring .v files have no query commands, Tej Chajed, 02/18/2022
- Re: [Coq-Club] ensuring .v files have no query commands, Abhishek Anand, 02/18/2022
- Re: [Coq-Club] ensuring .v files have no query commands, Timothy Carstens, 02/18/2022
Archive powered by MHonArc 2.6.19+.