Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] ensuring .v files have no query commands

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: Timothy Carstens <intoverflow AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] ensuring .v files have no query commands
  • Date: Thu, 17 Feb 2022 19:09:27 -0800
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=intoverflow AT gmail.com; spf=Pass smtp.mailfrom=intoverflow AT gmail.com; spf=None smtp.helo=postmaster AT mail-pj1-f50.google.com
  • Ironport-data: A9a23:QjRQkKlUggTQ/PnyK+fsR23o5gypIERdPkR7XQ2eYbSJt1+Wr1Gzt xIaWGqBP6mPZzb3fIwiPtu1oUIDuJfSyNNkSQtk/HhgHltH+JHPbTi7BhepbnnKdqUvb2o+s p5AMoGYRCwQZiWBzvt4GuG59RGQ7YnRGvykTres1hlZHWeIcg944f5Ys7N/0t4AbeSRWVvX4 4uo+pKHYzdJ5hYtWo4qw/LbwP9QlK+q0N8olgRWiSdj4TcyP1FMZH4uDfnZw0nQGuG4LcbmL wr394xVy0uCl/sb5nxJpZ6gGqECaua60QFjERO6UYD66vRJjnRaPqrWqJPwZG8P4whlkeydx /1PjsKqE18VZJHylc4hAxMbPyhBYfNvreqvzXiX6aR/zmXDenrohu1sVQQ4YNVe9eFwDmVDs /cfLVjhbDjZ37PwkO/9ELAywJl7RCXoFNt3VnVIzDfFCugrW57HRLri6tpR3TN2jcdLdRrbT 5RDN2MyMkSojxtneXYIDZYYmMiSxUbebBlomUqTmqZn7D2GpOB2+OG1bIC9lsaxbc5ShwOTo n/M13/oBwkTct2Z0zuMtHy27tIjhgv+UYMWUaW6r7tk3QXVyWsUBxkbE1C8pJFVl3JSRfpdE BIOoHIS95QM+WaXHtO+cxSH/CCt60t0t8VrL8U27wSEy6zx6gmfB3QZQjMpVDDAnJ9mLdDN/ g/Z9+4FFQCDo5XOFi3Arub8QSeafHlKfTVbNEfoWCNcu4G7yLzfmC4jWTqKLUJYptj8GDW12 zLT6SZj3/MciskE06j99lfC695NmnQrZl5ojuk0djj9hu+cWGJDT9LygbQ8xagbRLt1tnHb4 BA5dzG2tYji962lmi2XW/kqF7q0/fuDOzC0qQcxQ8R4rW7zoyb/LNw4DNRCyKFBYpZsldjBM B+7hO+tzMI70IaCMfUuONroU6zGM4C5TYu5B5g4keaikrAoLFPdlM2fTUGX2G/pnSARfVIXa P+mnTKXJS9CU8xPlWLoL89EiOND7n1gmAv7GM+jpzz6gOL2TCPEEt8tbQreBshnt/jsiFuOo 75i2z6ikUo3vBvWOXmJr+b+7DkicRAGOHwBg5YJLrXaelI+QgnMyZb5mNscRmCspIwN/s+gw 513chYwJIPXiSKVJAOURGpkbb+zD59zoWhqbyMpNFesnXMkZN/3vqsYcpI2e5gh9fBinaYkF albJ53YD6QdUCnD9hQccYL5895veRGtsgSEYHiobT05SJh/SlGb4dTjZAbuqHIDA3Pv58szq rGtzC3BRp8HS1gwBcracqP9wFa4vHxbk+V3BhOaLt5WcUTq0Y5rNy2h1q9tc59QcU3On2LI2 RyXDBEUofj2j7U0qNSZ17qZq4qJEvdlGhUIEmTe64GwP3aI82emx7hGT7/ULz3QUWXD+JKia /9Q+PfyPaBVh11NqYd9T+9mwK9itdvio7hWklZtEHnRNQ/5D7phJjye35AKuPAVgLBevgSyV wSE/dwDYeeFP8bsEVgwIgs5b7TciatFxGGKtfllcl/n4CJX/aacVRkANRe7jiEAfqB+N5kow Lt8tcNKuRazjAEmboSPgixOrT/eK3UBV+A/tMhfDtKzzAUszV5GbNrXDSqvuMODbNBFM08LJ D6Ihfqd2+4NmBKaK3djR2LQ2ed9hIgVvEwYxlE1IVnUyMHOgeU63UEM/Dk6JuiPIs6rDw6u1 qlX20xJyWGm+j5pgI1bXTnpFVwZQhKe/UP1xh0Ck2ixo4xEkIDSBDVVBApP1BlxH6Fgkvxz8 7SRyWKjWjHvFC009jVnQlZr8pQPUvQonjAvW6mb8wCtEJwzYD6jiairDYbNR90LHutp7HD6S SJWECqcpEE12eP8Y0H2NmVC6YktdQ==
  • Ironport-hdrordr: A9a23:F5k25KiClWZmDqGj+Mw3+HxRZnBQXvgji2hC6mlwRA09TyXqrb HNoB19726PtN9xYgBapTnuAse9qB/nhPhICMwqTM6ftWrd2VdATrsM0WKK+VSJcECTygce79 YET0EZMqyWMbEQt7eY3ODXKadF/DDKysCVbZK09QYRcekiAJsQkzuQV2ugYzVLrdZ9b6YEKA ==
  • Ironport-phdr: A9a23:kBPV3hXoxsUSMnzA/9wsUKgGOnLV8KwRXzF92vMcY1JmTK2v8tzYM VDF4r011RmVB9+dtKMP1rGempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yN s1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffRtEiCC/bL52I xm7rQvcvdQKjIV/Lao81gHHqWZSdeRMwmNoK1OTnxLi6cq14ZVu7Sdete8/+sBZSan1cLg2Q rJeDDQ9LmA6/9brugXZTQuO/XQTTGMbmQdVDgff7RH6WpDxsjbmtud4xSKXM9H6QawyVD+/6 apgVR3mhzodNzMh7G7Zhcx+g61GrhyvpBJ/zYzbbp+SOvdlZKzQf9YaSHBBXspNVSFMBJ63Y YsVD+oGOOZVt5fzp1oLrRu5GQmsBOPuwSJWi3Dsx606yPghHh/A3Aw7AtkDt3XUrNPpNKcVT +C60rPIzTvHb/NR1zbw84fIchU7rvGNWbJ8a9beyU4qFw7ciFibtIPqMS+P2OsXr2ib8/RvV fipi2M/pQx8ojuiy9syh4TJmI4YxVHJ+CdkzIs3IdC1TEF2b9C4HJZQtSyUOIt7T8M+T29mt is0xKEKtIO5cSQXyZkpyRjSYOGJfYiP5xLsTueRITFgiXJqebK/mxay8VW7xeHmSsa011NKo yxYmdfPrnAAzwLf5tSDR/dn/Uqs2SyD2x7O5uxFO0w5lbbXJ4Yjz7M+jJYfrFjPEyvslEnog qKaal8o9vW15+nhf77ovIWTN5VuhQH7KqkumtKwAeA/MgUWWmiU4+W81Ln68U3hQrVGk+Q6k qfZvZzGP8gbqam5Awha0oYn9RmzFSup0NMdnXUfLVJFfgyIj5TxNl3QPPz1Ce2zjlesnTtx2 fzKI7zsDo/NI3TfiLvheKxy609YyAo919Bf4JdUB6kAIPL1Rk/xs8LYAQEjMwy6x+bnD9t82 5gRWWKKGKCZMafSvUWU6eIoJumAfIkVty3lJPg/+/HulWM5mUMafaSxwJcbcGq4Eeh+I0WFf Xrshc8MHnsNvgonVeDllFmCUSNIaHupRKI95jQ7CJq8AovZR4CthqaB3CahEZFMaGBGEAPEL XC9fIKdHvwIdSi6I8l7kzVCW6LyZZUm0ESStQr917p2ZsHd4DYEuJT4nIx04fHUixwo+zhzE OyS1miMSyd/mWZeFGx+57x2vUEokgTL6qN/mfENTbS7httMWwY+btvHyvBiTsv1QkTHd8uIT 1CvRpOnByswR5Q/2YxGeF5zTvOliB2LxC+2G/kNjbXeBZoo9bzRxXb1INlVxHPP1a1nhF4jE YNULWPzvqdk7EDIApLR1UCQlqKkb6MZiS/L6GCdwHCAuEZHeAF1WKTBG3sYYxietsz3s2XFS bLmErE7Kk1BxMqFf7NNccHshE5aSe3LPd3fZyepmT71C0vQgLyLa4XudiMW2yC15FEstQcV8 D7GMAE/AnzkuGfCFHl1EkqpZUrw8O54oXf9T0kuzgjMYVczn7yysgUYg/CRUZZxlvoNpTshp jNoHV28w8OeCtyOoBBkdbldZtV16UlO1GbQvQhwdpK6KKUqilkbegVx90Tgsnc/QoRGjc80o WkkyA1tAa2d2VJFMTif2NG4O7HaLHXz4AH6c7TfiRnV1Neb/LtK6ext8Q2y+lH0UBB7rTM6i 4owsTPU/JjBAQsMXIikV08280M/vLTGemwm4JuS03RwMK6yuzuE2tQzBeJjxAzzGrUXeK6CC gL2FNUXQsa0L+l/0VmvchUaMfpc8KkrF8yjfvqCnqWsOawz+VDuxXQC+4173k+WomB9TPLPw ZsfzfWfwSOIUj79iBGqtcW9yuUmLXkCW2G4zybjHotYYKZ/KJ0KBWmZKMqy3txihpTpVha07 XabDkgdkI+scBuWNBnm2BFIkF8QuTqhkDe5yDp9l3coqLCe1WrA2baqeB0CM29NDG5s6DWka Ymyk9cEUVKmaw82vBSg7Ef+gaNcoexzInLSTkFBYyXtZzs6A+3g6/zYOpAJtctguD4fSOmmZ FGGVrPxxnlSmzjuGWdT3nFzdj2nvIn4gw0vjWucKHhpq3+KMcp0xBrZ+JndXasLhmtAFHQ+0 2CJQAXkbLzLtZ2OmpzOs/6zTTekX5xXKmzwyJ+Y8TC8/StsCAG+mPa6npvmFxI72Gn1zYoPN 22AoRDib43sz6n/P/hgexwiBVng7NR3AI96lZQYi5QZ2HxcjZKQtyli8y+7IZBA1KTyYWBYD z8N39nL7RLr3Ep8Bn2MzoP9EH6ax4EyArvyKnNT0SU74cdQDa6S57ERhip5rG2zqgfJaOR8l DMQmrM+rWQXiOYTtE8x3z2QV/oMSFJAM3WmxHHqp5iu6b9ab2G1ff2s2VpiyJq/WaqarFgUW W6lKMx/W3YhtoMlbA2KiDqptsnlYIWCM45V7EbP1U6e164Nb8tg85hCzSt/ZTCj4zt8k7R91 Vo2msvi9ImfdzczouTjXk8eZmWzP4RJonnslfoMwZzQhtzpR8Q7XG1MBcuNL7rgESpO56u7c V/UTXtk7C/cQOSXHBfDuh4+/zSWTM/tZzfPYyNAhdR6GEvEexcZ2VFIGm18xtlgSGXIjITga BsrvGhAoA6l7EIWmqQwcECgGmbH+FXyM2lyFcjZdUsMqFkFvhadMNTCvLgqQWcCpczn91bLc ivCNmEqRSkfU0iATTgPJ5GI4t/Nu6idD+u6dL7VZKmW7PdZT7GOzI6u1Y1v+3CNMN+ONz9sF a9z3E0LRn1/F8nD/ldHAyUKiyLAadKarxag62V2qM646vHiRAPo48OGFbJTNdxl/x3+j72EM qacgyNwKDAQ0Z1ppzeA0L8EwFsbkD1jbRGoGLUE8DbPFefex/cRABkcZCd+csBP6uN03wVAP 9LalsKg1rN8ia1QaR8NXljgl8e1IM0SdjvlZRWXWQDRberAeGWYpqO/KbmxQrBRkuhO4hi5u DLAVlTmIizGjD7xERamLeBLiiifeh1YooC0NBh3Wg2BBJrrbAO2NNhvgHg427ox0znLM3IbL zVmfUdKsZWf6CpZhrN0HGkLvR8HZaGU3j2U6eXVMMNcqfxwHiF9jP5X+lw/wrpRqTlGHbl7x XOUodlprFWr1OKIz3A0NXgG4iYOj4WNs0J4PKzf/ZQVQnfI8iUG6mCIAggLrd9oYjUAk69Vw 9nL0qn0LWUbmzo11c4VBsyRMMDedXR8aVzmHznbCAZDRjmuZzm3b6l1n/Sb93nTpZ8/+MCEp Q==
  • Ironport-sdr: 7pre9OQVw+ws9A6dI3OuCXjAIIfNVXM9JkibA/EtkFaHNbZLB3KH7aR/m9v5/N18eAhy2qpLc0 f5yCt+89V0u0o5W76M1WuAGFbx+KRe0YRwE35joc2m31TWBWQGgvB9XTMXBZyrBeyMemev6bJS 2uOlPeksMSbO8HdNPqWjFfiU56d91PA+S86Qu3OTxaVKyyUI/lY9CtzkyeFye39Qj33OkoIJGf wkwh/k02q7CuaPwNZo3X/EwIoTZpD+DhuJYrx/9TsKvZ8g2u6YMCkUPQAxPK1IuF6xu47urT5K y2BWGcA56KmPj3WHZYH998Kx

This would be (another) good feature for a Coq formatter/linter 

I have slowly been working on such a thing but it is not yet in a “production ready” state

Just for fun, the repo is here:

https://github.com/appliedfm/vstyle-tools

Sent from my iPhone

On 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



Archive powered by MHonArc 2.6.19+.

Top of Page