Michael Soegtrop (Oct 26 2022 at 09:13): 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.
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.
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).
Notification Bot (Oct 26 2022 at 09:52):Michael Soegtrop has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC