Hello. I would like to harness proofs using Elpi, that were made with the universe polymorphism option enabled, but when calling a tactic I get a "not yet implemented" error. What would it take to add this kind of feature to Coq-Elpi?
I will try to see if I can bypass this, but I am afraid it is likely to be a crucial point in the proofs I am using (univalent parametricity). I am willing to help if you don't have time to implement such a feature. I would just probably need an introduction to the Elpi internals beforehand.
Thanks in advance. Have a nice week-end.
Help is surely welcome. I have a PR to be refined. Maybe we can chat via visio next week?
I have a related(?) issue so I'm reviving this thread; I'm happy to move to a new thread as well.
We have infrastructure for generating "hints" that can later be registered and utilized by our internal proof automation, and I would like to be able to execute this "hint" generation and registration within
elpi. Unfortunately this infrastructure utilizes
Set Universe Polymorphism/
Set Polymorphic Inductive Cumulativity, and this results in terms containing universes. Based on the error message, it seems as if using
coq.ltac.call to invoke the tactic succeeds in generating this (universe-containing) term - at which point the injection of the Coq-constr back into elpi fails; the
constr2lp case for
C.const calls check_univ_inst, which itself checks Univ.Instance.is_empty.
Generating and registering these "hint" terms is extremely important for our elpi use-case. Do you have a status update regarding support for this functionality (or a link to the relevant PR)? What blockers do you see w.r.t my particular use case?
Here is a relevant PR: https://github.com/LPCIC/coq-elpi/pull/315
Thanks Ali, yes we are working on it. I'll detail better the plan so that you can tell me which features are more relevant to you.
How to do it is now clear, but which feature to implement first is open. With that branch you can probably alreary read from coq a upoly term, but not write it for example.
Wonderful! Thank you for working on this :~) I will take a look at the PR and comment regarding features which seem relevant to our use case (@Janno do you mind also taking a look?).
Fwiw, Janno was able to find a workaround which seems to be sufficient for the near-term use-cases we have for elpi, so luckily we are not immediately blocked on this feature. However, we certainly prefer an approach in which universes are handled in a principled way within elpi itself!
Just to make sure I'm not missing something: is the current (pre-PR) status of coq-elpi that it's incapable of dealing with any terms involving universe polymorphism? Or is there some workaround?
Not that I'm aware of, there is no work around. I count one more user interested in the feature. It happens both @Enzo Crance and mayself had to focus on other things, so https://github.com/LPCIC/coq-elpi/pull/315 did not make progress. Still you can already read a polymorphic term from the environment, but not write one to, with that PR, see the very simple example here: https://github.com/LPCIC/coq-elpi/pull/315/files#diff-913332ff5affe04bc3a3a00beb38b7164761f2f35c4f21fc11c17ec531c9ec2d
The current plan is to go back to work on this feature soonish, possibly with a sprint (in person) in June. Hope it helps.
Last updated: Feb 05 2023 at 15:03 UTC