Paolo Giarrusso (Dec 01 2022 at 01:56): 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?
Paolo Giarrusso (Dec 01 2022 at 01:57):MetaCoq seems to have the same problem https://github.com/MetaCoq/metacoq/issues/794
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
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.
Enrico Tassi (Dec 01 2022 at 08:08): Enrico Tassi (Dec 01 2022 at 08:09):For the API, I don't have time before mid December
Paolo Giarrusso (Dec 01 2022 at 11:05):Thanks for fhe prompt response!
Last updated: Oct 13 2024 at 01:02 UTC