search

LPCIC / coq-elpi-lang

VSCode extension for coq-elpi
MIT License
3 stars 0 forks source link

Repeatedly processing the same text gives errors with quote-nested Elpi metavariables #2

Open patrick-nicodemus opened 1 year ago

patrick-nicodemus commented 1 year ago

I think this is a bug but I am not sure. I am new to Elpi.

How to replicate:

  1. Open this in a fresh file in VSCode. https://github.com/LPCIC/coq-elpi/blob/master/examples/example_record_to_sigma.v
  2. Process the text, put cursor at the end and hit Alt-R
  3. Move the cursor to of the head of document, before "From elpi Require Import elpi" and hit Alt-R
  4. Move the cursor to the end of the document and hit Alt-R This yields an error saying that in the clause 
    wrap-fields-bo.aux [X|XS] {{ sigT lp:F }} {{ existT lp:F lp:X lp:Rest }} :-
F = fun _ _ G,
wrap-fields-bo.aux XS (G X) Rest.

    "The reference F is not found in the global environment."

The problem seems to occur more generally with Elpi variables nested within Coq quotes, as in this example. It seems to be necessary that the user runs the "From elpi Require Import elpi" command twice to cause the bug? One gets around the problem by using the Coq reset command, Alt-Home.

gares commented 1 year ago

Yes, you cannot unload Elpi. This is not really specific to Elpi, but to plugins extending Coq grammar.