When I work with Coq-Elpi, I usually open a command, import my Elpi files and databases, then do an
Elpi Query block testing my main predicates on custom test cases. Now, if I want to build a command or a tactic from this code, I can just wrap it in a
main predicate where the code processes the arguments of the command instead of my test cases, or a
solve predicate processing the goal and context in the case of a tactic (+ changing
Elpi Command to
This morning, I ran into a case where just changing one line from
Elpi Command to
Elpi Tactic made the code fail one my test cases with a Coq term error:
The term pglobal X2 X3 cannot be represented in Coq since its gref or univ-instance part is illformed
What could be the source of the bug?
Hard to say with little context.
One difference is the code which is loaded automatically, see https://github.com/LPCIC/coq-elpi/blob/master/elpi/elpi-command-template.elpi vs https://github.com/LPCIC/coq-elpi/blob/master/elpi/elpi-command-template.elpi
The main difference is this one, IIRC: https://github.com/LPCIC/coq-elpi/blob/efcf63c433834592beb221c09a5e76f9a847128a/elpi/coq-elaborator.elpi#L7-L9
It is impossible for me to say how it impacts your code exactly.
What it does is that, if you are building a tactics, evars (uvars linked to coq evars) assignments gets typechecked by Coq. While for commands it is not the case. I'm not defending the choice, just documenting it.
Sorry for being abstract, but I think it was sufficient for you to find the reason of the bug. I guess the
evar constraints come from calls to
coq.typecheck made while forging a term which contains holes, and when I fill these holes, the
evar goals are resumed and fail. What is surprising is that my final crafted term passes
coq.typecheck with the expected type. I wonder if it's because of
coq.elaborate-skeleton being called — a predicate I try to keep away from me, mainly because it refreshes all the universe levels IIRC.
Is it possible to create a tactic that does not add this additional case for the
evar predicate? I mean, there's a
:name "coq-assign-evar" right before so it can be indexed with this name I guess. Maybe it's a dirty way to bypass the problem and my crafted term really has a problem, but if it is the case I prefer having the Coq
refine call fail and tell me the typing error.
yes, put a clause before that which does nothing and cuts the others away (like the default one). I think I should turn this feature into an explicit option, as for
#[evars(raw)], rather than having to hack a clause.
IMO you build a term which is not well typed (maybe there are Type levels which are not ok), but can be fixed (easily) by refreshing the levels (or also inserting a coercion). Note that refine in the end calls elaborates: https://github.com/LPCIC/coq-elpi/blob/master/elpi/elpi-ltac.elpi#L9 . I guess that if you call refine.typcheck instead, you get the error which makes your current code fail (earlier).
Last updated: Jun 07 2023 at 00:01 UTC