Jason Gross (Apr 29 2021 at 22:29): 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.
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 :-(
Jason Gross (Apr 29 2021 at 22:31):(Elpi then replies with an empty error message, which is questionable...)
Jason Gross (Apr 29 2021 at 22:31):(
File "(stdin)", line 44, characters 2946-2946:
Error:
)
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.
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: Oct 13 2024 at 01:02 UTC