Stream: Elpi users & devs

Topic: What is the syntax of comments?


view this post on Zulip Li-yao (Apr 04 2022 at 22:47):

It seems that lp:{{ blocks can be terminated in the same line as a % comment, and braces {{ can be nested in such comments:

From elpi Require Import elpi.
Elpi Program w lp:{{
  % {{
  % }} }}.

How is the end of an antiquotation determined exactly? I'm adding elpi support to coqtail and I'm not sure how to understand this corner case. I'm currently just ignoring the rest of the line after a % but that's not what the Coq/elpi parser is doing.

view this post on Zulip Enrico Tassi (Apr 05 2022 at 06:37):

You have to think that in order to find the end, you don't need the elpi parser. Coq has to parse the string without calling elpi, so % is no different than, say, x. just count for {{ and }}.

Then I believe it is a bit smarter than that, as in you can start with any number of { and the end is when you find the same. But for example vscoq does not understand that.

view this post on Zulip Enrico Tassi (Apr 05 2022 at 06:39):

https://github.com/coq/coq/blob/f2bf445b8f4f5241ebdc348b69961041b4e57883/parsing/cLexer.ml#L542


Last updated: Feb 05 2023 at 13:02 UTC