Stream: Elpi users & devs

Topic: `.glob` entries from elpi


view this post on Zulip Paolo Giarrusso (Dec 01 2022 at 01:56):

@Abhishek Anand noticed that constants from coq-elpi (created via coq.env.add-const) don't show up in .glob files — are we misusing the Coq-Elpi API, or could coq.env.add-const hook into the appropriate Coq API?

view this post on Zulip Paolo Giarrusso (Dec 01 2022 at 01:57):

MetaCoq seems to have the same problem https://github.com/MetaCoq/metacoq/issues/794

view this post on Zulip Paolo Giarrusso (Dec 01 2022 at 01:59):

the motivation is that Abhishek's using the definition entries to improve Company Coq's jump-to-definition

view this post on Zulip Enrico Tassi (Dec 01 2022 at 08:05):

I Think the right API is to give you a way to emit an entry into a glob file.

FTR Elpi passes to each command the invocation loc (as an attribute), and you can store that as a clause linked to the constant. We do that in HB and retrieve that with HB.about.

You can probably hack the .glob by opening the file in append mode and write in there a line, but of course that is a bit too low level to be recommend. We do something like this in HB as well, so the APIs are there.

view this post on Zulip Enrico Tassi (Dec 01 2022 at 08:08):

https://github.com/LPCIC/coq-elpi/blob/834323a62682db872eec95ced06d4b273cbe3400/elpi-builtin.elpi#L1142

view this post on Zulip Enrico Tassi (Dec 01 2022 at 08:09):

For the API, I don't have time before mid December

view this post on Zulip Paolo Giarrusso (Dec 01 2022 at 11:05):

Thanks for fhe prompt response!


Last updated: Mar 29 2024 at 14:01 UTC