Stream: Coq users

Topic: Notations with (* *)


view this post on Zulip Kenji Maillard (Feb 19 2021 at 16:20):

I just found out that Coq accepts notations containing comments delimiters without complaining, and then fail to make sense out of the resulting mess:

Notation "(*ghost*)" := (5). (* Accepting readily *)

Check (*ghost*).
(* Error: *)
(* Syntax error: [constr:lconstr] expected after 'Check' (in [vernac:query_command]). *)

Definition x := (*ghost*).
(* Error: Syntax error: [reduce] expected after ':=' (in [vernac:def_body]). *)

Is that a bug or a feature ?

view this post on Zulip Kenji Maillard (Feb 19 2021 at 16:23):

The context is that I'm trying to make sense of this line of Coq code, but that's probably a no-op (up to side effects...).

view this post on Zulip Gaëtan Gilbert (Feb 19 2021 at 16:32):

it gets printed fine (though not with 5, I guess because numeral notations interfere)

view this post on Zulip Kenji Maillard (Feb 19 2021 at 16:42):

So that would be a way not to print some garbage term ?
I still don't understand how that can be usefull in the example I linked because the rhs does not seem to typecheck..

view this post on Zulip Enrico Tassi (Feb 19 2021 at 17:28):

it's a feature: https://github.com/coq/coq/blob/a2938972537389b9813794147412f51494f48dd1/theories/ssr/ssreflect.v#L213

view this post on Zulip Guillaume Melquiond (Feb 19 2021 at 17:33):

That said, maybe all of those should be marked (only printing) to make them less confusing.

view this post on Zulip Li-yao (Feb 19 2021 at 17:40):

What does that feature do actually?

view this post on Zulip Enrico Tassi (Feb 19 2021 at 17:44):

Another use case https://github.com/coq/coq/blob/a2938972537389b9813794147412f51494f48dd1/theories/ssr/ssreflect.v#L80-L86 which requires it to be a parsing one (but which cannot be actually parsed)

view this post on Zulip Enrico Tassi (Feb 19 2021 at 17:46):

SSR => [: H ] and abstract: H manage a proof variable H whose type is initially an evar and later a a term. When it is an evar, we print a number, when it gets assigned we print the number in comment. But if you copy paste the type, the number does not get in the way, since it is commented. I think we could survive without that number being printed... but being able to print it in a comment seems a feature to me.

view this post on Zulip Kenji Maillard (Feb 19 2021 at 17:56):

Thanks for the enlightning explanation @Enrico Tassi, I see how that can be useful as a print-only notation.

view this post on Zulip Enrico Tassi (Feb 19 2021 at 17:57):

They are all "little hacks", I just warned in case you tried to remove that "feature"

view this post on Zulip Gaëtan Gilbert (Feb 19 2021 at 17:58):

what's the "dummy" in odd-order for though? https://github.com/math-comp/odd-order/blob/19eb998e2d08c21c6e61806cc7b588238629757e/theories/PFsection3.v#L208

view this post on Zulip Enrico Tassi (Feb 19 2021 at 18:05):

It's funny because I don't know, even if Prop Prop is a term I like to use when I want o assert it does not occur (e.g. as an unused argument of a notation).

view this post on Zulip Enrico Tassi (Feb 19 2021 at 18:07):

And git is not helping: https://github.com/math-comp/mathcomp-history-before-github/commit/ca72e8eb87a1a7feb33c6d447dc2aa7e63940700


Last updated: Feb 09 2023 at 00:03 UTC