The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi,

I wouldn’t call ltac “human readable”. Only gallina (commands like lemmas statements, but not tactics) is readable to me. I find proof scripts, being interactive and highly imperative, are not readable without replaying them.

IMHO Most printing command are for interactive purpose and should not remain in the .v file (and should better not be written in a file since most IDE allow to send them to coqtop without writing them in the file).

That said I often use special commands in dedicated files, for instance a few "Print Assumptions <mylemma>" precisely to see the output at compile time. I could also do a few Print and Check to ensure critical definitions have not been changed. So IMHO there should be some way to tell "yes please do this even at compile time". Is there such a way?

Best,

Pierre

 

Le lun. 21 févr. 2022 à 08:28, Vedran Čačić <veky AT math.hr> a écrit :

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> 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> 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

--

Vedran Čačić