Enzo Crance (Feb 28 2023 at 10:53): Enzo Crance (Feb 28 2023 at 10:53):Hello.
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 Elpi Tactic).
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?
Enrico Tassi (Feb 28 2023 at 12:30):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.
Enzo Crance (Mar 02 2023 at 08:50):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.
Enrico Tassi (Mar 02 2023 at 10:24):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 #[arguments(raw)]. Eg #[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: Oct 13 2024 at 01:02 UTC