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.
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 :-(
(Elpi then replies with an empty error message, which is questionable...)
File "(stdin)", line 44, characters 2946-2946: Error:
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.
https://github.com/math-comp/hierarchy-builder/blob/d5b96c3f706dd8fccda349bdb0b09ce19e06ac73/structures.v#L351 is a teaser, I know you like backward compat.
Last updated: Jun 06 2023 at 22:01 UTC