The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi all,

"hate" is not a word I would use (nor has anyone used it in this thread I 
think), but my main issue with them is that they clutter the output of `make`, 
making it harder to see actual warnings or other diagnostics one should care about.

; Ralf

On 18.02.22 20:34, Vedran Čačić wrote:
> I never understood what's the point of that. Coq scripts are not just "for 
> machines to execute", they are also "for humans to read", and in that context, 
> occasional Check, or Print, or even Search, can be very informative. Previous 
> versions of Coq warned of such usage, now I see the warning is gone, and I was 
> happy because I thought it signified that query commands are officially 
> supported in scripts now. Obviously I was wrong, but I still don't understand 
> why you hate them.
>
> pet, 18. velj 2022. u 22:19 Tej Chajed <tchajed AT mit.edu 
> <mailto:tchajed AT mit.edu>> napisao je:
>
>     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
>     <mailto: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 <mailto: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
> >         <https://github.com/appliedfm/vstyle-tools>
> >
> >         Sent from my iPhone
> >
> > >         On Feb 17, 2022, at 4:39 PM, Abhishek Anand <aa755 AT pm.me
> > >         <mailto: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
>
>
>
> --
> Vedran Čačić

--
Website: https://ralfj.de/research