Coq PG doesn't recognize the new quotation mechanism of coq/coq#9733

[pi8027]

For example, with the coq-elpi plugin, we can write the following Vernacular command. But PG doesn't recognize the proper end of the command when we do C-c C-n.
https://github.com/LPCIC/coq-elpi/blob/6d21fa61fb59a555c5075ba3e3c89844a5d14bee/theories/tutorial/elpi_lang.v#L53-L58

Elpi Program tutorial lp:{{

  kind person  type.
  type mallory, bob, alice person.

}}.

This quotation mechanism lp:{{ ... }} is introduced by coq/coq#9733. Since the delimiters can be nested, I think that we need a recursive grammar (CFG, PEG, etc.) to detect the end of commands, and couldn't write regexps like coq-end-command-regexp(-backward) anymore to detect it. But I wonder that PG handled the following command properly.

idtac (* (* *) . *).

Does anyone have a workaround or fix for this problem?

cc: @gares

[cpitclaudel]

idtac (* (* *) . *).

That's because Emacs has special handling for comments and strings. I imagine we might be able to piggy-back on this using a syntax-propertize function

[pi8027]

As information for other coq-elpi users, I'd like to record that this workaround does work:

Elpi Program tutorial lp:{{
/*(*/
  kind person  type.
  type mallory, bob, alice person.
/*)*/
}}.

[gares]

Yeah!

Also this one I guess:

Elpi Program tutorial lp:{{
%(*
  kind person  type.
  type mallory, bob, alice person.
%*)
}}.

Altough it is not as cool as yours ;-)

[pi8027]

@gares Unfortunately, that one doesn't work because PG removes newlines from the input before passing it to coqtop... (So we cannot use line comments in Coq PG. Could this be another issue for us? Edit: #362 and #428 might be related.)
Anyway, I can start the tutorial.😂

[theolaurent]

It seems nowadays you can also use strings.

Elpi Program tutorial "
  kind person  type.
  type mallory, bob, alice person.
".

[gares]

This has always been the case, but you have to quote " in there, which can be quite painful.

[phikal]

FWIW this issue can be fixed by evaluating this expression:

(setq coq-end-command-regexp-forward
      (rx (opt "{" (*? anything) "}" (*? anything))
          (or (: (group-n 2 (or (not (any ".")) point ".."))
                 (group-n 1 ".")
                 (group-n 3 (or (syntax whitespace) "}" eos)))
              (: point (group-n 1 (or (one-or-more (group "-"))
                                      (one-or-more (group "+"))
                                      (one-or-more (group "*")))))
              (or (: (group-n 2 point) 
                     (group-n 1 (opt (or (one-or-more (any "0-9"))
                                         (seq "[" (one-or-more (syntax word)) "]"))
                                     (zero-or-more (syntax whitespace))
                                     ":" (zero-or-more (syntax whitespace)))
                              "{")
                     (group-n 3 (zero-or-more (syntax whitespace)) (not (any "{|"))))
                  (: (group-n 2 (or (not (any ".|")) point)) (group-n 1 "}"))))))

It is a bit of a hack (it ensures that any matching brackets are skipped before looking for the end of a proof. Coq-ELPI confuses PG because the Lambda Prolog terms also use . for termination), but I guess it could be converted into a patch, if there is interest.

[SkySkimmer]

It doesn't work with more complicated bracket nesting, eg Check foo:{{ { . } }}..
Maybe we should give up on using regex to find the end of the command.