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?
You need to register your action using Libobject.
Or use Elpi and its acumulation mechanism, which does it behind the scenes for you.
Cool, thanks! I'll give this a go!
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?
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
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.
should the module stuff ever become relevant, https://link.springer.com/chapter/10.1007/10930755_18 will be relevant
Last updated: Nov 29 2023 at 18:01 UTC