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.