Stream: Dune devs & users

Topic: Elpi Support


view this post on Zulip Ali Caglayan (Jun 20 2023 at 22:07):

Over the summer I hope to support "extra sources" in dune so people with elpi projects can compile their code using dune. I had a prototype at some point, still need to think some things over.

view this post on Zulip Notification Bot (Jun 20 2023 at 22:08):

A message was moved here from #Dune devs & users > Dune 3.8 theories declarations by Emilio Jesús Gallego Arias.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 20 2023 at 22:08):

Maybe it would be even easier just to consider .elpi files as sources

view this post on Zulip Ali Caglayan (Jun 20 2023 at 22:10):

Yeah that could be done. We would need some garuntees about elpi's compilation workflow however. Haven't thought much about it yet.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 20 2023 at 22:10):

As of today coqdep will register the dep properly, but the file needs to be copied to the build dir right?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 20 2023 at 22:11):

So that's where the problem was, I think

view this post on Zulip Emilio Jesús Gallego Arias (Jun 20 2023 at 22:11):

Actually on Flèche I'm using a better mechanism, I emit an effect on require, so no need for coqdep

view this post on Zulip Emilio Jesús Gallego Arias (Jun 20 2023 at 22:11):

and commands that read files need to declare that on their type

view this post on Zulip Emilio Jesús Gallego Arias (Jun 20 2023 at 22:12):

so we can rev-look

There has been friction with getting this API in Coq, but it is a pity because it does provide a lot of advantages

view this post on Zulip Ali Caglayan (Jun 20 2023 at 22:12):

yeah I guess the plugin takes the .elpi sources together.

view this post on Zulip Ali Caglayan (Jun 20 2023 at 22:13):

So the effect on require was the reason you don't like separation of parsing / exec?

view this post on Zulip Paolo Giarrusso (Jun 21 2023 at 09:31):

seems requires and imports must still be executed eagerly even with separation to enable parsing

view this post on Zulip Paolo Giarrusso (Jun 21 2023 at 09:34):

because you need parse rules from notations (and might want to install their interpretation eagerly or not, that seems less obvious), right?

view this post on Zulip Paolo Giarrusso (Jun 21 2023 at 09:35):

But back to elpi, we indeed ran into this problem, down to ".elpi files aren't in _build because coq rules hardcode that they copy .v files"

view this post on Zulip Emilio Jesús Gallego Arias (Jun 21 2023 at 11:48):

Ali Caglayan said:

So the effect on require was the reason you don't like separation of parsing / exec?

No. What I mean by "I emit and effect on require" is that when a require is executed, the build manager is called back, and if the object is not ready, it will be built.


Last updated: May 25 2024 at 20:01 UTC