ProofGeneral/PG

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

pi8027 opened this issue · 7 comments

pi8027 commented

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 commented

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 commented

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 commented

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 commented

@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 commented

It seems nowadays you can also use strings.

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

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

phikal commented

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.

  • 👍1
  • ❤️1