Stream: Elpi users & devs

Topic: Using Elpi with Emacs/PG


view this post on Zulip Jason Gross (Apr 29 2021 at 22:29):

Is there a good way to make use of .v files with elpi in them in Emacs/PG? It seems that interaction is broken if I try to include both elpi and Coq code, because PG will wait for Coq's response on the first . before continuing, while coqtop thinks it needs to wait for the end of the elpi quotation to give response.

view this post on Zulip Jason Gross (Apr 29 2021 at 22:30):

I can kludge this by replacing every . at the end of a line with .%, but things still don't work because PG removes all newlines :-(

view this post on Zulip Jason Gross (Apr 29 2021 at 22:31):

(Elpi then replies with an empty error message, which is questionable...)

view this post on Zulip Jason Gross (Apr 29 2021 at 22:31):

(

File "(stdin)", line 44, characters 2946-2946:
Error:

)

view this post on Zulip Enrico Tassi (Apr 30 2021 at 06:06):

Sorry, no Emacs. There is an open issue btw on the PG tracker. Either viscose or coqide. But you can also put the Elpi code in a separate file and use Accumulate File, inline code is nice for examples and quick hacks, I never use it in final products.

view this post on Zulip Enrico Tassi (Apr 30 2021 at 06:09):

https://github.com/math-comp/hierarchy-builder/blob/d5b96c3f706dd8fccda349bdb0b09ce19e06ac73/structures.v#L351 is a teaser, I know you like backward compat.


Last updated: Feb 04 2023 at 02:03 UTC