The Coq mailing list

[Tej Chajed <tchajed AT mit.edu>]

This kind of problem is hard in general because you need to process comments and strings at a minimum. However if you’re just trying to catch stray commands that trusted developers make, I would think rg -g '*.v' '^\s*(Search|Locate|Print)\b' would be a pretty good solution. I'd be curious where this kind of regex fails for your use case Abhishek.

Adding the feature to Coq itself has the downside that the check is coupled with compilation, which is much slower than a simpler syntactic check.

On Thu, Feb 17, 2022 at 10:52 PM Abhishek Anand <aa755 AT pm.me> wrote:

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:

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