Rodolphe Lepigre (Feb 13 2023 at 17:34): Rodolphe Lepigre (Feb 13 2023 at 17:34):I'd like to write a plugin that accumulates identifiers in its internal state using a custom vernacular command, and that set can be queried using another command. The intended behaviour I have in mind is the following: at the end of a file, if I query the set, then I expect it to contain all identifiers declared in the file or in its transitive dependencies. I naively thought I could achieve this using Summary.ref, but it seems that this only maintains the state internally to a given file. Is there an higher-level abstraction I can use to do what I want?
Enrico Tassi (Feb 13 2023 at 17:39):You need to register your action using Libobject.
Or use Elpi and its acumulation mechanism, which does it behind the scenes for you.
Rodolphe Lepigre (Feb 13 2023 at 19:08):Cool, thanks! I'll give this a go!
Rodolphe Lepigre (Feb 14 2023 at 08:58):I'm having trouble understanding how Libobject works, since the ocamldoc documentation is quite scarce. I tried declaring something using Libobject.declare_object (Libobject.global_object ~cat name ~cache ~subst ~discharge), implementing all functions with assert false as their body, and then called the resulting function on some dummy object to see what would trigger, and nothing seems to happen (I do not get any assertion failure). What am I missing here?
Also, I'm not yet sure I understand what is meant by "substitution" and "discharge" in the documentation. I'm pretty sure this is pretty simple, but the terminology is not clean. Could anyone explain?
Enrico Tassi (Feb 14 2023 at 09:37):It is related to modules (substitution is for functors) and sections.
I'd rather point you to this POC: https://github.com/LPCIC/coq-elpi/blob/master/examples/example_data_base.v
Rodolphe Lepigre (Feb 14 2023 at 10:14):I'll have a look to this, thanks.
@Janno pointed me to the plugin tutorial, where there is an example with a persistent counter which is similar to what I want to achieve.
Paolo Giarrusso (Feb 14 2023 at 14:08):should the module stuff ever become relevant, https://link.springer.com/chapter/10.1007/10930755_18 will be relevant
Last updated: Jun 09 2023 at 08:01 UTC