Stream: Elpi users & devs

Topic: Tactic populating database at runtime does not work


view this post on Zulip Enzo Crance (Jul 22 2021 at 10:21):

Hello. I have an elpi database I want to populate through a vernacular command (making the database grow a priori with static knowledge without a user having to touch elpi to add things manually) and a tactic (adding things to a database while solving a goal with Ltac). It looks like the command works but not the tactic. Let me show you a bit of the file architecture (along with a diagram).

Key: Green arrows mean that the file at the head of the arrow has a Require Export of the file at the source of the arrow. Red arrows mean Require Import. Grey arrows mean Elpi Accumulate File.

view this post on Zulip Enzo Crance (Jul 22 2021 at 10:22):

IMG_2091.jpg

view this post on Zulip Enzo Crance (Jul 22 2021 at 10:22):

So here is a short explanation. I have a Commands.v file containing both the command and the tactic. Both do the same thing, so they internally call a common predicate add written in an elpi file commands.elpi, that accumulates a clause to a x.db database. Both the command and the tactic need the initial DB and the elpi code to be defined. I think I had a bug once when the database wasn't sourced with Require Export, so I used green arrows when sourcing the DB, but that might be a reason for the current bug, idk.

I also have a Tactic.v file defining my main tactic which only uses the DB as information but does not push anything into it. Therefore, in the Test.v file, I have access to:

Do you have an idea? I hope I am as clear as possible and the diagram helps. Thanks in advance for your help.

view this post on Zulip Enrico Tassi (Jul 22 2021 at 10:38):

Hum, I think the code should raise an error if you call coq.elpi.accumulate from a tactic (since it is not supported). I guess I forgot to add it.
Said that I'd like a little proof script example where you use add and then your tactic. There must be a way out without using a global db, in particular C => works like coq.elpi.accumulate (clause C) but does not have a persistent effect, so we should have all we need.

view this post on Zulip Enzo Crance (Jul 22 2021 at 10:57):

Proof.
  add T U.
  main_tactic.

vs

Add T U.
Goal ...
Proof.
  main_tactic.

Only the second one works. But I guess if we want to use => then the add tactic would have to take a sort of continuation as an argument, otherwise it does not know what to put at the right of the arrow.

view this post on Zulip Enzo Crance (Jul 22 2021 at 11:00):

Or maybe we could put the arguments of add in a global variable that the main_tactic can access, thus consuming them and emptying this variable for next calls in the Coq file. But I do not know if that notion of global variable exists.

view this post on Zulip Enrico Tassi (Jul 22 2021 at 12:03):

If T and U are "global", then you should use Add in the middle of the proof. Unfortuantely the addition will be global, and not local to the proof, but this is a general Coq problem.

view this post on Zulip Enrico Tassi (Jul 22 2021 at 12:05):

Yes, I was thinking to something like main_tactic with U, V and internally do [caluase_for_U , clause_for_V] => usual_code

view this post on Zulip Enrico Tassi (Jul 22 2021 at 12:05):

This works fine even if U and V are proof variables and not global terms.

view this post on Zulip Enrico Tassi (Jul 22 2021 at 12:06):

No, there is no notion of global, mutable, variable. I could add one, I think it may be useful, but here it seems unnecessary.

view this post on Zulip Enzo Crance (Jul 22 2021 at 12:21):

Enrico Tassi said:

Yes, I was thinking to something like main_tactic with U, V and internally do [clause_for_U , clause_for_V] => usual_code

I will try something like this. Thanks for the suggestion.

view this post on Zulip Enrico Tassi (Jul 22 2021 at 12:36):

I think you should be able to do

Tactic Notation "mytac" "with" constr_list_sep(l, ",") := elpi main_tactic ltac_term_list:(l).

to get your tactic called with a list of term arguments as in

solve (goal _ _ _ _ [trm <the_term_for_U>, trm <the_term_for_V>]) _ :- ...

Hope it works.


Last updated: Mar 28 2024 at 15:01 UTC