The Coq mailing list

[Abhishek Anand <aa755 AT pm.me>]

That rg query doesnt seems to match anything, perhaps there is some minor syntactic issue. Based on my understanding of what it is intended to do, I do have some corner cases like a file containing "Binary Search tree" in comments, so it is not something I would enforce in CI. but it is good enough to manually find the possible leftovers. To further ease the process, I wrote an emacs function to create a hyperlinked list of all (leftover) queries:

One can use the following elist to bind C-c M-u automate the following: go to the project root (nearest dir ancestor containing _CoqProject) of the currently open .v file and look for query commands in .v files in all (sub)dirs starting from there:

(defun check-coq-query ()

  (interactive)

  (let* ((proot (locate-dominating-file (buffer-file-name) "_CoqProject")))

    (grep (concat "egrep -e '(^Search\s|[^A-Za-z0-9]Search\s|^Locate\s|[^A-Za-z0-9]Locate\s|^About\s|[^A-Za-z0-9]About\s)'  --include=\"*.v\" -rn " proot))))

(eval-after-load 'company-coq

                 '(define-key company-coq-map (kbd "C-c M-u") 'check-coq-query))

--

Abhishek Anand

------- Original Message -------
On Friday, February 18th, 2022 at 4:18 PM, Tej Chajed <tchajed AT mit.edu> wrote:

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