Stream: Elpi users & devs

Topic: ✔ Question on tutorial


view this post on Zulip Michael Soegtrop (Oct 26 2022 at 09:13):

Following the tutorial (https://lpcic.github.io/coq-elpi/tutorial_coq_elpi_command.html) it is not clear to me what the difference is between:

Elpi Command age.
Elpi Accumulate Db age.db.
Elpi Accumulate lp:{{
:

end

Elpi Command age.
Elpi Accumulate age.db lp:{{
:

I think the command Elpi Accumulate Db age.db. deserves some explanation. My intuition would be that it is the same as the second one, but this does not seem to be the case.

view this post on Zulip Enzo Crance (Oct 26 2022 at 09:25):

Hello. IIUC, Accumulate Db imports a database and makes it visible to a command or tactic, whereas Accumulate age.db adds content to a database that is already visible. In the architecture of a project, this would be reflected as having files declaring the various databases and filling them with initial data (with Accumulate x.db), and files declaring your commands and tactics (that do not necessarily use all the databases you declared) where you make part of the databases visible with Accumulate Db. I will let Enrico correct me if I'm wrong. I agree this could be documented somewhere.

view this post on Zulip Michael Soegtrop (Oct 26 2022 at 09:50):

Ah yes - and it is documented in the same tutorial under (https://lpcic.github.io/coq-elpi/tutorial_coq_elpi_command.html#defining-commands).

view this post on Zulip Notification Bot (Oct 26 2022 at 09:52):

Michael Soegtrop has marked this topic as resolved.


Last updated: Feb 04 2023 at 02:03 UTC