8000 Coq PG doesn't recognize the new quotation mechanism of coq/coq#9733 · Issue #437 · ProofGeneral/PG · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
pi8027 opened this issue Aug 8, 2019 · 8 comments
Open

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

pi8027 opened this issue Aug 8, 2019 · 8 comments

Comments

@pi8027
Copy link
Contributor
pi8027 commented Aug 8, 2019 •
edited
Loading

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 rocq-prover/rocq#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
Copy link
Member

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
Copy link
Contributor Author
pi8027 commented Aug 8, 2019

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
Copy link
Contributor
gares commented Aug 8, 2019

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
Copy link
Contributor Author
pi8027 commented Aug 8, 2019 •
edited
Loading

@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
Copy link
theolaurent commented Aug 10, 2022 •
edited
Loading

It seems nowadays you can also use strings.

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

@gares
Copy link
Contributor
gares commented Aug 10, 2022

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

@Zimmi48 Zimmi48 mentioned this issue Sep 30, 2022
Open
@phikal
Copy link
Contributor
phikal commented Aug 4, 2023

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
Copy link
Contributor

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
3641
Development

No branches or pull requests
6 participants
@pi8027 @gares @SkySkimmer @phikal @theolaurent @cpitclaudel
0