Stream: Elpi users & devs

Topic: Resolving Extra Dependencies

Philip (Oct 11 2023 at 13:18):

Dies Coq-ELPI have any existing mechanism to resolve extra dependencies?

Enrico Tassi (Oct 11 2023 at 13:53):

Something wrong happened, since this thread title changed.
Anyway, what do you mean exactly by resolving a dependency?

Philip (Oct 11 2023 at 13:57):

Enrico Tassi said:

Something wrong happened, since this thread title changed.
Anyway, what do you mean exactly by resolving a dependency?

Sorry, that was my bad, Zulip confuses me I assumed that this would work like on a mailing list :/

What I mean is I want my Elpi command to take a Extra Dependency identifier and resolve the file name bind that. I couldn't find anything in the coq_elpi_builtins.ml. Did I miss something, or could I propose a patch?

Enrico Tassi (Oct 11 2023 at 14:27):

There is no such an API.
The names defined by Extra Dependency are available to Elpi Accumulate, you can look at it for the Coq API it uses.
But I'm not so sure I get what you want to do from Elpi itself.

Philip (Oct 11 2023 at 19:17):

I want to parse an external file, and instead of having to pass a string with a path, I'd like to make use of Coq's system for external dependencies.

Enrico Tassi (Oct 11 2023 at 20:52):

Right, and why accumulating it via Elpi Accumulate is not an option?

Philip Kaludercic (Oct 12 2023 at 10:36):

I assumed that Elpi Accumulate would add code to the current program, while I just want to get determine the file path behind an extra dependency.

Enrico Tassi (Oct 12 2023 at 11:29):

OK, then yes please expose the API for that. As I was saying the Coq API is here:

https://github.com/LPCIC/coq-elpi/blob/e5f9a7feca641e31831718432ea19b71308ce036/src/coq_elpi_programs.ml#L322-L334

Actually, Elpi initialization takes a file resolver for accumulate "something"., and that resolver is defined using Coq's APIs.
In particular external dependencies are encoded as coq://logical/path/file (if the dep is Elpi Accumulate file From logical.path.).

So maybe you could expose the resolver API in Elpi directly, and when Elpi is used inside Coq you would get it to do what you want by calling the API on a "coq URI".

Enrico Tassi (Oct 12 2023 at 11:40):

After thinking a bit more, this is the easiest:

• bind https://github.com/LPCIC/elpi/blob/master/src/API.mli#L109 in Coq-Elpi
• use ensure_initialized in Coq_elpi_programs to get the elpi handle
  • you need to put Coq_elpi_programs before Coq_elpi_builtints in here https://github.com/LPCIC/coq-elpi/blob/master/src/elpi_plugin.mlpack to make the api visible
• call the API with the coq://.... syntax on the external dependency

Enrico Tassi (Oct 12 2023 at 11:43):

The external predicate could be coq.locate-extra-dep i:list string, i:string, o:string. to be called as in coq.locate-extra-dep ["logical","path"] "file.elpi" Path.

Last updated: Oct 13 2024 at 01:02 UTC