In Coq 8.13 dev, I keep getting the warning grammar entry "ident" permitted "_" in addition to proper
here and there.
The formulation of this warning is cryptic to me, and there is no corresponding switch I can look up in the doc.
Can someone refer me to the appropriate section of the manual?
My best guess is that I am using ident
instead of binder
, maybe?
That's for @Hugo Herbelin I think
This is coq/coq#11841, look for -deprecated-ident-entry
in the syntax extension chapter. Doesn't the warning occur at a line where your precisely use ident
?
Would it be clearer if, e.g., the warning were just grammar entry "ident" is deprecated and its meaning will change in the future; use "name" instead.
?
Probably, yes.
Hugo Herbelin said:
Doesn't the warning occur at a line where your precisely use
ident
?
I just noticed it does, except since the warning is cut over several lines, github action does not display it completely. And the rest of the message is clearer... My bad and sorry for the noise.
It would be nice if we could print all the warnings and error in a single line, to take maximal advantage of github actions reporting them in the PR code.
Yeah, it's pretty annoying that warnings are cut to a single line in GitHub Action reporting.
I'm wondering if changing the printing width when compiling will fix this.
Last updated: Oct 13 2024 at 01:02 UTC