Cyril Cohen (Dec 03 2020 at 20:15): Cyril Cohen (Dec 03 2020 at 20:15):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?
Matthieu Sozeau (Dec 03 2020 at 21:32):That's for @Hugo Herbelin I think
Hugo Herbelin (Dec 04 2020 at 07:04):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.?
Théo Zimmermann (Dec 04 2020 at 08:23):Probably, yes.
Cyril Cohen (Dec 04 2020 at 08:56):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.
Théo Zimmermann (Dec 04 2020 at 08:57):Yeah, it's pretty annoying that warnings are cut to a single line in GitHub Action reporting.
Théo Zimmermann (Dec 04 2020 at 08:58):I'm wondering if changing the printing width when compiling will fix this.
Last updated: Apr 19 2024 at 00:02 UTC