coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] ensuring .v files have no query commands

From: Abhishek Anand <aa755 AT pm.me>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] ensuring .v files have no query commands
Date: Fri, 18 Feb 2022 00:39:02 +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-40133.protonmail.ch
Ironport-data: A9a23:yHaxMaDDoTHOyBVW/8jlw5YqxClBgxIJ4kV8jS/XYbTApDkq0DQHz mseWTvXbveKajGgeIh2aIXkphgOucOHmNNlOVdlrnsFo1Bi+ZOUX4zBRqvTF3rPdZObFBoPA +E2MISowBUcFyeEzvuVGuG96yE6jMlkf5KkYAL+EnkZqTRMFWFx2XqPp8Zj2tQy2YLgXFvW0 T/Pi5S31GGNi2Yc3l08sPrrRCNH5JwebxtF1rCWTakjUG72zxH5PrpHTU2CByeQrr1vIwKPb 72rIIdVUY/u10xF5tuNyt4Xe6CRK1LYFVDmZnF+A8BOjvXez8A/+v5TCRYSVatYozGFtdt78 81ficfuYgsJMPbcg/4iCCANRkmSPYUekFPGCX22sMjWkxWfKCCq2+9pEEYwOIQZ/qB8AQmi9 9RBeG1LMUjF27rwmengIgVvrpxLwM3DNYpA5yxI1TSfCPtOrZXrHf+WuoQFhl/cgOhKM9bnR 9NFLgYoTx+fJDxmHlErELYHybLAan7XKGEI8gvJ9cLb+VP7xwtolbPpLdD9Yc2PXcwTn0CCp 2uA8X6RP/0BHNmWyD7Arir13bSJhTn8RIUUEbS58rhhgDV/21D/FjUSWXGwq8KhmHLlBflTC 0JP6jE0kvMLoRnDosbGYzW0p3uNvxg5UtVWEvEn5Azl9kYyy1vIboTjZmMQAOHKpPPaVhR2i QbVw4KB6ShH4OTIFCr1GqK89GvqURX5O1PucgcvbWM4DzTLpYgyileTFo84S+itlNrpHjf1y jGO6iM+71nysSLp//vrlbwkq2j2znQscuLTzlmINo5Cxl8nDLNJn6TytTDmAQ9ode51tGWps nkegNS55+sTF5yLnyHlaLxTQOzwvazbaGaM2QAH83wdG9KFpi/LkWd4vWAWGauVGp9slcLBO hSL5Wu9GrcKZCPCgVBLj3KZUJh6l/G8RbwJp9jMdN1SZZ45fQDvwc2dTRD44owZq2B1yftXE c7DL66EVC9GYYw6kmbeb7pDgNcDm3BvrUuOFMuT50n2gdK2OiXPIZ9bawTmUwzMxPjZyOkj2 40DbJTiJtQ2eLGWXxQ7BqZJcwhRdCBjXcqeRg4+XrfrHzeK0VoJU5f5qY7NsaQ890iMvuuXr Hy7RGFCz1/z2S/OJQmQNyJ7bfXqUM8n/348OCUtO3eu2mQiONzzvPtDLsVtJbR3pvZ+yfNUT uUef5nSCPp4TDmaqS8WaoPwrdA/eRny3VCOMiOpbSIRZZllQwCVqNbochGypjELSC+67JNsr 7ql3wLdYJwCWwU7VpqGNK72kQnpsCFEyuxoXkbOLt1CQ2nW8dBne37rk/s6A8AQMhGflDGU4 ACbXEUDru7Xro5prdTEiPnf/YekGudzBHBXB23K8bGyOXWI92av29ISSOPOeD2EDDH4/6CrZ ON0yfDgMaRdwAYW79MiSe5mnfAk+t/ih75G1QA4Tn/FWFKmV+F7KX6c0MgT66BAy+MLuQayX U7TqNBWNa/TZJHgGV8VYVZ9N7/Yk+kOnSXV6/E8IUG87y8upOiLVkBbPh+tji1BLeIub9x6m rt94JYbu16llx4nEtealSQKpW6CGXw3Vfl1vJ8tBoK22BEgzUtPYMCHByKqsouDbc5AbhsjL jOO3vaQgr1dwg+eKyNoTj7Vx+1BgpILsRFOilQCfgzblt3Aj/4x/RtQ7TVuFVsKkU4bj7orN zg5LVBxKIWP4yxs2ppJUVesLAcdVheXzUr8lgkSn2rDQkj0DWHAIQXR4wpWEJz1Lo6dQtRaw F1c4GPsUDKvIJmohXB0QVRit/vlSNVw8kvJmKhL2uybSoIib2ONbrCGPAI1R9nPWKvdR3ErY cFy+aB1ZMUX8AYO9rYjBdDyOas4EXi5ya8rfR2l1LsMW2TREN13Nf5iNGjpEv5wyzf2HYNUx iCgyg+jl/hz6cpWkg0mOA==
Ironport-hdrordr: A9a23:N/EOaap8CdKpnjb6EQC/r1UaV5o+eYIsimQD101hICG9E/bo9P xG+c5w6faasl0ssR0b9exoW5PhfZq/z/9ICOAqVN+ftW/d11dAR7sN0WKN+VDd8jXFh4tgPL lbAspDNOE=
Ironport-phdr: A9a23:hWYNhBMtV9tdSvAs6Iol6nbFBhdPi9zP1u491JMrhvp0f7i5+Ny6Z QqDv68r0w6CB96TwskHotKei7rnV20E7MTJm1E5W7sIaSU4j94LlRcrGs+PBB6zBvfraysnA JYKDwc9rDm0PkdPBcnxeUDZrGGs4j4OABX/Mhd+KvjoFoLIgMm7yf6+94fRbghMizaxf71/J wiqoAvMscUbnZFsIbsrxBvTpXtIdeVWxWd2Kl+Wgh3x+MS+8oN9/ipJo/4u+NJOXqv8f6QjU LxXFy8mPHwv5M3qrhbMUw2C7WYBX2oMkxpIBw/F7AzmXpr0ryD3uPZx1DWcMMbrS70/RDas4 LpxSBLwhikJKT438HvKhMJzg61UvAmsqAZjz4POeoyZKOZyc6HbcNgHRWRBRMFRVylZD46gd IQPD+sBPf1Yr4bjpFsFsAezBQ+2C+Pp1zBDm3j70rcg3OkjEQzL3BctH8oLsHjOqdX6Kr4fX Oaox6bH0TvNdelZ2Svh6IfWaBAhp+mBULNsfcfPyEQjCQPIg1aNpYD7MD6Yy+cAvWeV4uZ+S ++ilmEpph9trjWs2MohjpfFipwVx1zY9Ch03Js4KN24RUN9fNWqE4NQujmHO4Z1Qs4uWWNlt DogxrAJpZK3ZjUGxZopyhPZdveJaZKH4gj5W+aUOTp4hGxqeLa4hxuq9Eiv0Oz8Vs2t3FtFs iZJj9fBu34X2xzL8MiHTed9/kCn2TaKzQ/T6+VELVoomqrbM5Ihw7gwmYQPsUnbAyP7m0X7g LWUe0k44OSl5Pjrbq/7qpKSOYJ4kgT+Pb4vmsy7D+Q4KA8OX22D9OumzrLu/030TbVRg/0ul 6nVqpXaKtoDqq6/GABaypwj5AqnDze6zNQYmmEKIE9ddBKdk4fpI03OIOz/Dfqnn1usly5ry +naMb3lH5XCNWPOkKzhfLZ4805T0hA/zdFZ55JOC7EOOuj/WkHrtI+QMhhseQez2qPsDMh3/ oIYQ2OGRKGDeuuGuliRo+krPuOkZYkPuT+7JeJztMTjlXsopVhIVKOp3IAXZXPwN/JvJUnRN XPl3YpcOX8P+A8zGr/EklqHBBdZZ3epX68/rhg9AYSqRdPKT9/w3ZSZ2WG+E8sFNSh9FlmQH CKwJM2/UPAWZXfKSicAujkNVLz6DpQkyQnrrwjijbxuMuvT/CQc85Plztl8oePJxlkp7TIhK cOb3imWSn1s2HsSTmo/1f8i/GRlzxGG3PswmORWQORa/OgBSQImLdjZxu1+Bcr1X1fId4jUF X6+R5OjDGJ5Vco/lucHeF01ANC+llbD0i6tVqcSjKCODYco/7j02nHwI4Mhky+dj+85lV46R c1KPGyiwKV/n+TKL6jOlUjR16OjdKBHmTXI6H/G1m2W+kdRTA93V6zBG3EZfErf69rjtAvES Pe1BLIrPxEkq4bKI7ZWatDvkVRNRevycNXYbWWrnm6sBBGOjrqSZYvucm8Z0W3TEk8B2wwU+ H+HM0A5CELD6yrXBWMzSHr3ZgXp/Kg2qX+2SFM10xDfd1dohPK+/h8Yg+DZSutGh+JZ/nh57 WksWg/mhIGzaZLIvQdqcaRCbMlo5V5G0TmcrAlhJtm7KLgkgFcCcgNxtkeo1hNtC4wGn9J5y RFihAd0N6+c10tMMj2C2pWlcLTedTSv1AiqLavbkAKWwJON96ED5e5t4Vzq41z0PlIntXBqm YowsTPU9tDBCwwcVoj0W0A8+k1hpr3UVSI64pvdyXxmNaTcXibq49syH6Nlzx+he4waK6aYD ErpFNVcAcGyKessklzvbxQePekU+rRmd8+hcvKH3uasMoMC1HqvhDsavahl1wSJ+mJwR/XJ0 JAM3/yDllLXCnGj1BH96oauwtsMbCpaBmelzCn4GINdLrZ/e4oGEybLQYX/x9lzgYLsR28N8 VeiA10c38r6MRGWblH7wUhRzRFO8SHhxnP+k2Qyympy/c/9lGTUzu/vdQQKIDtOTWhm1hL3J JSsyssdRA6uZhQokx2s4QD7wbJareJxNTq2Iw8Aci7oImVlSqb1uKCFZpsF4Zp37Hh/SOH6Z F3QGfbt5gAX1S/uBT4UzTlkKmyCopC/mhEw2wf/ZD5j6XHef8933xLW4tfREOVQ0jQxTy59k TDLB1K4Morh7ZCOmpzEqOz7S3O5W8gZb3zw1Y3Z/njehyUiEVilkvu0gNGiDQUqzXqxyYxxT SuR5BfkPtuyh/n8brohIhEuXBimt4J7At0sy9ttws5InyRDwM3SpyZi8y+7MM0Hi/uuMTxSH XhXmJiNp1K5kExlJXaUy4+rYW6FzJEnf8O9fmQQ3ys864ZBCO+C5bhA10OZu3KApBnKKbh4l zYZkr417WICxvoOoEwrxzmcBbYbGQ9ZOzbtnlKG9YL2oKJSbWepOb++sSg21cimF62HqxpAV WzRf54jGWostpwkaxTUynrv7YfhcdjUK9kT/hGZiBbPieFJJYl5z6pXw3U/fz6l+yR+kItZx VRnxtmisZKCKnlx8a7xGRNeOjDvJosS9jzrkadCj5OW0oSoTd1qHjQGWoetTOr9SWJP86u/c VrWVmRn8ST+e/KXBwKU5UZ4omiaFpmqMyrSP3wF1ZB5QwHbIkVDgQcSVTF8n5gjFwnsytayF SUxrj0X+FP8rQNBj+xyMByqGG7W+1r1Qi8xDp2SZkkzjEkK9wLOPMqS4/gmVTlf5YGkpReRJ 3azYg1JCSRVAhXfXBb7JL6y4t/F+umcQOG+ZairA/3GualVUPGGwoiq241t8mOXN8mBCXJlC uUyxktJWX0qU9ScgTgETDYb0j7cd8PO7gnp4TV594rslZajEBKq/4aEDKFedMli6wzjy7nWL Pae3W54MWoKj8NRgyCQjuRHmgdJ0Gl4fj2pW9zoWgbVSeTVl/0OZ/b6QyZ6Nc8Ns/plhVILI dTcltTz07d5irg+CwUcPbQEstmsI8kHcTnVCQ==
Ironport-sdr: akwM/iwIitYqqVnQIKk1gCAu+w/QFXnC9oxiLekX6IXrmtIUqhQT28RVKt2+pWP14rKITy6WkT VJR0iFGWUtcr2WOWx631asStFYt5WWkuV90yVvj3VE/mv6Ew4aLgwC4ex91ReWh5MIQbXrWns7 F5do3nKVTSiRrwsVzNFzrK+nhLpwFDZXimAdK7aSA6EpXhDodLuw2DYkqqEqdkC6nLSK65/Dxr yR0cmQISG/fltiGR2g1ml9Mm5DhC67Fxy3Lqwuw93c9WPuivdvIfkCe905/CLChlWa7rzbP4e9 +OeYTGan8CuDDEqdncDuHguj

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, Pierre Courtieu, 02/21/2022
      - Re: [Coq-Club] ensuring .v files have no query commands, Abhishek Anand, 02/21/2022