Stream: Coq Universe

Topic: Adding elpi to coq-universe


view this post on Zulip Roland Coeurjoly (Jun 10 2022 at 16:20):

Does it make sense to add elpi to coq-universe? It is not a coq development but it can be used with coq.

view this post on Zulip Paolo Giarrusso (Jun 10 2022 at 19:18):

I think so, especially since elpi and coq-elpi often evolve in lockstep

view this post on Zulip Paolo Giarrusso (Jun 10 2022 at 19:20):

Said otherwise, if developing elpi can require rebuilding client coq libraries, it seems to make sense. But I'm an outsider, and @Enrico Tassi knows better

view this post on Zulip Emilio Jesús Gallego Arias (Jun 11 2022 at 09:31):

@Roland Coeurjoly for now we are not vendoring OCaml packages, as this is usually a bit more complex. But for example elpi or menhir (which Ali did vendor originally) could be added to it

view this post on Zulip Emilio Jesús Gallego Arias (Jun 11 2022 at 09:31):

Tho I feel that the primary goal of this project is to gather projects that contain .v files, that is to say, Coq projects

view this post on Zulip Enrico Tassi (Jun 11 2022 at 12:13):

Do you mean elpi or coq-elpi? Because elpi alone has to be seen as an ocaml dependency, like zarith or menhir.

coq-elpi is a Coq project, why not add it. But it does not have a dune file for a technical reason: only from Coq 8.16 it will be possible to build (and load) a working coq-elpi with dune. @Emilio Jesús Gallego Arias wrote the dune file a few times, but it was never ok, for that technical reason primarily. So maybe we should wait a month (8.16 will come out soon), and then try again porting coq-elpi to dune.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 11 2022 at 12:27):

They are talking about elpi, not coq-elpi

view this post on Zulip Paolo Giarrusso (Jun 11 2022 at 18:32):

my answer was about elpi — for the goals of coq-universe, I guess the question is how often changes to elpi itself might propagate to e.g. hierarchy-builder and hb-based-math-comp

view this post on Zulip Enrico Tassi (Jun 11 2022 at 20:18):

elpi and coq-elpi go in tandem, but then coupling typically stops there

view this post on Zulip Ali Caglayan (Jun 14 2022 at 14:10):

@Emilio Jesús Gallego Arias Do you have a link to the dune branch, we should add elpi as an opam dep, and then put your branch of coq-elpi in. I would love to get HB working (with dune).

view this post on Zulip Emilio Jesús Gallego Arias (Jun 14 2022 at 14:11):

Actually we should discuss how to do this

view this post on Zulip Emilio Jesús Gallego Arias (Jun 14 2022 at 14:11):

because my branch was a hack

view this post on Zulip Ali Caglayan (Jun 14 2022 at 14:14):

What is the main barrier today? The elpi plugin relying on .elpi files?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 14 2022 at 14:14):

coq-elpi relying on fl_dynload

view this post on Zulip Emilio Jesús Gallego Arias (Jun 14 2022 at 14:14):

so we need to update dune

view this post on Zulip Emilio Jesús Gallego Arias (Jun 14 2022 at 14:15):

that would be easy, if not for this bug

view this post on Zulip Emilio Jesús Gallego Arias (Jun 14 2022 at 14:15):

https://github.com/ocaml/dune/issues/5833

view this post on Zulip Ali Caglayan (Jun 14 2022 at 14:16):

Are we talking about the plugin loading or is elpi doing something else with fl_dynload?

view this post on Zulip Ali Caglayan (Jun 14 2022 at 14:21):

OK so same problem every plugin is having.

view this post on Zulip Ali Caglayan (Jun 14 2022 at 14:21):

I will propose the work around of (package ...) and putting the plugin in a separate library.

view this post on Zulip Ali Caglayan (Jun 14 2022 at 14:22):

Not that we should merge that into coq-elpi, but we will at least be able to use it

view this post on Zulip Ali Caglayan (Jun 14 2022 at 14:31):

The reason I think we should use a work around for now, is that the fix you were describing with a ".lib" runtime dep folder, is probably gonna take some work to set up in Dune. I am still not fully convinced that it is what we want for doing fl_dynload, but I am not against it either.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 14 2022 at 14:37):

Not the same problem, elpi is actually really loading elpi as a dep

view this post on Zulip Emilio Jesús Gallego Arias (Jun 14 2022 at 14:38):

their previous methods was broken in 4.08, so hence why Enrico did implement that

view this post on Zulip Emilio Jesús Gallego Arias (Jun 14 2022 at 14:39):

Ali Caglayan said:

I will propose the work around of (package ...) and putting the plugin in a separate library.

Umm, I think that doesn't work either

view this post on Zulip Emilio Jesús Gallego Arias (Jun 14 2022 at 14:40):

We could just depend on package internally, try that, but it is broken by the same bug I think

view this post on Zulip Emilio Jesús Gallego Arias (Jun 14 2022 at 17:08):

Actually coq-elpi should work fine with dune now as long as you use the compat syntax

view this post on Zulip Emilio Jesús Gallego Arias (Jun 14 2022 at 17:08):

it won't work if we compose it with elpi!

view this post on Zulip Emilio Jesús Gallego Arias (Jun 14 2022 at 17:08):

but if elpi is installed in opam, I think that should fine

view this post on Zulip Emilio Jesús Gallego Arias (Jun 14 2022 at 17:08):

Umm, maybe we get some problem composing with Coq, but should be very hard to trigger

view this post on Zulip Emilio Jesús Gallego Arias (Jun 14 2022 at 17:11):

Indeed, if you look carefully at dep_conf_eval.ml

view this post on Zulip Emilio Jesús Gallego Arias (Jun 14 2022 at 17:11):

where (package ...) is implemented

view this post on Zulip Emilio Jesús Gallego Arias (Jun 14 2022 at 17:12):

I don't see why depending on package won't trigger the same bug

view this post on Zulip Emilio Jesús Gallego Arias (Jun 14 2022 at 17:13):

What is this doing tho?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 14 2022 at 17:13):

let package_install ~(context : Build_context.t) ~(pkg : Package.t) =
  let dir =
    let dir = Package.dir pkg in
    Path.Build.append_source context.build_dir dir
  in
  let name = Package.name pkg in
  sprintf ".%s-files" (Package.Name.to_string name)
  |> Alias.Name.of_string |> Alias.make ~dir

Last updated: Feb 06 2023 at 05:03 UTC