Stream: Coq users

Topic: warning: `grammar entry "ident" permitted "_" in addition...


view this post on Zulip 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?

view this post on Zulip Matthieu Sozeau (Dec 03 2020 at 21:32):

That's for @Hugo Herbelin I think

view this post on Zulip 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.?

view this post on Zulip Théo Zimmermann (Dec 04 2020 at 08:23):

Probably, yes.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Dec 04 2020 at 08:58):

I'm wondering if changing the printing width when compiling will fix this.


Last updated: Jan 31 2023 at 14:03 UTC