search

LPCIC / coq-elpi

Coq plugin embedding elpi
GNU Lesser General Public License v2.1
139 stars 51 forks source link

Undoing `Require` does not unload Elpi commands #452

Closed Blaisorblade closed 1 year ago

Blaisorblade commented 1 year ago

Discovered on derive — not minimized. Here, the syntax remains in place after stepping back; https://github.com/LPCIC/coq-elpi/issues/449 also has an issue with Undo, but there undoing works and redoing doesn't.

With #[only(eq_dec)] derive some_type.:

File "./fmdeps/cpp2v-core/theories/lang/cpp/model/inductive_pointers.v", line 279, characters 18-24:
Error:
Syntax error: [quoted_attributes] or [vernac] expected (in [decorated_vernac]).

With derive alloc_id_aux.:

File "./fmdeps/cpp2v-core/theories/lang/cpp/model/inductive_pointers.v", line 279, characters 2-8:
Error: Syntax error: illegal begin of vernac.
Blaisorblade commented 1 year ago

Relatedly, a colleague has reported an unexplained Syntax error: entry [elpi_loc] is empty. in Proof General (fixed by restarting proof general). In coq-lsp, I'm also seeing spurious Syntax error: entry [elpi_loc] is empty. in code that does not load elpi, but only if I open other files that do load elpi.

gares commented 1 year ago

Hum, LSP wants one server for all your files... so I guess the bug leaks. What I still don't get is what is coq-elpi specific.. there are other plugins extending the grammar...

Blaisorblade commented 1 year ago

oh maybe it's just https://github.com/coq/coq/issues/12575 / https://github.com/coq/coq/pull/17069

Blaisorblade commented 1 year ago

Not quite — https://github.com/coq/coq/pull/17069 was backported.

But comments there suggest plugins need changes — SkySkimmer mentions elpi needs special support since it has an evolving grammar.

gares commented 1 year ago

@SkySkimmer can you help me reproduce the problem and fix elpi? I tried with Reset Initial but I could not get a bug.

SkySkimmer commented 1 year ago

I'll try to have a look next week

SkySkimmer commented 1 year ago

IIRC the idea is that you do Elpi Export of some program (or Import something that does), then backtrack (either interactively, or closing the current module), the exported syntax is still active.

SkySkimmer commented 1 year ago

https://github.com/LPCIC/coq-elpi/pull/463

SkySkimmer commented 1 year ago

Relatedly, a colleague has reported an unexplained Syntax error: entry [elpi_loc] is empty. in Proof General (fixed by restarting proof general).

This may be a bug in the grammar engine state reset. Hard to say without reproducing.